GoLLVM semantics

a not well tested toy project.

semantics of memory operations for LLVM IR generated by GoLLVM written in K(currently a interpreter not well tested actually)

based on K v5.6.22(K semantic framework is a rolling release), see runtimeverification/k: K Framework Tools 5.0

Demo

cd src
kompile gollvm-semantics.k --enable-llvm-debug
krun ../test/preprocessed.min_level.ll --definition ./gollvm-semantics-kompiled --statistics > log # run the interpreter with statistics of rewriting steps

Use

1. use gollvm's -emit-llvm -S option to generate the llvm ir of golang source code.
2. use utils/IRpreprocess/IRpreprocess.go to preprocess the llvm ir to generate parse tree(The parser, i.e. the gollvm-syntax.k, is modified from K-LLVM which is previously built on older K whose version is possibly 3.6. It's not well tested.)
3. use krun to interpret the semantics of preprocessed llvm ir. it will give the memory state in the <mem></mem> cell of configuration and check whether the memory operation violate the escape analysis invariant. Static program analysis might be more suitable for this check.