parsing complete, precondition SMT generation needs a little attention

[pnwamk]

@simonjwinwood I've got parsing implemented for everything I think we'll need for all the demos.

The only two remaining issues I'm aware of are:

1) Well-typed SMT term generation

W.r.t. generating well-typed SMT terms from the parsed preconditions (i.e., BlockExprs), I still need to fix probably the following:

• how to properly emit a variable name with a known sort (I have a something that has the right type but is almost certainly using the wrong part of the API here)
• how to properly emit a well-typed application of a non-builtin, llvm-related (undefined, I assume) function applied to one or more argument, e.g. (fnstart reg13), (llvm foo), etc. Currently I just left these BlockExpr terms as "TODO"s basically.

At the moment I'm assuming we'll need to set up some initial environment with properly typed SMT function declarations (using define_fun?) that is a necessary parameter to the toSMT function, but I haven't dug enough to verify or fully understand that part yet.

2) Build issue for tests at the moment =\

As of 4abe3ba I'm getting a linker issue issue when it tries to build the test suite:

/home/vagrant/reopt-vcg/lean4/../local/bin/leanc -fPIC -ggdb3 `llvm-config-8 --cxxflags` -Wno-variadic-macros -Wno-gnu-zero-variadic-macro-arguments  -fexceptions -o build/reopt-vcg-unit-test build/deps/galois_stdlib/src/Galois/Data/Array.cpp build/deps/galois_stdlib/src/Galois/Data/Bitvec.cpp build/deps/galois_stdlib/src/Galois/Data/ByteArray.cpp build/deps/galois_stdlib/src/Galois/Data/RBMap.cpp build/deps/galois_stdlib/src/Galois/Data/SExp.cpp build/deps/galois_stdlib/src/Galois/Init/Int.cpp build/deps/galois_stdlib/src/Galois/Init/Io.cpp build/deps/galois_stdlib/src/Galois/Init/Nat.cpp build/deps/galois_stdlib/src/Galois/Init/Json.cpp build/deps/galois_stdlib/src/Galois/Category/Coe1.cpp build/deps/galois_stdlib/src/Galois/Data/ParserComb.cpp build/deps/smtlib/src/SMTLIB/Syntax.cpp build/deps/lean-llvm/src/Alignment.cpp build/deps/lean-llvm/src/AST.cpp build/deps/lean-llvm/src/PP.cpp build/deps/lean-llvm/src/DataLayout.cpp build/deps/lean-llvm/src/LLVMCodes.cpp build/deps/lean-llvm/src/LLVMFFI.cpp build/deps/lean-llvm/src/LLVMLib.cpp build/deps/lean-llvm/src/LLVMOutput.cpp build/deps/lean-llvm/src/Memory.cpp build/deps/lean-llvm/src/SimMonad.cpp build/deps/lean-llvm/src/Simulate.cpp build/deps/lean-llvm/src/Parser.cpp build/deps/lean-llvm/src/TypeContext.cpp build/deps/lean-llvm/src/Value.cpp build/deps/llvm-tablegen-support/lean/DecodeX86.cpp build/deps/x86_semantics/src/X86Semantics/BufferMap.cpp build/deps/x86_semantics/src/X86Semantics/Common.cpp build/deps/x86_semantics/src/X86Semantics/BackendAPI.cpp build/deps/x86_semantics/src/X86Semantics/ConcreteBackend.cpp build/deps/x86_semantics/src/X86Semantics/SymbolicBackend.cpp build/deps/x86_semantics/src/X86Semantics/Evaluator.cpp build/deps/x86_semantics/src/X86Semantics/Instructions.cpp build/deps/x86_semantics/src/X86Semantics/MachineMemory.cpp build/simulator/Elf.cpp build/simulator/Runelf.cpp build/simulator/Translate.cpp build/app/Annotations.cpp build/app/LoadLLVM.cpp build/app/ReoptVCG.cpp build/app/SMTParser.cpp build/app/Types.cpp build/app/VCGBackend.cpp build/app/VCGBlock.cpp build/tests/JsonRoundtrip.cpp build/tests/LoadElf.cpp build/tests/SExp.cpp build/deps/galois_stdlib/src/Galois/Init/io_runtime.o build/deps/lean-llvm/src/llvm_exports.o build/deps/llvm-tablegen-support/src/Metadata.o build/deps/llvm-tablegen-support/src/lean_support.o build/deps/llvm-tablegen-support/src/X86Disassembler.o build/tests/Main.cpp `llvm-config-8 --ldflags --system-libs --libs x86` -lstdc++ -lm
/usr/bin/clang-8
/usr/bin/clang-8
/tmp/Main-8fdb28.o: In function `_init_l_Test_tests___closed__13':
/home/vagrant/reopt-vcg/lean4/build/tests/Main.cpp:2611: undefined reference to `l_ReoptVCG_parseReachableBlockAnn___rarg___closed__10'
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Makefile:106: recipe for target 'build/reopt-vcg-unit-test' failed
make: *** [build/reopt-vcg-unit-test] Error 1

I haven't yet taken a chance to dive into this yet =\ Will report when I figure out more.

Update: the build seems to work on TravisCI... I just blew away and rebuilt it locally and I'm getting the same error... hmm...