From a19f618cb9e1dcabe750745c4d558135dacdda08 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Fri, 24 Jul 2026 00:17:18 -0400 Subject: [PATCH 01/11] refactor wip --- headers/gensym/branch.hpp | 2 + headers/gensym/external_imp.hpp | 2 + headers/gensym/external_pure.hpp | 2 + headers/gensym/smt_stp.hpp | 2 + src/main/scala/gensym/Driver.scala | 13 ++- src/main/scala/gensym/External.scala | 42 +++++----- .../gensym/{engines => }/ImpCPSEngine.scala | 0 .../gensym/{states => }/ImpSymExeState.scala | 0 src/main/scala/gensym/RunGenSym.scala | 12 +-- src/main/scala/gensym/engines/ImpEngine.scala | 2 + .../scala/gensym/engines/PureCPSEngine.scala | 2 + .../scala/gensym/engines/PureEngine.scala | 3 +- .../scala/gensym/states/SymExeState.scala | 3 +- src/test/scala/gensym/TestCases.scala | 13 +-- src/test/scala/gensym/TestExternal.scala | 2 + src/test/scala/gensym/TestGS.scala | 81 +------------------ 16 files changed, 70 insertions(+), 111 deletions(-) rename src/main/scala/gensym/{engines => }/ImpCPSEngine.scala (100%) rename src/main/scala/gensym/{states => }/ImpSymExeState.scala (100%) diff --git a/headers/gensym/branch.hpp b/headers/gensym/branch.hpp index 5cd689d01..68566533f 100644 --- a/headers/gensym/branch.hpp +++ b/headers/gensym/branch.hpp @@ -228,7 +228,9 @@ sym_exec_br_k(SS& ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond, std::function)> tf, std::function)> ff, std::function k) { + INFO("Before solver call"); auto [tbr_sat, fbr_sat] = check_branch(ss.get_PC(), t_cond); + INFO("After solver call"); if ((tbr_sat == solver_result::sat) && (fbr_sat == solver_result::sat)) { // both branches are sat cov().inc_path(1); diff --git a/headers/gensym/external_imp.hpp b/headers/gensym/external_imp.hpp index aa94d26dc..c3b11f594 100644 --- a/headers/gensym/external_imp.hpp +++ b/headers/gensym/external_imp.hpp @@ -636,6 +636,7 @@ inline T __syscall(SS& state, List& args, __Cont k) { errno = proj_IntV(state.at(state.error_loc(), 4)); switch (syscall_number) { +#if defined(__x86_64__) || defined(__i386__) case __NR_read: { int fd = get_int_arg(state, args.at(1)); ASSERT(0 == fd, "syscall read can only read from stdin, other fd should use pread64\n"); @@ -765,6 +766,7 @@ inline T __syscall(SS& state, List& args, __Cont k) { case __NR_openat: case __NR_futimesat: case __NR_newfstatat: +#endif default: ABORT("Unsupported system call"); break; diff --git a/headers/gensym/external_pure.hpp b/headers/gensym/external_pure.hpp index 236f69c0f..7c48a67be 100644 --- a/headers/gensym/external_pure.hpp +++ b/headers/gensym/external_pure.hpp @@ -429,6 +429,7 @@ inline T __syscall(SS& state, List& args, __Cont k) { SS res = state; switch (syscall_number) { +#if defined(__x86_64__) || defined(__i386__) case __NR_read: { int fd = get_int_arg(state, args.at(1)); ASSERT(0 == fd, "syscall read can only read from stdin, other fd should use pread64\n"); @@ -558,6 +559,7 @@ inline T __syscall(SS& state, List& args, __Cont k) { case __NR_openat: case __NR_futimesat: case __NR_newfstatat: +#endif default: ABORT("Unsupported Systemcall"); break; diff --git a/headers/gensym/smt_stp.hpp b/headers/gensym/smt_stp.hpp index 530f7c646..9866861f3 100644 --- a/headers/gensym/smt_stp.hpp +++ b/headers/gensym/smt_stp.hpp @@ -161,7 +161,9 @@ class CheckerSTP : public CachedChecker { solver_result check_model_internal() { ExprHandle fls = vc_falseExpr(vc); + INFO("Start solver call"); int retcode = vc_query(vc, fls.get()); + INFO("Finish solver call"); static solver_result mapping[4] = {sat, unsat, unknown, unknown}; return mapping[retcode]; } diff --git a/src/main/scala/gensym/Driver.scala b/src/main/scala/gensym/Driver.scala index 5283f0f3b..ee0744057 100644 --- a/src/main/scala/gensym/Driver.scala +++ b/src/main/scala/gensym/Driver.scala @@ -12,7 +12,6 @@ import gensym.llvm.parser.Parser._ import gensym.lmsx._ import gensym.utils.Utils.time import gensym.imp.Mut -import gensym.imp.ImpGSEngine import gensym.imp.ImpCPSGSEngine import gensym.Constants._ @@ -149,6 +148,7 @@ abstract class GenericGSDriver[A: Manifest, B: Manifest] } } +/* abstract class PureEngineDriver[A: Manifest, B: Manifest] extends GenericGSDriver[A, B] { q: EngineBase => override lazy val codegen: GenericGSCodeGen = new PureGSCodeGen { @@ -166,6 +166,7 @@ abstract class PureEngineDriver[A: Manifest, B: Manifest] extends GenericGSDrive } else g0 } } +*/ abstract class ImpureEngineDriver[A: Manifest, B: Manifest] extends GenericGSDriver[A, B] { q: EngineBase => @@ -237,6 +238,7 @@ abstract class ImpureEngineDriver[A: Manifest, B: Manifest] extends GenericGSDri } +/* // Using immer data structures for // 1) internal state/memory representation // 2) function call argument list @@ -270,6 +272,7 @@ abstract class ImpVecGSDriver[A: Manifest, B: Manifest]( setBlockMap(q.nodeBlockMap) } } +*/ // Generting CPS code with C++ containers for internal state/memory representation. // Function call argument lists and result lists still use immer containers. @@ -309,14 +312,17 @@ trait GenSym { } } +/* trait PureState { self: GenSym => override def extraFlags = "-D PURE_STATE" } +*/ trait ImpureState { self: GenSym => override def extraFlags = "-D IMPURE_STATE" } +/* class PureGS extends GenSym with PureState { val insName = "PureGS" def newInstance(m: Module, name: String, fname: String, config: Config): GenericGSDriver[Int, Unit] = @@ -329,7 +335,9 @@ class PureGS extends GenSym with PureState { } } } +*/ +/* class PureCPSGS extends GenSym with PureState { val insName = "PureCPSGS" def newInstance(m: Module, name: String, fname: String, config: Config): GenericGSDriver[Int, Unit] = @@ -340,7 +348,9 @@ class PureCPSGS extends GenSym with PureState { } } } +*/ +/* class ImpGS extends GenSym with ImpureState { val insName = "ImpGS" def newInstance(m: Module, name: String, fname: String, config: Config): GenericGSDriver[Int, Unit] = @@ -364,6 +374,7 @@ class ImpVecGS extends GenSym with ImpureState { } } } +*/ class ImpCPSGS extends GenSym with ImpureState { val insName = "ImpCPSGS" diff --git a/src/main/scala/gensym/External.scala b/src/main/scala/gensym/External.scala index c1606696a..8a8c2c465 100644 --- a/src/main/scala/gensym/External.scala +++ b/src/main/scala/gensym/External.scala @@ -19,8 +19,9 @@ import scala.collection.mutable.{Map => MutableMap, Set => MutableSet} // external/intrinsic functions with only slightly backend difference. // Can we generate them from our Scala DSL? +/* @virtualize -trait GenExternal extends SymExeDefs { +trait GenExternal extends ImpSymExeDefs { trait Auto def info(msg: String) = unchecked("INFO(\"[FS] \" << \"" + msg + "\")") def info_obj(p: Rep[_], l: String = ""): Rep[Unit] = unchecked("INFO(\"", if (l == "") "" else l + ": ", "\" << ", p, ")") @@ -88,7 +89,7 @@ trait GenExternal extends SymExeDefs { val canRead = ((mode & IntV(S_IRUSR, bw)) | (mode & IntV(S_IRGRP, bw)) | (mode & IntV(S_IROTH, bw))) val illegalRead = IntOp2.eq(canRead, IntV(0, bw)) - + val canWrite = ((mode & IntV(S_IWUSR, bw)) | (mode & IntV(S_IWGRP, bw)) | (mode & IntV(S_IWOTH, bw))) val illegalWrite = IntOp2.eq(canWrite, IntV(0, bw)) @@ -96,16 +97,16 @@ trait GenExternal extends SymExeDefs { } // returns a SymV that encodes each element in the list equals the element in the other list - def listEq(l1: Rep[List[Value]], l2: Rep[List[Value]]): Rep[Value] = + def listEq(l1: Rep[List[Value]], l2: Rep[List[Value]]): Rep[Value] = l1.zip(l2).foldLeft[Value](SymV.fromBool(true))((symv, pair) => IntOp2("and", symv, IntOp2.eq(pair._1, pair._2))) - // takes the current ss, fs, a symbolic file path, - // the continuation k takes the new ss, fs, and a concrete path, + // takes the current ss, fs, a symbolic file path, + // the continuation k takes the new ss, fs, and a concrete path, // with the assumption that the symbolic file path is resolved to the concrete path. // The continuation tk can be called multiple times // The continuation fk will be called only one time when the resolution failed. - def resolvePath[T: Manifest](ss: Rep[SS], fs: Rep[FS], symPath: Rep[List[Value]], + def resolvePath[T: Manifest](ss: Rep[SS], fs: Rep[FS], symPath: Rep[List[Value]], tk: (Rep[SS], Rep[FS], Rep[String]) => Rep[T], fk: (Rep[SS], Rep[FS]) => Rep[T]): Rep[T] = { if (symPath.foldLeft[Boolean](true)((b, v) => b && v.isConc)) { info("symPath is concrete") @@ -140,7 +141,7 @@ trait GenExternal extends SymExeDefs { // not match stop[T](ss) }) - acc + acc }) } else { fk(ss, fs) @@ -151,7 +152,7 @@ trait GenExternal extends SymExeDefs { } } - /* + /* * int open(const char *pathname, int flags); * int open(const char *pathname, int flags, mode_t mode); */ @@ -208,14 +209,14 @@ trait GenExternal extends SymExeDefs { k(ss, IntV(0, 32)) } - /* + /* * int close(int fd); */ def close[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { unchecked("INFO(\"close syscall\")") val fd: Rep[Fd] = args(0).int.toInt unchecked("INFO(\"fd: \" << ", fd, ")") - if (!fs.hasStream(fd)) + if (!fs.hasStream(fd)) k(ss.setErrorLoc(flag("EBADF")), fs, IntV(-1, 32)) else { val strm = fs.getStream(fd) @@ -240,7 +241,7 @@ trait GenExternal extends SymExeDefs { info_ptrval(loc, "loc") val count: Rep[Int] = args(2).int.toInt info_obj(count, "count") - if (!fs.hasStream(fd)) + if (!fs.hasStream(fd)) k(ss.setErrorLoc(flag("EBADF")), fs, IntV(-1, 64)) else { val strm = fs.getStream(fd) @@ -252,7 +253,7 @@ trait GenExternal extends SymExeDefs { } } - /* + /* * ssize_t write(int fd, const void *buf, size_t count); */ def write[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { @@ -284,7 +285,7 @@ trait GenExternal extends SymExeDefs { val fd: Rep[Fd] = args(0).int.toInt val o: Rep[Long] = args(1).int val w: Rep[Int] = args(2).int.toInt - if (!fs.hasStream(fd)) + if (!fs.hasStream(fd)) k(ss.setErrorLoc(flag("EBADF")), fs, IntV(-1, 64)) else { val strm = fs.getStream(fd) @@ -294,7 +295,7 @@ trait GenExternal extends SymExeDefs { else if (w == SEEK_END) strm.seekEnd(o) else -1L } - if (pos == -1L) + if (pos == -1L) k(ss.setErrorLoc(flag("EINVAL")), fs, IntV(-1, 64)) else { fs.setStream(fd, strm) @@ -332,7 +333,7 @@ trait GenExternal extends SymExeDefs { unchecked("INFO(\"fstat syscall\")") val fd: Rep[Fd] = args(0).int.toInt val buf: Rep[Value] = args(1) - if (!fs.hasStream(fd)) + if (!fs.hasStream(fd)) k(ss.setErrorLoc(flag("EBADF")), fs, IntV(-1, 32)) else { val stat = fs.getStream(fd).file.stat @@ -508,10 +509,10 @@ trait GenExternal extends SymExeDefs { val bw = Constants.BYTE_SIZE * StructCalc()(null).getFieldOffsetSize(StatType.types, getFieldIdx(statFields, "st_mode"))._2 val ischr: Rep[Value] = IntOp2.eq(mode & IntV(cmacro[Int]("S_IFMT"), bw), IntV(cmacro[Int]("S_IFCHR"), bw)) brFs(ss, fs, ischr, - (ss, fs) => { + (ss, fs) => { info("is character") k(ss, fs, IntV(0, 32)) - }, + }, (ss, fs) => { info("is not a character, return error") k(ss.setErrorLoc(flag("ENOTTY")), fs, IntV(-1, 32)) @@ -572,7 +573,7 @@ trait GenExternal extends SymExeDefs { f } - def _errno_location[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = + def _errno_location[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = k(ss, ss.getErrorLoc) def _has_file_type(f: Rep[File], mask: Rep[Int]): Rep[Value] = { @@ -621,6 +622,7 @@ trait GenExternal extends SymExeDefs { res } } +*/ @virtualize trait ExternalUtil { self: BasicDefs with ValueDefs with SAIOps => @@ -648,6 +650,7 @@ trait ExternalUtil { self: BasicDefs with ValueDefs with SAIOps => } } +/* class ExternalGSDriver(folder: String = "./headers/gensym") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q => import java.io.{File, PrintStream} @@ -731,10 +734,13 @@ class ExternalGSDriver(folder: String = "./headers/gensym") extends SAISnippet[I () } } +*/ +/* object GenerateExternal { def main(args: Array[String]): Unit = { val code = new ExternalGSDriver code.genHeader } } +*/ diff --git a/src/main/scala/gensym/engines/ImpCPSEngine.scala b/src/main/scala/gensym/ImpCPSEngine.scala similarity index 100% rename from src/main/scala/gensym/engines/ImpCPSEngine.scala rename to src/main/scala/gensym/ImpCPSEngine.scala diff --git a/src/main/scala/gensym/states/ImpSymExeState.scala b/src/main/scala/gensym/ImpSymExeState.scala similarity index 100% rename from src/main/scala/gensym/states/ImpSymExeState.scala rename to src/main/scala/gensym/ImpSymExeState.scala diff --git a/src/main/scala/gensym/RunGenSym.scala b/src/main/scala/gensym/RunGenSym.scala index 93a2a0875..9c339053d 100644 --- a/src/main/scala/gensym/RunGenSym.scala +++ b/src/main/scala/gensym/RunGenSym.scala @@ -13,8 +13,8 @@ object SwitchType extends Enumeration { import SwitchType._ case class Config( - nSym: Int, - useArgv: Boolean, + nSym: Int, + useArgv: Boolean, mainFileOpt: String, var opt: Boolean = true, var iteSelect: Boolean = true, @@ -72,9 +72,8 @@ object RunGenSym { |--randomUninit - model uninitialized variables as a random value instead of a symbolic one |--engine= - compiler/backend variant (default=ImpCPS) | =ImpCPS - generate code in CPS with impure data structures, can run in parallel - | =ImpDirect - generate code in direct-style with impure data structures, cannot run in parallel - | =PureCPS - generate code in CPS with pure data structures, can run in parallel - | =PureDirect - generate code in direct-style with pure data structures, cannot run in parallel + | =app + | =lib |--main-opt= - g++ optimization level when compiling the main file containing the initial heap object |--emit-block-id-map - emit a map from block names to id in common.h |--emit-var-id-map - emit a map from variable names to id in common.h @@ -117,9 +116,6 @@ object RunGenSym { val gensym = engine match { case "ImpCPS" => new ImpCPSGS - case "ImpDirect" => new ImpGS - case "PureCPS" => new PureCPSGS - case "PureDirect" => new PureGS case "lib" => new ImpCPSGS_lib case "app" => new ImpCPSGS_app } diff --git a/src/main/scala/gensym/engines/ImpEngine.scala b/src/main/scala/gensym/engines/ImpEngine.scala index ecef69dd5..607c75ad3 100644 --- a/src/main/scala/gensym/engines/ImpEngine.scala +++ b/src/main/scala/gensym/engines/ImpEngine.scala @@ -1,5 +1,6 @@ package gensym.imp +/* import lms.core._ import lms.core.Backend._ import lms.core.virtualize @@ -407,3 +408,4 @@ trait ImpGSEngine extends ImpSymExeDefs with EngineBase { fv[Ref](ss, args) } } +*/ \ No newline at end of file diff --git a/src/main/scala/gensym/engines/PureCPSEngine.scala b/src/main/scala/gensym/engines/PureCPSEngine.scala index d825dcacf..1a20a8004 100644 --- a/src/main/scala/gensym/engines/PureCPSEngine.scala +++ b/src/main/scala/gensym/engines/PureCPSEngine.scala @@ -1,5 +1,6 @@ package gensym +/* import lms.core._ import lms.core.Backend._ import lms.core.virtualize @@ -389,3 +390,4 @@ trait PureCPSGSEngine extends SymExeDefs with EngineBase { fv[Id](ss.push.updateArg.initErrorLoc, args, k) } } +*/ \ No newline at end of file diff --git a/src/main/scala/gensym/engines/PureEngine.scala b/src/main/scala/gensym/engines/PureEngine.scala index 334e51771..eb1872bca 100644 --- a/src/main/scala/gensym/engines/PureEngine.scala +++ b/src/main/scala/gensym/engines/PureEngine.scala @@ -1,5 +1,5 @@ package gensym - +/* import lms.core._ import lms.core.Backend._ import lms.core.virtualize @@ -501,3 +501,4 @@ trait GSEngine extends StagedNondet with SymExeDefs with EngineBase { reify[Value](initState(heap0))(comp) } } +*/ \ No newline at end of file diff --git a/src/main/scala/gensym/states/SymExeState.scala b/src/main/scala/gensym/states/SymExeState.scala index aee5480f8..af6e331e0 100644 --- a/src/main/scala/gensym/states/SymExeState.scala +++ b/src/main/scala/gensym/states/SymExeState.scala @@ -1,5 +1,5 @@ package gensym - +/* import lms.core._ import lms.core.Backend._ import lms.core.virtualize @@ -191,3 +191,4 @@ trait SymExeDefs extends SAIOps with StagedNondet with BasicDefs with ValueDefs def writebackPointerArg(res: Rep[Any], addr: Rep[Value], x: Rep[Ptr[Char]]): Comp[E, Rep[Unit]] = updateState(_.writebackPointerArg(res, addr, x)) } +*/ \ No newline at end of file diff --git a/src/test/scala/gensym/TestCases.scala b/src/test/scala/gensym/TestCases.scala index 93e611f29..02c034db3 100644 --- a/src/test/scala/gensym/TestCases.scala +++ b/src/test/scala/gensym/TestCases.scala @@ -58,7 +58,8 @@ object TestCases { TestPrg(switchTestConc, "switchConcreteTest", "@main", noArg, noOpt, nPath(1)), TestPrg(trunc, "truncTest", "@main", noArg, noOpt, nPath(1)), TestPrg(floatArith, "floatArithTest", "@main", noArg, noOpt, nPath(1)), - TestPrg(floatFp80, "floatFp80Test", "@main", noArg, noOpt, nPath(1)), + // FIXME: ANTLR/parser fails on this file + //TestPrg(floatFp80, "floatFp80Test", "@main", noArg, noOpt, nPath(1)), TestPrg(arrayAccess, "arrayAccTest", "@main", noArg, noOpt, nPath(1)), TestPrg(arrayAccessLocal, "arrayAccLocalTest", "@main", noArg, noOpt, nPath(1)), @@ -155,10 +156,12 @@ object TestCases { TestPrg(chmodTest, "chmodTest", "@main", noArg, noOpt, nPath(2)++status(0)), TestPrg(stdinTest, "stdinTest", "@main", noArg, "--sym-stdin 10", nPath(2)++status(0)), TestPrg(ioctlTest, "ioctlTest", "@main", noArg, "--add-sym-file A", nPath(1)++status(0)), - TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0)), - TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0)), - TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0)), - TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)), + + // FIXME: temporally commented klee-related tests because it only works for x86 + //TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0)), + //TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0)), + //TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0)), + //TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)), ) lazy val coreutils: List[TestPrg] = List( diff --git a/src/test/scala/gensym/TestExternal.scala b/src/test/scala/gensym/TestExternal.scala index c29114360..8cd328118 100644 --- a/src/test/scala/gensym/TestExternal.scala +++ b/src/test/scala/gensym/TestExternal.scala @@ -18,6 +18,7 @@ import scala.collection.mutable.{Map => MutableMap, Set => MutableSet} import sys.process._ import org.scalatest.FunSuite +/* class ExternalTestDriver(folder: String = "./headers/test") extends SAISnippet[Int, Unit] with SAIOps with GenExternal with ExternalUtil { q => import java.io.{File, PrintStream} @@ -447,3 +448,4 @@ class TestGenExternal extends FunSuite { testUnit("./headers/test", "external_test") } +*/ \ No newline at end of file diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index bbe6423ad..f34ed912a 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -100,34 +100,10 @@ abstract class TestGS extends FunSuite { def testGS(gs: GenSym, tests: List[TestPrg]): Unit = tests.foreach(testGS(gs, _)) } -class TestPureGS extends TestGS { - testGS(new PureGS, TestCases.all ++ filesys ++ varArg) -} - -class TestPureCPSGS extends TestGS { - val gs = new PureCPSGS - - // Note: the following test cases need to use `--thread=n` to enable random path selection strategy. - // They also relies on block-level path switching to increase randomness, which currently has only - // been implemented in PureCPS engine. - testGS(gs, TestPrg(unboundedLoop, "unboundedLoop", "@main", noArg, "--thread=2 --search=random-path --output-tests-cov-new --timeout=2 --solver=z3", minTest(1))) - testGS(gs, TestPrg(unboundedLoop, "unboundedLoopMT", "@main", noArg, "--thread=2 --timeout=2 --solver=z3", minTest(1))) - testGS(gs, TestPrg(data_structures_set_multi_proc_ground_1, "testCompArraySet1", "@main", noArg, "--thread=2 --search=random-path --solver=z3", status(255))) - testGS(gs, TestPrg(standard_allDiff2_ground, "stdAllDiff2Ground", "@main", noArg, "--thread=2 --output-tests-cov-new --solver=z3", status(255))) - testGS(gs, TestPrg(standard_copy9_ground, "stdCopy9", "@main", noArg, "--thread=2 --search=random-path --solver=z3", status(255))) - - // Timeout - //testGS(gs, TestPrg(sorting_selection_ground_1, "testCompSelectionSort", "@main", noArg, "--thread=2 --timeout=2 --solver=z3", minTest(1))) -} - -class TestImpGS extends TestGS { - testGS(new ImpGS, TestCases.all ++ filesys ++ varArg) -} - class TestImpCPSGS extends TestGS { val gs = new ImpCPSGS testGS(gs, TestCases.all ++ filesys ++ varArg) - // Note: compile-time switch merge is only implement for ImpCPS so far + // Note: compile-time switch merge is only implemented for ImpCPS so far testGS(gs, TestPrg(switchMergeSym, "switchMergeTest", "@main", noArg, noOpt, nPath(3))) // Test uninitialized ptr access, only enabled for CPS+thread pool version @@ -154,7 +130,8 @@ class TestImpCPSGS extends TestGS { class TestImpCPSGS_Z3 extends TestGS { val gs = new ImpCPSGS - val cases = (TestCases.all ++ filesys ++ varArg).map { t => + //val cases = (TestCases.all ++ filesys ++ varArg).map { t => + val cases = (TestCases.all).map { t => t.copy(runOpt = t.runOpt ++ Seq("--solver=z3")) } testGS(gs, cases) @@ -205,54 +182,4 @@ class Playground extends TestGS { import gensym.llvm.parser.Parser._ Global.config.enableOpt val gs = new ImpCPSGS - //testGS(gs, TestPrg(unboundedLoop, "unboundedLoop", "@main", noArg, "--thread=2 --search=random-path --output-tests-cov-new --timeout=2 --solver=z3", minTest(1))) - //testGS(gs, TestPrg(unboundedLoop, "unboundedLoopMT", "@main", noArg, "--thread=2 --timeout=2 --solver=z3", minTest(1))) - - //testGS(gs, TestPrg(mergesort, "mergeSortTest1", "@main", noArg, noOpt, nPath(720))) - //testGS(new PureCPSGS, TestPrg(arrayFlow, "arrayFlow", "@main", noArg, noOpt, nPath(15)++status(0))) - //testGS(new ImpCPSGS, TestPrg(arrayFlow, "arrayFlow2", "@main", noArg, noOpt, nPath(15)++status(0))) - - //testGS(gs, TestPrg(switchMergeSym, "switchMergeTest", "@main", noArg, noOpt, nPath(3))) - //testGS(gs, TestPrg(switchTestSym, "switchSymTest", "@main", noArg, noOpt, nPath(5))) - //testGS(gs, TestPrg(switchTestConc, "switchConcreteTest", "@main", noArg, noOpt, nPath(1))) - //testGS(gs, TestPrg(maze, "mazeTest", "@main", noArg, noOpt, nPath(309))) - - //testGS(new PureCPSGS, TestPrg(mergesort, "mergeSortTest2", "@main", noArg, noOpt, nPath(720))) - //testGS(new ImpGS, TestPrg(mergesort, "mergeSortTest3", "@main", noArg, noOpt, nPath(720))) - //testGS(gs, TestPrg(knapsack, "knapsackTest", "@main", noArg, noOpt, nPath(1666))) - //val echo_linked = parseFile("/home/kraks/research/gs/coreutils/obj-llvm/playground/echo_gs.ll") - //testGS(gs, TestPrg(echo_linked, "echo_linked_posix", "@main", - // noMainFileOpt, Seq("--cons-indep", "--argv=./echo.bc --sym-stdout --sym-arg 8"), nPath(4971)++status(0))) - - //testGS(gs, TestPrg(mp1048576, "mp1mTest", "@f", symArg(20), "--solver=disable", nPath(1048576))) - //testGS(gs, TestPrg(quicksort, "quickSortTest", "@main", noArg, noOpt, nPath(120))) - //testGS(gs, TestPrg(printfTest, "printfTest", "@main", noArg, noOpt, nPath(1)++status(0))) - //testGS(gs, TestPrg(selectTestSym, "selectTest", "@main", noArg, noOpt, nPath(1))) - //testGS(new ImpCPSGS, List(TestPrg(base32_linked, "base32_linked_posix", "@main", noMainFileOpt, Seq("--cons-indep","--argv=./true.bc --sym-stdout --sym-stdin 2 --sym-arg 1 -sym-files 2 10"), nPath(4971)++status(0)))) - //testGS(new PureCPSGS, TestPrg(unboundedLoop, "unboundedLoop", "@main", noArg, "--thread=2 --timeout=2 --solver=z3", minTest(1))) - // testGS(new ImpCPSGS, TestPrg(standard_minInArray_ground_1, "standard_minInArray_ground_1", "@main", noArg, noOpt, status(255))) - - //testGS(new PureCPSGS, TestPrg(mp1048576, "mp1mTest_CPS", "@f", symArg(20), "--disable-solver", nPath(1048576))) - - //testGS(new PureGS, List(TestPrg(echo_linked, "echo_linked_posix", "@main", noMainFileOpt, Seq("--cons-indep","--argv=./true.bc --sym-stdout --sym-arg 8"), nPath(4971)++status(0)))) - //testGS(new ImpCPSGS, List(TestPrg(cat_linked, "cat_linked_posix", "@main", noMainFileOpt, Seq("--cons-indep","--argv=./true.bc --sym-stdout --sym-stdin 2 --sym-arg 1 -sym-files 2 10"), nPath(256)++status(0)))) - //testGS(new ImpCPSGS, List(TestPrg(echo_linked, "echo_linked_posix", "@main", noMainFileOpt, Seq("--cons-indep","--argv=./true.bc --sym-stdout --sym-arg 8"), nPath(4971)++status(0)))) - //testGS(new PureGS, List(TestPrg(echo_gs_linked, "echo_gs_linked", "@main", noMainFileOpt, Seq("--cons-indep","--argv=./true.bc #{3}"), nPath(26)++status(0)))) - //testGS(gs, TestPrg(mp1048576, "mp1mTest", "@f", symArg(20), "--disable-solver", nPath(1048576))) - //testGS(gs, TestPrg(parseFile("benchmarks/demo-benchmarks/nqueen_opt.ll"), "nQueensOpt", "@main", noArg, noOpt, nPath(1363))) - //testGS(new PureGS, List(TestPrg(true_linked, "true_linked", "@main", useArgv, "--argv=./true.bc --sym-arg 3", nPath(16)++status(0)))) - //testGS(new PureGS, List(TestPrg(false_linked, "false_linked", "@main", useArgv, "--argv=./false.bc --sym-arg 3", nPath(16)++status(0)))) - //testGS(gs, TestPrg(bubbleSort2Ground, "bubbleSort2Ground", "@main", 0, noOpt, status(255))) - //testGS(gs, TestPrg(bubbleSortGround2, "bubbleSortGround2", "@main", 0, noOpt, status(255))) - - // Timeout: - //testGS(gs, TestPrg(copysome1_2, "copysome1_2", "@main", noArg, noOpt, status(255))) - //testGS(gs, TestPrg(copysome2_2, "copysome2_2", "@main", noArg, noOpt, status(255))) - //testGS(gs, TestPrg(sorting_bubblesort_2_ground, "bubbleSort2Ground", "@main", noArg, noOpt, status(255))) - //testGS(gs, TestPrg(sorting_bubblesort_ground_2, "bubbleSortGround2", "@main", 0, noOpt, status(255))) - //testGS(gs, TestPrg(copysome1_2, "copysome1_2", "@main", noArg, noOpt, status(255))) - //testGS(gs, TestPrg(copysome2_2, "copysome2_2", "@main", noArg, noOpt, status(255))) - //testGS(gs, TestPrg(sorting_bubblesort_2_ground, "bubbleSort2Ground", "@main", noArg, noOpt, status(255))) - //testGS(gs, TestPrg(sorting_bubblesort_ground_2, "bubbleSortGround2", "@main", 0, noOpt, status(255))) -} - +} \ No newline at end of file From 1ed8a5ac4cc8bd671bb512b3ad9711c63463fe7e Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 00:11:03 -0400 Subject: [PATCH 02/11] disable test --- .github/workflows/scala.yml | 4 ++-- src/test/scala/gensym/TestGS.scala | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml index 732161e42..7483171c3 100644 --- a/.github/workflows/scala.yml +++ b/.github/workflows/scala.yml @@ -71,8 +71,8 @@ jobs: run: | cd third-party/wasmfx-tools cargo build --release - - name: Generate models - run: sbt 'runMain gensym.GenerateExternal' + #- name: Generate models + # run: sbt 'runMain gensym.GenerateExternal' - name: Run tests run: | sbt 'testOnly gensym.TestImpCPSGS' diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index f34ed912a..67731c915 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -182,4 +182,7 @@ class Playground extends TestGS { import gensym.llvm.parser.Parser._ Global.config.enableOpt val gs = new ImpCPSGS + + val rtOpt = "--thread=1 --solver=z3" + testGS(gs, TestPrg(branch, "branch1", "@f", symArg(2), rtOpt, nPath(4))) } \ No newline at end of file From 23fd8d8253c17cdadf37d2deba97c818ec5f10c1 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 01:28:48 -0400 Subject: [PATCH 03/11] refactor to separately compiled library (by codex) --- .gitignore | 1 + README.md | 20 ++ headers/gensym/auxiliary.hpp | 18 +- headers/gensym/external_imp.hpp | 6 +- headers/gensym/libcpolyfill.hpp | 13 +- headers/gensym/runtime.hpp | 271 ++++++++++++++++++++++ headers/gensym/value_ops.hpp | 6 +- runtime/Makefile | 29 +++ runtime/runtime.cpp | 310 ++++++++++++++++++++++++++ src/main/scala/gensym/Codegen.scala | 90 ++++++++ src/main/scala/gensym/Driver.scala | 107 +++++++-- src/main/scala/gensym/IRUtils.scala | 4 +- src/test/scala/gensym/TestCases.scala | 10 + src/test/scala/gensym/TestGS.scala | 47 +++- 14 files changed, 880 insertions(+), 52 deletions(-) create mode 100644 headers/gensym/runtime.hpp create mode 100644 runtime/Makefile create mode 100644 runtime/runtime.cpp diff --git a/.gitignore b/.gitignore index 160554632..4114ea2f1 100644 --- a/.gitignore +++ b/.gitignore @@ -12,6 +12,7 @@ .vscode .bsp target +runtime/build/ klee-out-* gs_gen output diff --git a/README.md b/README.md index 0ba3254cb..f168077eb 100644 --- a/README.md +++ b/README.md @@ -127,6 +127,26 @@ This steps generates the executable `branch`, then running the executable file p ``` The generated executable file also has several runtime options. + +### Precompiled native runtime + +The active LLVM ImpCPS backend links generated programs with +`runtime/build/libgensym_runtime.a`. The public generated-code interface is the +standard-library-only header `headers/gensym/runtime.hpp`; Immer, solver details, +the filesystem model, scheduler, and monitor implementation are compiled once +inside the runtime archive. + +Build the runtime explicitly with: + +```sh +make -C runtime +``` + +Generated Makefiles also invoke this incremental build automatically. If the +runtime sources and private headers are unchanged, subsequent generated programs +reuse the existing archive without recompiling it. `make clean` in a generated +program removes only that program. To force a runtime rebuild, run +`make -C runtime clean all` from the repository root. For most of users, it suffices to use the default options. However if you would like to play with it, you can check those options by `./branch --help`. diff --git a/headers/gensym/auxiliary.hpp b/headers/gensym/auxiliary.hpp index 1eb25bcc3..427c3c93d 100644 --- a/headers/gensym/auxiliary.hpp +++ b/headers/gensym/auxiliary.hpp @@ -22,15 +22,15 @@ # define ASSERT(condition, message) do { } while (false) #endif -#ifdef DEBUG -# define INFO(message) \ - do { \ +inline bool runtime_debug = false; +#undef INFO +#define INFO(message) \ + do { \ + if (runtime_debug) { \ std::cout << "[Info] " << __FILE__ << " line " << __LINE__ \ << ": " << message << std::endl; \ - } while (false) -#else -# define INFO(message) do { } while (false) -#endif + } \ + } while (false) #define MAX(a, b) ((a) > (b)) ? (a) : (b) #define MIN(a, b) ((a) < (b)) ? (a) : (b) @@ -129,9 +129,7 @@ inline uint32_t rand_uint32() { inline int rand_int(int ub) { int r = (rng32() % ub) + 1; // [1, ub] -#ifdef DEBUG - std::cout << "Generate a rand number: " << r << std::endl; -#endif + if (runtime_debug) std::cout << "Generate a rand number: " << r << std::endl; return r; } diff --git a/headers/gensym/external_imp.hpp b/headers/gensym/external_imp.hpp index c3b11f594..2f93a5658 100644 --- a/headers/gensym/external_imp.hpp +++ b/headers/gensym/external_imp.hpp @@ -572,7 +572,7 @@ inline void copy_native2state(SS& state, PtrVal ptr, char* buf, int size) { ASSERT(bytes_num > 0, "Invalid bytes"); // Do not over-write symbolic variable if (old_val->to_SymV()) { - #ifdef GENSYM_SYMBOLIC_UNINIT + if (symbolic_uninit) { // add constraint on symbolic variable to be equal to concrete for (int j = 0; j < bytes_num; j++) { auto eq_constraint = int_op_2(iOP::op_eq, state.at_simpl(ptr + i), make_IntV(buf[i], 8)); @@ -580,9 +580,9 @@ inline void copy_native2state(SS& state, PtrVal ptr, char* buf, int size) { i++; if (i >= size) break; } - #else + } else { i += bytes_num; - #endif + } } else { for (int j = 0; j < bytes_num; j++) { state.update_simpl(ptr + i, make_IntV(buf[i], 8)); diff --git a/headers/gensym/libcpolyfill.hpp b/headers/gensym/libcpolyfill.hpp index 11271c2ab..5380c8b7f 100644 --- a/headers/gensym/libcpolyfill.hpp +++ b/headers/gensym/libcpolyfill.hpp @@ -1,14 +1,15 @@ // prepare necessary declarations and definitions for library mode compilation -#include -std::monostate app_main(SS&, immer::flex_vector, std::function); -std::monostate gs_main(SS&, immer::flex_vector, std::function); -inline std::monostate gs_dummy(SS&, immer::flex_vector, std::function) { +#include +using namespace gensym::runtime::v1; +std::monostate app_main(SS&, Args, Cont); +std::monostate gs_main(SS&, Args, Cont); +inline std::monostate gs_dummy(SS&, Args, Cont) { std::cout << "Warning: invoking gs_dummy, some path is not continued!\n"; return std::monostate{}; } -inline std::monostate start_gs_main(SS& state, immer::flex_vector args, std::function cont) { +inline std::monostate start_gs_main(SS& state, Args args, Cont cont) { if (can_par_tp()) { - tp.add_task(1, [=] () mutable { return gs_main(state, args, cont); }); + add_task(1, [=] () mutable { return gs_main(state, args, cont); }); return std::monostate{}; } return gs_main(state, args, cont); diff --git a/headers/gensym/runtime.hpp b/headers/gensym/runtime.hpp new file mode 100644 index 000000000..dfb8476c2 --- /dev/null +++ b/headers/gensym/runtime.hpp @@ -0,0 +1,271 @@ +#ifndef GENSYM_RUNTIME_HPP +#define GENSYM_RUNTIME_HPP + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace gensym::runtime::v1 { + +inline constexpr std::uint32_t api_version = 1; + +enum class iOP { + op_add, op_sub, op_mul, op_sdiv, op_udiv, + op_eq, op_uge, op_ugt, op_ule, op_ult, + op_sge, op_sgt, op_sle, op_slt, op_neq, + op_shl, op_lshr, op_ashr, op_and, op_or, op_xor, + op_urem, op_srem, op_neg, op_sext, op_zext, op_trunc, + op_concat, op_extract, op_ite, op_bvnot, const_true, const_false +}; + +enum class fOP { + op_fadd, op_fsub, op_fmul, op_fdiv, + op_oeq, op_ogt, op_oge, op_olt, op_ole, op_one, op_ord, + op_ueq, op_ugt, op_uge, op_ult, op_ule, op_une, op_uno, + const_false, const_true +}; + +struct LocV { enum Kind { kStack, kHeap, kNative }; }; + +class Value; +class State; +class PathCondition; + +using PtrVal = Value; +using SS = State; +using PC = PathCondition; +using String = std::string; +using Addr = std::uint32_t; +using BlockLabel = int; +using IntData = std::int64_t; +using UIntData = std::uint64_t; +using Args = std::vector; +using Ids = std::vector; +using Cont = std::function; +using CPSFunc = std::monostate (*)(State&, Args, Cont); +using Block = std::function; + +class Value { + void* impl_ = nullptr; + explicit Value(void* impl) noexcept : impl_(impl) {} + friend struct Bridge; +public: + Value() noexcept = default; + Value(std::nullptr_t) noexcept {} + Value& operator=(std::nullptr_t) noexcept { impl_ = nullptr; return *this; } + explicit operator bool() const noexcept { return impl_ != nullptr; } + bool operator==(std::nullptr_t) const noexcept { return impl_ == nullptr; } + bool operator!=(std::nullptr_t) const noexcept { return impl_ != nullptr; } + Value* operator->() noexcept { return this; } + const Value* operator->() const noexcept { return this; } + Value& operator*() noexcept { return *this; } + const Value& operator*() const noexcept { return *this; } + + bool is_conc() const; + std::size_t get_bw() const; + Args to_bytes() const; + Args to_bytes_shadow() const; + static Value from_bytes(const Args&); + static Value from_bytes_shadow(const Args&); +}; + +std::ostream& operator<<(std::ostream&, const Value&); + +class PathCondition { + void* impl_ = nullptr; + explicit PathCondition(void* impl) noexcept : impl_(impl) {} + friend struct Bridge; + friend class State; +public: + PathCondition(); + PathCondition(const PathCondition&); + PathCondition(PathCondition&&) noexcept; + PathCondition& operator=(const PathCondition&); + PathCondition& operator=(PathCondition&&) noexcept; + ~PathCondition(); + PathCondition& add(Value); +}; + +class State { + void* impl_ = nullptr; + bool owned_ = false; + State(void* impl, bool owned) noexcept : impl_(impl), owned_(owned) {} + friend struct Bridge; +public: + State(); + State(const State&); + State(State&&) noexcept; + State& operator=(const State&); + State& operator=(State&&) noexcept; + ~State(); + + State fork(); + State copy() const; + std::uint64_t get_ssid() const; + int incoming_block() const; + Value env_lookup(int); + std::size_t heap_size() const; + std::size_t stack_size() const; + Value at(Value, std::size_t); + Value at_struct(Value, int); + Args at_seq(Value, int); + Value heap_lookup(std::size_t); + State& alloc_stack(std::size_t); + State& alloc_heap(std::size_t); + State& update(Value, Value); + State& update(Value, Value, std::size_t); + State& update_seq(Value, const Args&); + State& push(); + State& push(Cont); + Cont pop(std::size_t); + State& assign(int, Value); + State& assign_seq(const Ids&, const Args&); + State& heap_append(const Args&); + State& add_PC(Value); + PathCondition get_PC() const; + PathCondition copy_PC() const; + State& add_incoming_block(int); + State& cover_block(int); + State& init_arg(); + State& init_error_loc(); + Value error_loc(); +}; + +struct ProgramConfig { + std::size_t block_count = 0; + std::vector> branch_arity; + bool symbolic_uninitialized = false; + bool debug = false; +}; + +class Coverage { +public: + void set_num_blocks(std::size_t); + void extend_blocks(std::size_t, const std::vector>&); + void inc_block(std::size_t); + void inc_branch(std::size_t, std::size_t); + void inc_path(std::size_t); + void inc_inst(std::size_t); + void start_monitor(); + void print_block_cov(); + void print_time(); + void print_path_cov(); +}; + +Coverage& cov(); +bool debug_enabled(); +void configure(const ProgramConfig&); +void prelude(int argc, char** argv, const ProgramConfig&); +void epilogue(); +int runtime_exit_code(); +bool can_par_tp(); +void add_task(std::uint64_t, std::function); + +State make_initial_state(const Args& heap = {}); +extern Value g_argc; +extern Value g_argv; +Value make_IntV(std::int64_t, std::size_t = 32, bool = true); +Value make_FloatV(double, std::size_t); +Value make_FloatV_fp80(const std::vector&); +Value make_LocV(std::uint32_t, LocV::Kind, std::size_t, std::size_t = 0); +Value make_LocV_null(); +Value make_SymV(const std::string&, std::size_t); +Value make_SymLocV(std::uint32_t, LocV::Kind, std::size_t, Value); +Value make_ShadowV(); +Value make_ShadowV(std::int8_t); +std::int64_t proj_IntV(Value); +Value int_op_1(iOP, Value); +Value int_op_2(iOP, Value, Value); +Value int_op_3(iOP, Value, Value, Value); +Value float_op_2(fOP, Value, Value); +Value bv_sext(Value, std::size_t); +Value bv_zext(Value, std::size_t); +Value trunc(Value, int, int); +Value ite(Value, Value, Value); +Value ptr_add(Value, Value); + +Value make_CPSFunV(CPSFunc); +std::monostate cps_apply(Value, State, Args, Cont); +std::monostate cont_apply(Cont, State&, Value); +std::monostate sym_exec_br_k(State&, unsigned, Value, Value, Block, Block, Cont); +std::vector> array_lookup(State&, Value, Value, std::size_t); +std::monostate array_lookup_k(State&, Value, Value, std::size_t, Cont); +bool check_pc(PathCondition); +void check_pc_to_file(const State&); + +std::int64_t get_int_arg(State&, Value); +double get_float_arg(State&, Value); +void* get_pointer_arg(State&, Value); +void writeback_pointer_arg(State&, Value, void*); + +#define GENSYM_RUNTIME_EXTERNAL(name) \ + std::monostate name(State&, Args, Cont) +GENSYM_RUNTIME_EXTERNAL(stop); +GENSYM_RUNTIME_EXTERNAL(noop); +GENSYM_RUNTIME_EXTERNAL(_exit); +GENSYM_RUNTIME_EXTERNAL(exit); +GENSYM_RUNTIME_EXTERNAL(abort); +GENSYM_RUNTIME_EXTERNAL(sym_exit); +GENSYM_RUNTIME_EXTERNAL(print_string); +GENSYM_RUNTIME_EXTERNAL(sym_print); +GENSYM_RUNTIME_EXTERNAL(gs_assert); +GENSYM_RUNTIME_EXTERNAL(gs_assert_eager); +GENSYM_RUNTIME_EXTERNAL(__assert_fail); +GENSYM_RUNTIME_EXTERNAL(llvm_va_start); +GENSYM_RUNTIME_EXTERNAL(llvm_va_end); +GENSYM_RUNTIME_EXTERNAL(llvm_va_copy); +GENSYM_RUNTIME_EXTERNAL(gs_assume); +GENSYM_RUNTIME_EXTERNAL(gs_is_symbolic); +GENSYM_RUNTIME_EXTERNAL(gs_get_valuel); +GENSYM_RUNTIME_EXTERNAL(getpagesize); +GENSYM_RUNTIME_EXTERNAL(gs_prefer_cex); +GENSYM_RUNTIME_EXTERNAL(gs_posix_prefer_cex); +GENSYM_RUNTIME_EXTERNAL(gs_warning_once); +GENSYM_RUNTIME_EXTERNAL(make_symbolic); +GENSYM_RUNTIME_EXTERNAL(make_symbolic_whole); +GENSYM_RUNTIME_EXTERNAL(malloc); +GENSYM_RUNTIME_EXTERNAL(memalign); +GENSYM_RUNTIME_EXTERNAL(calloc); +GENSYM_RUNTIME_EXTERNAL(realloc); +GENSYM_RUNTIME_EXTERNAL(reallocarray); +GENSYM_RUNTIME_EXTERNAL(llvm_memcpy); +GENSYM_RUNTIME_EXTERNAL(llvm_memmove); +GENSYM_RUNTIME_EXTERNAL(llvm_memset); +GENSYM_RUNTIME_EXTERNAL(syscall); +GENSYM_RUNTIME_EXTERNAL(__errno_location); +GENSYM_RUNTIME_EXTERNAL(syscall_open); +GENSYM_RUNTIME_EXTERNAL(syscall_close); +GENSYM_RUNTIME_EXTERNAL(syscall_read); +GENSYM_RUNTIME_EXTERNAL(syscall_write); +GENSYM_RUNTIME_EXTERNAL(syscall_lseek); +GENSYM_RUNTIME_EXTERNAL(syscall_lseek64); +GENSYM_RUNTIME_EXTERNAL(syscall_stat); +GENSYM_RUNTIME_EXTERNAL(syscall_fstat); +GENSYM_RUNTIME_EXTERNAL(syscall_lstat); +GENSYM_RUNTIME_EXTERNAL(syscall_statfs); +GENSYM_RUNTIME_EXTERNAL(syscall_mkdir); +GENSYM_RUNTIME_EXTERNAL(syscall_rmdir); +GENSYM_RUNTIME_EXTERNAL(syscall_creat); +GENSYM_RUNTIME_EXTERNAL(syscall_unlink); +GENSYM_RUNTIME_EXTERNAL(syscall_chmod); +GENSYM_RUNTIME_EXTERNAL(syscall_chown); +GENSYM_RUNTIME_EXTERNAL(syscall_ioctl); +GENSYM_RUNTIME_EXTERNAL(syscall_fcntl); +#undef GENSYM_RUNTIME_EXTERNAL + +Value make_symbolic_det(State&, Args); +Value make_symbolic_whole_det(State&, Args); + +} // namespace gensym::runtime::v1 + +#ifndef INFO +#define INFO(message) do { if (::gensym::runtime::v1::debug_enabled()) { std::cout << "[Info] " << message << std::endl; } } while (false) +#endif + +#endif diff --git a/headers/gensym/value_ops.hpp b/headers/gensym/value_ops.hpp index 382b238ab..20adb828d 100644 --- a/headers/gensym/value_ops.hpp +++ b/headers/gensym/value_ops.hpp @@ -590,14 +590,14 @@ inline PtrVal SymV::neg(const PtrVal& v) { // Uninitialized value inline PtrVal make_UnInitV() { - #ifdef GENSYM_SYMBOLIC_UNINIT + if (symbolic_uninit) { std::string name = fresh("uninit"); PtrVal UnInitV = make_SymV(name, 8); return UnInitV; - #else + } else { PtrVal UnInitV = make_IntV(0, 8); return UnInitV; - #endif + } } inline TrList make_UnInitList(int n) { diff --git a/runtime/Makefile b/runtime/Makefile new file mode 100644 index 000000000..d538d9da6 --- /dev/null +++ b/runtime/Makefile @@ -0,0 +1,29 @@ +CXX ?= g++ +AR ?= ar +ROOT := $(abspath ..) +BUILD_DIR := build +TARGET := $(BUILD_DIR)/libgensym_runtime.a +OBJECT := $(BUILD_DIR)/runtime.o +DEP := $(OBJECT:.o=.d) + +CPPFLAGS := -I$(ROOT)/headers -I$(ROOT)/third-party/immer -I$(ROOT)/third-party/parallel-hashmap +CXXFLAGS ?= -O3 +CXXFLAGS += -std=c++17 -Wno-format-security -fno-omit-frame-pointer -MMD -MP + +.DEFAULT_GOAL := all + +all: $(TARGET) + +$(TARGET): $(OBJECT) + $(AR) rcs $@ $^ + +$(OBJECT): runtime.cpp + @mkdir -p $(@D) + $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c -o $@ $< + +clean: + rm -rf $(BUILD_DIR) + +-include $(DEP) + +.PHONY: all clean diff --git a/runtime/runtime.cpp b/runtime/runtime.cpp new file mode 100644 index 000000000..1a2579aa6 --- /dev/null +++ b/runtime/runtime.cpp @@ -0,0 +1,310 @@ +#include + +#define IMPURE_STATE +#include + +namespace gensym::runtime::v1 { + +struct Bridge { + static ::PtrVal unwrap(Value v) { return ::PtrVal(static_cast<::Value*>(v.impl_)); } + static Value wrap(::PtrVal v) { return Value(v.get()); } + static ::SS& unwrap(State& s) { return *static_cast<::SS*>(s.impl_); } + static const ::SS& unwrap(const State& s) { return *static_cast(s.impl_); } + static State own(::SS s) { return State(new ::SS(std::move(s)), true); } + static State borrow(::SS& s) { return State(&s, false); } + static ::PC& unwrap(PathCondition& pc) { return *static_cast<::PC*>(pc.impl_); } + static const ::PC& unwrap(const PathCondition& pc) { return *static_cast(pc.impl_); } + static PathCondition own(::PC pc) { return PathCondition(new ::PC(std::move(pc))); } +}; + +static ::List<::PtrVal> unwrap_args(const Args& args) { + auto out = ::List<::PtrVal>{}.transient(); + for (auto value : args) out.push_back(Bridge::unwrap(value)); + return out.persistent(); +} + +static Args wrap_args(const ::List<::PtrVal>& args) { + Args out; + out.reserve(args.size()); + for (auto value : args) out.push_back(Bridge::wrap(value)); + return out; +} + +static ::Cont unwrap_cont(Cont cont) { + return [cont = std::move(cont)](::SS& state, ::PtrVal value) mutable { + auto view = Bridge::borrow(state); + return cont(view, Bridge::wrap(value)); + }; +} + +static Cont wrap_cont(::Cont cont) { + return [cont = std::move(cont)](State& state, Value value) mutable { + return cont(Bridge::unwrap(state), Bridge::unwrap(value)); + }; +} + +bool Value::is_conc() const { return Bridge::unwrap(*this)->is_conc(); } +std::size_t Value::get_bw() const { return Bridge::unwrap(*this)->get_bw(); } +Args Value::to_bytes() const { return wrap_args(Bridge::unwrap(*this)->to_bytes()); } +Args Value::to_bytes_shadow() const { return wrap_args(Bridge::unwrap(*this)->to_bytes_shadow()); } +Value Value::from_bytes(const Args& values) { return Bridge::wrap(::Value::from_bytes(unwrap_args(values))); } +Value Value::from_bytes_shadow(const Args& values) { return Bridge::wrap(::Value::from_bytes_shadow(unwrap_args(values))); } +std::ostream& operator<<(std::ostream& out, const Value& value) { + if (!value) return out << "nullptr"; + return out << Bridge::unwrap(value)->toString(); +} + +PathCondition::PathCondition() : impl_(new ::PC(::mt_pc)) {} +PathCondition::PathCondition(const PathCondition& rhs) : impl_(new ::PC(Bridge::unwrap(rhs))) {} +PathCondition::PathCondition(PathCondition&& rhs) noexcept : impl_(rhs.impl_) { rhs.impl_ = nullptr; } +PathCondition& PathCondition::operator=(const PathCondition& rhs) { + if (this != &rhs) { + if (impl_) *static_cast<::PC*>(impl_) = Bridge::unwrap(rhs); + else impl_ = new ::PC(Bridge::unwrap(rhs)); + } + return *this; +} +PathCondition& PathCondition::operator=(PathCondition&& rhs) noexcept { + if (this != &rhs) { delete static_cast<::PC*>(impl_); impl_ = rhs.impl_; rhs.impl_ = nullptr; } + return *this; +} +PathCondition::~PathCondition() { delete static_cast<::PC*>(impl_); } +PathCondition& PathCondition::add(Value value) { Bridge::unwrap(*this).add(Bridge::unwrap(value)); return *this; } + +State::State() : impl_(new ::SS(::mt_ss)), owned_(true) {} +State::State(const State& rhs) : impl_(new ::SS(Bridge::unwrap(rhs))), owned_(true) {} +State::State(State&& rhs) noexcept : impl_(rhs.impl_), owned_(rhs.owned_) { rhs.impl_ = nullptr; rhs.owned_ = false; } +State& State::operator=(const State& rhs) { + if (this != &rhs) { + if (owned_) delete static_cast<::SS*>(impl_); + impl_ = new ::SS(Bridge::unwrap(rhs)); owned_ = true; + } + return *this; +} +State& State::operator=(State&& rhs) noexcept { + if (this != &rhs) { + if (owned_) delete static_cast<::SS*>(impl_); + impl_ = rhs.impl_; owned_ = rhs.owned_; rhs.impl_ = nullptr; rhs.owned_ = false; + } + return *this; +} +State::~State() { if (owned_) delete static_cast<::SS*>(impl_); } +State State::fork() { return Bridge::own(Bridge::unwrap(*this).fork()); } +State State::copy() const { return State(*this); } +std::uint64_t State::get_ssid() const { return const_cast<::SS&>(Bridge::unwrap(*this)).get_ssid(); } +int State::incoming_block() const { return const_cast<::SS&>(Bridge::unwrap(*this)).incoming_block(); } +Value State::env_lookup(int id) { return Bridge::wrap(Bridge::unwrap(*this).env_lookup(id)); } +std::size_t State::heap_size() const { return const_cast<::SS&>(Bridge::unwrap(*this)).heap_size(); } +std::size_t State::stack_size() const { return const_cast<::SS&>(Bridge::unwrap(*this)).stack_size(); } +Value State::at(Value address, std::size_t size) { return Bridge::wrap(Bridge::unwrap(*this).at(Bridge::unwrap(address), size)); } +Value State::at_struct(Value address, int size) { return Bridge::wrap(Bridge::unwrap(*this).at_struct(Bridge::unwrap(address), size)); } +Args State::at_seq(Value address, int size) { return wrap_args(Bridge::unwrap(*this).at_seq(Bridge::unwrap(address), size)); } +Value State::heap_lookup(std::size_t address) { return Bridge::wrap(Bridge::unwrap(*this).heap_lookup(address)); } +State& State::alloc_stack(std::size_t size) { Bridge::unwrap(*this).alloc_stack(size); return *this; } +State& State::alloc_heap(std::size_t size) { Bridge::unwrap(*this).alloc_heap(size); return *this; } +State& State::update(Value address, Value value) { Bridge::unwrap(*this).update(Bridge::unwrap(address), Bridge::unwrap(value), (value.get_bw() + 7) / 8); return *this; } +State& State::update(Value address, Value value, std::size_t size) { Bridge::unwrap(*this).update(Bridge::unwrap(address), Bridge::unwrap(value), size); return *this; } +State& State::update_seq(Value address, const Args& values) { Bridge::unwrap(*this).update_seq(Bridge::unwrap(address), unwrap_args(values)); return *this; } +State& State::push() { Bridge::unwrap(*this).push(); return *this; } +State& State::push(Cont cont) { Bridge::unwrap(*this).push(unwrap_cont(std::move(cont))); return *this; } +Cont State::pop(std::size_t keep) { return wrap_cont(Bridge::unwrap(*this).pop(keep)); } +State& State::assign(int id, Value value) { Bridge::unwrap(*this).assign(id, Bridge::unwrap(value)); return *this; } +State& State::assign_seq(const Ids& ids, const Args& values) { + auto iids = ::List<::Id>(ids.begin(), ids.end()); + Bridge::unwrap(*this).assign_seq(std::move(iids), unwrap_args(values)); return *this; +} +State& State::heap_append(const Args& values) { Bridge::unwrap(*this).heap_append(unwrap_args(values)); return *this; } +State& State::add_PC(Value value) { Bridge::unwrap(*this).add_PC(Bridge::unwrap(value)); return *this; } +PathCondition State::get_PC() const { return Bridge::own(const_cast<::SS&>(Bridge::unwrap(*this)).copy_PC()); } +PathCondition State::copy_PC() const { return get_PC(); } +State& State::add_incoming_block(int block) { Bridge::unwrap(*this).add_incoming_block(block); return *this; } +State& State::cover_block(int block) { Bridge::unwrap(*this).cover_block(block); return *this; } +State& State::init_arg() { Bridge::unwrap(*this).init_arg(); return *this; } +State& State::init_error_loc() { Bridge::unwrap(*this).init_error_loc(); return *this; } +Value State::error_loc() { return Bridge::wrap(Bridge::unwrap(*this).error_loc()); } + +static Coverage public_coverage; +Coverage& cov() { return public_coverage; } +bool debug_enabled() { return ::runtime_debug; } +void Coverage::set_num_blocks(std::size_t n) { ::cov().extend_blocks(n, {}); } +void Coverage::extend_blocks(std::size_t n, const std::vector>& branches) { ::cov().extend_blocks(n, branches); } +void Coverage::inc_block(std::size_t id) { ::cov().inc_block(id); } +void Coverage::inc_branch(std::size_t id, std::size_t branch) { ::cov().inc_branch(id, branch); } +void Coverage::inc_path(std::size_t n) { ::cov().inc_path(n); } +void Coverage::inc_inst(std::size_t n) { ::cov().inc_inst(n); } +void Coverage::start_monitor() { ::cov().start_monitor(); } +void Coverage::print_block_cov() { ::cov().print_block_cov(std::cout); } +void Coverage::print_time() { ::cov().print_time(false, std::cout); } +void Coverage::print_path_cov() { ::cov().print_path_cov(std::cout); } + +void configure(const ProgramConfig& config) { + ::symbolic_uninit = config.symbolic_uninitialized; + ::runtime_debug = config.debug; + ::cov().extend_blocks(config.block_count, config.branch_arity); +} +Value g_argc; +Value g_argv; +void prelude(int argc, char** argv, const ProgramConfig& config) { + configure(config); + ::prelude(argc, argv); + g_argc = Bridge::wrap(::g_argc); + g_argv = Bridge::wrap(::g_argv); +} +void epilogue() { ::epilogue(); } +int runtime_exit_code() { return ::exit_code.load().value_or(0); } +bool can_par_tp() { return ::can_par_tp(); } +void add_task(std::uint64_t id, std::function task) { ::tp.add_task(id, std::move(task)); } + +State make_initial_state(const Args& heap) { + if (heap.empty()) return Bridge::own(::mt_ss); + return Bridge::own(::SS(unwrap_args(heap), ::mt_stack, ::mt_pc, ::mt_meta)); +} +Value make_IntV(std::int64_t value, std::size_t bw, bool msb) { return Bridge::wrap(::make_IntV(value, bw, msb)); } +Value make_FloatV(double value, std::size_t bw) { return Bridge::wrap(::make_FloatV(value, bw)); } +Value make_FloatV_fp80(const std::vector& bytes) { + std::array data{}; + std::copy_n(bytes.begin(), std::min(bytes.size(), data.size()), data.begin()); + return Bridge::wrap(::make_FloatV_fp80(data)); +} +static ::LocV::Kind unwrap_kind(LocV::Kind kind) { return static_cast<::LocV::Kind>(kind); } +Value make_LocV(std::uint32_t base, LocV::Kind kind, std::size_t size, std::size_t off) { return Bridge::wrap(::make_LocV(base, unwrap_kind(kind), size, off)); } +Value make_LocV_null() { return Bridge::wrap(::make_LocV_null()); } +Value make_SymV(const std::string& name, std::size_t bw) { return Bridge::wrap(::make_SymV(name, bw)); } +Value make_SymLocV(std::uint32_t base, LocV::Kind kind, std::size_t size, Value off) { return Bridge::wrap(::make_SymLocV(base, unwrap_kind(kind), size, Bridge::unwrap(off))); } +Value make_ShadowV() { return Bridge::wrap(::make_ShadowV()); } +Value make_ShadowV(std::int8_t off) { return Bridge::wrap(::make_ShadowV(off)); } +std::int64_t proj_IntV(Value value) { return ::proj_IntV(Bridge::unwrap(value)); } +Value int_op_1(iOP op, Value value) { return Bridge::wrap(::int_op_1(static_cast<::iOP>(op), Bridge::unwrap(value))); } +Value int_op_2(iOP op, Value lhs, Value rhs) { return Bridge::wrap(::int_op_2(static_cast<::iOP>(op), Bridge::unwrap(lhs), Bridge::unwrap(rhs))); } +Value int_op_3(iOP op, Value a, Value b, Value c) { return Bridge::wrap(::int_op_3(static_cast<::iOP>(op), Bridge::unwrap(a), Bridge::unwrap(b), Bridge::unwrap(c))); } +Value float_op_2(fOP op, Value lhs, Value rhs) { return Bridge::wrap(::float_op_2(static_cast<::fOP>(op), Bridge::unwrap(lhs), Bridge::unwrap(rhs))); } +Value bv_sext(Value value, std::size_t bw) { return Bridge::wrap(::bv_sext(Bridge::unwrap(value), bw)); } +Value bv_zext(Value value, std::size_t bw) { return Bridge::wrap(::bv_zext(Bridge::unwrap(value), bw)); } +Value trunc(Value value, int from, int to) { return Bridge::wrap(::trunc(Bridge::unwrap(value), from, to)); } +Value ite(Value condition, Value then_value, Value else_value) { return Bridge::wrap(::ite(Bridge::unwrap(condition), Bridge::unwrap(then_value), Bridge::unwrap(else_value))); } +Value ptr_add(Value pointer, Value offset) { return Bridge::wrap(::ptr_add(Bridge::unwrap(pointer), Bridge::unwrap(offset))); } + +struct PublicCPSValue final : ::LocV { + CPSFunc function; + explicit PublicCPSValue(CPSFunc f) + : ::LocV(static_cast<::Addr>(reinterpret_cast(f)), ::LocV::kNative, 1, 0), function(f) { + ASSERT(f, "public CPS function cannot be null"); + } + bool compare(const ::Value* value) const override { + auto* rhs = dynamic_cast(value); + return rhs && function == rhs->function; + } + std::string toString() const override { return "PublicCPSFunV"; } +}; + +Value make_CPSFunV(CPSFunc function) { return Bridge::wrap(::PtrVal(new PublicCPSValue(function))); } +std::monostate cps_apply(Value value, State state, Args args, Cont cont) { + auto* function = dynamic_cast(Bridge::unwrap(value).get()); + ASSERT(function, "cps_apply: not a public CPS function value"); + return function->function(state, std::move(args), std::move(cont)); +} +std::monostate cont_apply(Cont cont, State& state, Value value) { return cont(state, value); } + +static std::function unwrap_block(Block block) { + return [block = std::move(block)](::SS& state, ::Cont cont) mutable { + auto view = Bridge::borrow(state); + return block(view, wrap_cont(std::move(cont))); + }; +} +std::monostate sym_exec_br_k(State& state, unsigned id, Value t, Value f, Block tb, Block fb, Cont cont) { + return ::sym_exec_br_k(Bridge::unwrap(state), id, Bridge::unwrap(t), Bridge::unwrap(f), + unwrap_block(std::move(tb)), unwrap_block(std::move(fb)), unwrap_cont(std::move(cont))); +} +std::vector> array_lookup(State& state, Value base, Value offset, std::size_t size) { + auto result = ::array_lookup(Bridge::unwrap(state), Bridge::unwrap(base), Bridge::unwrap(offset), size); + std::vector> out; + out.reserve(result.size()); + for (auto& [s, v] : result) out.emplace_back(Bridge::own(std::move(s)), Bridge::wrap(v)); + return out; +} +std::monostate array_lookup_k(State& state, Value base, Value offset, std::size_t size, Cont cont) { + return ::array_lookup_k(Bridge::unwrap(state), Bridge::unwrap(base), Bridge::unwrap(offset), size, unwrap_cont(std::move(cont))); +} +bool check_pc(PathCondition pc) { return ::check_pc(Bridge::unwrap(pc)); } +void check_pc_to_file(const State& state) { ::check_pc_to_file(Bridge::unwrap(state)); } + +std::int64_t get_int_arg(State& state, Value value) { return ::get_int_arg(Bridge::unwrap(state), Bridge::unwrap(value)); } +double get_float_arg(State& state, Value value) { return ::get_float_arg(Bridge::unwrap(state), Bridge::unwrap(value)); } +void* get_pointer_arg(State& state, Value value) { return ::get_pointer_arg(Bridge::unwrap(state), Bridge::unwrap(value)); } +void writeback_pointer_arg(State& state, Value address, void* buffer) { ::writeback_pointer_arg(Bridge::unwrap(state), Bridge::unwrap(address), buffer); } + +#define WRAP_EXTERNAL_REF(name) \ + std::monostate name(State& state, Args args, Cont cont) { \ + return ::name(Bridge::unwrap(state), unwrap_args(args), unwrap_cont(std::move(cont))); \ + } +#define WRAP_EXTERNAL_VAL(name) \ + std::monostate name(State& state, Args args, Cont cont) { \ + auto inner = Bridge::unwrap(state); \ + return ::name(std::move(inner), unwrap_args(args), unwrap_cont(std::move(cont))); \ + } + +WRAP_EXTERNAL_VAL(stop) +WRAP_EXTERNAL_VAL(noop) +WRAP_EXTERNAL_VAL(_exit) +WRAP_EXTERNAL_VAL(exit) +WRAP_EXTERNAL_VAL(abort) +WRAP_EXTERNAL_VAL(sym_exit) +WRAP_EXTERNAL_VAL(print_string) +WRAP_EXTERNAL_VAL(sym_print) +WRAP_EXTERNAL_VAL(gs_assert) +WRAP_EXTERNAL_VAL(gs_assert_eager) +WRAP_EXTERNAL_VAL(__assert_fail) +WRAP_EXTERNAL_VAL(llvm_va_start) +WRAP_EXTERNAL_VAL(llvm_va_end) +WRAP_EXTERNAL_VAL(llvm_va_copy) +WRAP_EXTERNAL_VAL(gs_assume) +WRAP_EXTERNAL_VAL(gs_is_symbolic) +WRAP_EXTERNAL_VAL(gs_get_valuel) +WRAP_EXTERNAL_VAL(getpagesize) +WRAP_EXTERNAL_VAL(gs_prefer_cex) +WRAP_EXTERNAL_VAL(gs_posix_prefer_cex) +WRAP_EXTERNAL_VAL(gs_warning_once) +WRAP_EXTERNAL_REF(make_symbolic) +WRAP_EXTERNAL_REF(make_symbolic_whole) +WRAP_EXTERNAL_REF(malloc) +WRAP_EXTERNAL_REF(memalign) +WRAP_EXTERNAL_REF(calloc) +WRAP_EXTERNAL_REF(realloc) +WRAP_EXTERNAL_REF(reallocarray) +WRAP_EXTERNAL_REF(llvm_memcpy) +WRAP_EXTERNAL_REF(llvm_memmove) +WRAP_EXTERNAL_REF(llvm_memset) +WRAP_EXTERNAL_REF(syscall) +WRAP_EXTERNAL_VAL(__errno_location) +WRAP_EXTERNAL_VAL(syscall_open) +WRAP_EXTERNAL_VAL(syscall_close) +WRAP_EXTERNAL_VAL(syscall_read) +WRAP_EXTERNAL_VAL(syscall_write) +WRAP_EXTERNAL_VAL(syscall_lseek) +WRAP_EXTERNAL_VAL(syscall_lseek64) +WRAP_EXTERNAL_VAL(syscall_stat) +WRAP_EXTERNAL_VAL(syscall_fstat) +WRAP_EXTERNAL_VAL(syscall_lstat) +WRAP_EXTERNAL_VAL(syscall_statfs) +WRAP_EXTERNAL_VAL(syscall_mkdir) +WRAP_EXTERNAL_VAL(syscall_rmdir) +WRAP_EXTERNAL_VAL(syscall_creat) +WRAP_EXTERNAL_VAL(syscall_unlink) +WRAP_EXTERNAL_VAL(syscall_chmod) +WRAP_EXTERNAL_VAL(syscall_chown) +WRAP_EXTERNAL_VAL(syscall_ioctl) +WRAP_EXTERNAL_VAL(syscall_fcntl) + +#undef WRAP_EXTERNAL_REF +#undef WRAP_EXTERNAL_VAL + +Value make_symbolic_det(State& state, Args args) { return Bridge::wrap(::make_symbolic_det(Bridge::unwrap(state), unwrap_args(args))); } +Value make_symbolic_whole_det(State& state, Args args) { return Bridge::wrap(::make_symbolic_whole_det(Bridge::unwrap(state), unwrap_args(args))); } + +} // namespace gensym::runtime::v1 + +namespace { +Monitor runtime_monitor; +} + +Monitor& cov() { return runtime_monitor; } diff --git a/src/main/scala/gensym/Codegen.scala b/src/main/scala/gensym/Codegen.scala index 6555908bd..e1ef992d4 100644 --- a/src/main/scala/gensym/Codegen.scala +++ b/src/main/scala/gensym/Codegen.scala @@ -343,6 +343,96 @@ trait ImpureGSCodeGen extends GenericGSCodeGen { } } +trait ImpCPSRuntimeCodeGen extends ImpureGSCodeGen { + unregisterHeader("", "", + "", "", "", + "") + includePaths -= "third-party/immer" + includePaths -= "third-party/parallel-hashmap" + registerHeader("headers", "") + + override def remap(m: Manifest[_]): String = { + if (m.runtimeClass.getName == "scala.collection.immutable.List") + s"std::vector<${remap(m.typeArguments(0))}>" + else super.remap(m) + } + + override def quote(s: Def): String = s match { + case Const(xs: List[_]) => + val mA = Adapter.typeMap(s.asInstanceOf[Backend.Exp]) + s"std::vector<${remap(mA.typeArguments(0))}>{${xs.map(x => quote(Const(x))).mkString(", ")}}" + case _ => super.quote(s) + } + + override def shallow(n: Node): Unit = n match { + case Node(s, "init-ss", List(), _) => es"make_initial_state()" + case Node(s, "init-ss", List(m), _) => es"make_initial_state($m)" + case Node(s, "list-new", Const(mA: Manifest[_])::xs, _) => + es"std::vector<${remap(mA)}>{" + if (xs.nonEmpty) { + shallow(xs.head) + xs.tail.foreach { x => emit(", "); shallow(x) } + } + es"}" + case Node(s, "list-fill", List(Const(mA: Manifest[_]), x, e), _) => + es"std::vector<${remap(mA)}>("; shallow(x); es", "; shallow(e); es")" + case Node(s, "list-apply", List(xs, i), _) => es"$xs.at($i)" + case Node(s, "list-head", List(xs), _) => es"$xs.front()" + case Node(s, "list-last", List(xs), _) => es"$xs.back()" + case Node(s, "list-size", List(xs), _) => es"$xs.size()" + case Node(s, "list-isEmpty", List(xs), _) => es"$xs.empty()" + case Node(s, "add_tp_task", List(ssid, b: Block), _) => + es"add_task($ssid" + quoteTypedBlock(b, false, true, capture = "=") + es")" + case _ => super.shallow(n) + } + + override def emitHeaderFile: Unit = { + val filename = codegenFolder + "/common.h" + val out = new java.io.PrintStream(filename) + withStream(out) { + emitln("/* Emitting header file */") + emitHeaders(stream) + emitln("using namespace gensym::runtime::v1;") + emitFunctionDecls(stream) + emitDatastructures(stream) + if (Global.config.emitVarIdMap) emitln(s""" + |/* variable-id map: + |${Counter.variable.toString} + |*/""".stripMargin) + if (Global.config.emitBlockIdMap) emitln(s""" + |/* block-id map: + |${Counter.block.toString} + |*/""".stripMargin) + emitln("/* End of header file */") + } + out.close + } + + override def emitAll(g: Graph, name: String)(m1: Manifest[_], m2: Manifest[_]): Unit = { + val ng = init(g) + val src = run(name, ng) + emitHeaderFile + emitFunctionFiles + emitInit(stream) + emitln(s"/* Generated main file: $name */") + emitln("#include \"common.h\"") + emit(src) + emitln(s""" + |int main(int argc, char *argv[]) { + | prelude(argc, argv, ProgramConfig{${Counter.block.count}, ${Counter.printBranchStat}, ${Global.config.symbolicUninit}, ${Global.config.genDebug}}); + | if (can_par_tp()) { + | add_task(1, []() { return $name(0); }); + | } else { + | $name(0); + | } + | epilogue(); + | return runtime_exit_code(); + |} """.stripMargin) + } +} + trait StdVectorCodeGen extends ExtendedCPPCodeGen { // TODO: make it more complete diff --git a/src/main/scala/gensym/Driver.scala b/src/main/scala/gensym/Driver.scala index ee0744057..56b7c87d0 100644 --- a/src/main/scala/gensym/Driver.scala +++ b/src/main/scala/gensym/Driver.scala @@ -73,6 +73,56 @@ abstract class GenericGSDriver[A: Manifest, B: Manifest] mainStream.close } + def genRuntimeMakefile: Unit = { + val out = new PrintStream(s"$folder/$appName/Makefile") + val curDir = new File(".").getCanonicalPath + val libraries = codegen.libraryFlags.mkString(" ") + val includes = codegen.includePaths.map(s"-I $curDir/" + _).mkString(" ") + val libraryPaths = codegen.libraryPaths.map(p => s"-L $curDir/$p -Wl,-rpath $curDir/$p").mkString(" ") + val debugFlags = if (Global.config.genDebug) "-g" else "" + + out.println(s"""|BUILD_DIR = build + |TARGET = $appName + |SRC_DIR = . + |SOURCES = $$(shell find $$(SRC_DIR)/ -name "*.cpp" ! -name "$${TARGET}.cpp") + |OBJECTS = $$(SOURCES:$$(SRC_DIR)/%.cpp=$$(BUILD_DIR)/%.o) + |OPT = -O3 + |CC = g++ -std=c++17 -Wno-format-security + |RUNTIME_DIR = $curDir/runtime + |RUNTIME_LIB = $$(RUNTIME_DIR)/build/libgensym_runtime.a + |PERFFLAGS = -fno-omit-frame-pointer $debugFlags + |CXXFLAGS = $includes $$(PERFFLAGS) + |LDFLAGS = $libraryPaths + |LDLIBS = $libraries -lpthread + | + |default: $$(TARGET) + | + |runtime: + |\t$$(MAKE) -C $$(RUNTIME_DIR) + | + |.SECONDEXPANSION: + | + |$$(OBJECTS): $$$$(patsubst $$(BUILD_DIR)/%.o,$$(SRC_DIR)/%.cpp,$$$$@) | runtime + |\tmkdir -p $$(@D) + |\t$$(CC) $$(OPT) -c -o $$@ $$< $$(CXXFLAGS) + | + |$$(BUILD_DIR)/$${TARGET}.o : $${TARGET}.cpp | runtime + |\tmkdir -p $$(@D) + |\t$$(CC) -${config.mainFileOpt} -c -o $$@ $$< $$(CXXFLAGS) + | + |$$(TARGET): $$(OBJECTS) $$(BUILD_DIR)/$${TARGET}.o $$(RUNTIME_LIB) | runtime + |\t$$(CC) $$(OPT) -o $$@ $$(OBJECTS) $$(BUILD_DIR)/$${TARGET}.o $$(LDFLAGS) -Wl,--start-group $$(LDLIBS) $$(RUNTIME_LIB) -Wl,--end-group + | + |clean: + |\t@rm $${TARGET} 2>/dev/null || true + |\t@rm build -rf 2>/dev/null || true + |\t@rm tests -rf 2>/dev/null || true + | + |.PHONY: default runtime clean + |""".stripMargin) + out.close + } + def genMakefile: Unit = { val out = new PrintStream(s"$folder/$appName/Makefile") val curDir = new File(".").getCanonicalPath @@ -278,7 +328,15 @@ abstract class ImpVecGSDriver[A: Manifest, B: Manifest]( // Function call argument lists and result lists still use immer containers. abstract class ImpCPSGSDriver[A: Manifest, B: Manifest]( val m: Module, val appName: String, val folder: String , val config: Config) - extends ImpureEngineDriver[A, B] with ImpCPSGSEngine + extends ImpureEngineDriver[A, B] with ImpCPSGSEngine { q => + override lazy val codegen: GenericGSCodeGen = new ImpCPSRuntimeCodeGen { + val IR: q.type = q + val codegenFolder = s"$folder/$appName/" + setFunMap(q.funNameMap) + setBlockMap(q.nodeBlockMap) + } + override def genMakefile: Unit = genRuntimeMakefile +} trait GenSym { val insName: String @@ -289,8 +347,17 @@ trait GenSym { libdef = libPath match { case Some(p) => // linking with external library - load its manifest import java.io._ - val ois = new ObjectInputStream(new FileInputStream(s"$p/Manifest")) - try { Some(ois.readObject().asInstanceOf[ModDef]) } finally { ois.close } + val manifestPath = s"$p/Manifest" + val ois = new ObjectInputStream(new FileInputStream(manifestPath)) + val loaded = try { ois.readObject().asInstanceOf[ModDef] } + catch { + case e: Exception => throw new IllegalArgumentException( + s"Incompatible GenSym symbolic-library manifest at $manifestPath; regenerate the library with runtime API v${RuntimeABI.Version}.", e) + } finally { ois.close } + if (loaded.runtimeApiVersion != RuntimeABI.Version) + throw new IllegalArgumentException( + s"GenSym symbolic-library manifest uses runtime API v${loaded.runtimeApiVersion}; regenerate it for v${RuntimeABI.Version}.") + Some(loaded) case None => None } libdef match { @@ -393,7 +460,7 @@ class ImpCPSGS_lib extends GenSym with ImpureState { new ImpCPSGSDriver[Int, Unit](m, name, outputDir, config) { q => import java.io.{File,PrintStream} implicit val me: this.type = this - override lazy val codegen: GenericGSCodeGen = new ImpureGSCodeGen { + override lazy val codegen: GenericGSCodeGen = new ImpCPSRuntimeCodeGen { val IR: q.type = q val codegenFolder = s"$folder/$appName/" setFunMap(q.funNameMap) @@ -405,14 +472,9 @@ class ImpCPSGS_lib extends GenSym with ImpureState { withStream(out) { emitln("/* Emitting header file */") emitHeaders(stream) - emitln("using namespace immer;") + emitln("using namespace gensym::runtime::v1;") emitFunctionDecls(stream) emitDatastructures(stream) - emitln(s""" - |inline Monitor& cov() { - | static Monitor m; - | return m; - |}""".stripMargin) emitln("/* End of header file */") } out.close @@ -440,7 +502,7 @@ class ImpCPSGS_lib extends GenSym with ImpureState { val out = new PrintStream(s"$folder/$appName/Makefile") val curDir = new File(".").getCanonicalPath val includes = codegen.includePaths.map(s"-I $curDir/" + _).mkString(" ") - val debugFlags = if (Global.config.genDebug) "-g -DDEBUG" else "" + val debugFlags = if (Global.config.genDebug) "-g" else "" out.println(s"""|BUILD_DIR = build |TARGET = $appName.a @@ -451,18 +513,22 @@ class ImpCPSGS_lib extends GenSym with ImpureState { |OPT = -O3 |CC = g++ -std=c++17 -Wno-format-security |AR = ar cvq + |RUNTIME_DIR = $curDir/runtime |PERFFLAGS = -fno-omit-frame-pointer $debugFlags - |CXXFLAGS = $includes $extraFlags $$(PERFFLAGS) + |CXXFLAGS = $includes $$(PERFFLAGS) | |default: $$(TARGET) | + |runtime: + |\t$$(MAKE) -C $$(RUNTIME_DIR) + | |.SECONDEXPANSION: | - |$$(OBJECTS): $$$$(patsubst $$(BUILD_DIR)/%.o,$$(SRC_DIR)/%.cpp,$$$$@) + |$$(OBJECTS): $$$$(patsubst $$(BUILD_DIR)/%.o,$$(SRC_DIR)/%.cpp,$$$$@) | runtime |\tmkdir -p $$(@D) |\t$$(CC) $$(OPT) -c -o $$@ $$< $$(CXXFLAGS) | - |$$(BUILD_DIR)/$$(INITFILE).o : $$(INITFILE).cpp + |$$(BUILD_DIR)/$$(INITFILE).o : $$(INITFILE).cpp | runtime |\tmkdir -p $$(@D) |\t$$(CC) -${config.mainFileOpt} -c -o $$@ $$< $$(CXXFLAGS) | @@ -474,7 +540,7 @@ class ImpCPSGS_lib extends GenSym with ImpureState { |\t@rm build -rf 2>/dev/null || true |\t@rm tests -rf 2>/dev/null || true | - |.PHONY: default clean + |.PHONY: default runtime clean |""".stripMargin) out.close } @@ -538,7 +604,8 @@ class ImpCPSGS_lib extends GenSym with ImpureState { varlist.toList, folder, appName, - CntInfo(Counter.variable.count, Counter.block.count)) + CntInfo(Counter.variable.count, Counter.block.count), + RuntimeABI.Version) val oos = new ObjectOutputStream(new FileOutputStream(s"$folder/$appName/Manifest")) oos.writeObject(module) oos.close @@ -553,7 +620,7 @@ class ImpCPSGS_app extends GenSym with ImpureState { override val mainRename = "app_main" val libcdef = libdef.get implicit val me: this.type = this - override lazy val codegen: GenericGSCodeGen = new ImpureGSCodeGen { + override lazy val codegen: GenericGSCodeGen = new ImpCPSRuntimeCodeGen { val IR: q.type = q val codegenFolder = s"$folder/$appName/" setFunMap(q.funNameMap) @@ -565,7 +632,7 @@ class ImpCPSGS_app extends GenSym with ImpureState { withStream(out) { emitln("/* Emitting header file */") emitHeaders(stream) - emitln("using namespace immer;") + emitln("using namespace gensym::runtime::v1;") emitFunctionDecls(stream) emitDatastructures(stream) emitln("/* End of header file */") @@ -588,10 +655,10 @@ class ImpCPSGS_app extends GenSym with ImpureState { emit(src) emitln(s""" |int main(int argc, char *argv[]) { - | prelude(argc, argv); + | prelude(argc, argv, ProgramConfig{${Counter.block.count}, ${Counter.printBranchStat}, ${Global.config.symbolicUninit}, ${Global.config.genDebug}}); | $name(0); | epilogue(); - | return exit_code.load().value_or(0); + | return runtime_exit_code(); |} """.stripMargin) } registerHeader(libcdef.folder, s"<${libcdef.libName}/common.h>") diff --git a/src/main/scala/gensym/IRUtils.scala b/src/main/scala/gensym/IRUtils.scala index af3b0c535..f358683e5 100644 --- a/src/main/scala/gensym/IRUtils.scala +++ b/src/main/scala/gensym/IRUtils.scala @@ -241,4 +241,6 @@ case class CFG(funMap: Map[String, FunctionDef]) { case class FuncDef(ref: String, name: String) case class VarDef(name: String, off: Int, size: Int) case class CntInfo(vars: Int, blks: Int) -case class ModDef(funlist: List[FuncDef], varlist: List[VarDef], folder: String, libName: String, counters: CntInfo) \ No newline at end of file +object RuntimeABI { final val Version = 1 } +case class ModDef(funlist: List[FuncDef], varlist: List[VarDef], folder: String, + libName: String, counters: CntInfo, runtimeApiVersion: Int) diff --git a/src/test/scala/gensym/TestCases.scala b/src/test/scala/gensym/TestCases.scala index 02c034db3..01ed9d86c 100644 --- a/src/test/scala/gensym/TestCases.scala +++ b/src/test/scala/gensym/TestCases.scala @@ -33,11 +33,21 @@ object TestPrg { val minPath = "minPath" // minimal number of paths val minTest = "minTest" // minimal number of generated tests val status = "status" // the return status of executable + val blockCounts = "blockCounts" + val branches = "branches" + val threads = "threads" + val queuedTasks = "queuedTasks" + val queries = "queries" def nPath(n: Int): Map[String, Any] = Map(nPath -> n) def nTest(n: Int): Map[String, Any] = Map(nTest -> n) def minTest(n: Int): Map[String, Any] = Map(minTest -> n) def minPath(n: Int): Map[String, Any] = Map(minPath -> n) def status(n: Int): Map[String, Any] = Map(status -> n) + def expectBlocks(covered: Int, total: Int): Map[String, Any] = Map(blockCounts -> ((covered, total))) + def branches(partial: Int, full: Int, total: Int): Map[String, Any] = Map(branches -> ((partial, full, total))) + def threads(n: Int): Map[String, Any] = Map(threads -> n) + def queuedTasks(n: Int): Map[String, Any] = Map(queuedTasks -> n) + def queries(branch: Int, tests: Int, cacheHits: Int): Map[String, Any] = Map(queries -> ((branch, tests, cacheHits))) def noOpt: Seq[String] = Seq() diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index 67731c915..5c238e4d6 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -29,10 +29,29 @@ import TestCases._ abstract class TestGS extends FunSuite { import java.time.LocalDateTime + private val forbiddenGeneratedRuntimeTokens = Seq("immer", "parallel_hashmap", "gensym.hpp", "gensym/state_", "gensym/value_ops") + private def generatedSources(root: java.io.File): Seq[java.io.File] = + Option(root.listFiles).toSeq.flatten.flatMap { file => + if (file.isDirectory) generatedSources(file) + else if (file.getName.endsWith(".cpp") || file.getName == "common.h") Seq(file) + else Seq.empty + } + private def assertThinGeneratedSources(root: java.io.File): Unit = generatedSources(root).foreach { file => + val source = scala.io.Source.fromFile(file) + val text = try source.mkString finally source.close() + forbiddenGeneratedRuntimeTokens.foreach { token => + assert(!text.contains(token), s"Generated file ${file.getPath} leaked private runtime token '$token'") + } + } + case class TestResult(time: LocalDateTime, commit: String, engine: String, testName: String, - extSolverTime: Double, intSolverTime: Double, wholeTime: Double, blockCov: Double, - partialBrCov: Double, fullBrCov: Double, pathNum: Int, brQueryNum: Int, - testQueryNum: Int, cexCacheHit: Int) { + extSolverTime: Double, intSolverTime: Double, wholeTime: Double, + blockCount: Int, blockTotal: Int, partialBranchCount: Int, fullBranchCount: Int, + totalBranchCount: Int, pathNum: Int, threadCount: Int, queuedTaskCount: Int, + brQueryNum: Int, testQueryNum: Int, cexCacheHit: Int) { + val blockCov = blockCount.toDouble / blockTotal.toDouble + val partialBrCov = partialBranchCount.toDouble / totalBranchCount.toDouble + val fullBrCov = fullBranchCount.toDouble / totalBranchCount.toDouble override def toString() = s"$time,$commit,$engine,$testName,$extSolverTime,$intSolverTime,$wholeTime,$partialBrCov,$fullBrCov,$blockCov,$pathNum,$brQueryNum,$testQueryNum,$cexCacheHit" } @@ -42,14 +61,14 @@ abstract class TestGS extends FunSuite { def parseOutput(engine: String, testName: String, output: String): TestResult = { // example: // [43.4s/43.5s/46.0s] #blocks: 12/12; #br: 0/1/2; #paths: 1666; #threads: 1; #task-in-q: 0; #queries: 7328/1666 (1996) - val pattern = raw"\[([^s]+)s/([^s]+)s/([^s]+)s/([^s]+)s\] #blocks: (\d+)/(\d+); #br: (\d+)/(\d+)/(\d+); #paths: (\d+); .+; #queries: (\d+)/(\d+) \((\d+)\)".r + val pattern = raw"\[([^s]+)s/([^s]+)s/([^s]+)s/([^s]+)s\] #blocks: (\d+)/(\d+); #br: (\d+)/(\d+)/(\d+); #paths: (\d+); #threads: (\d+); #task-in-q: (\d+); #queries: (\d+)/(\d+) \((\d+)\)".r output.split("\n").last match { case pattern(extSolverTime, intSolverTime, _/*fsTime ignored*/, wholeTime, blockCnt, blockAll, - partialBr, fullBr, totalBr, pathNum, brQuerynum, testQueryNum, cexCacheHit) => + partialBr, fullBr, totalBr, pathNum, threadNum, queuedTaskNum, brQuerynum, testQueryNum, cexCacheHit) => TestResult(LocalDateTime.now(), gitCommit, engine, testName, extSolverTime.toDouble, intSolverTime.toDouble, wholeTime.toDouble, - blockCnt.toDouble/blockAll.toDouble, partialBr.toDouble/totalBr.toDouble, - fullBr.toDouble/totalBr.toDouble, pathNum.toInt, brQuerynum.toInt, + blockCnt.toInt, blockAll.toInt, partialBr.toInt, fullBr.toInt, totalBr.toInt, + pathNum.toInt, threadNum.toInt, queuedTaskNum.toInt, brQuerynum.toInt, testQueryNum.toInt, cexCacheHit.toInt) } } @@ -71,6 +90,7 @@ abstract class TestGS extends FunSuite { testWithGlobalConfig(name) { val code = gs.run(m, outname, f, config, libPath) + assertThinGeneratedSources(new java.io.File(s"$outputDir/$outname")) val mkRet = code.makeWithAllCores assert(mkRet == 0, "make failed") if (runCode) { @@ -93,6 +113,11 @@ abstract class TestGS extends FunSuite { if (exp.contains(minTest)) { assert(resStat.testQueryNum >= exp(minTest).asInstanceOf[Int], "Unexpected number of least test cases") } + if (exp.contains(blockCounts)) assert((resStat.blockCount, resStat.blockTotal) == exp(blockCounts), "Unexpected block counts") + if (exp.contains(branches)) assert((resStat.partialBranchCount, resStat.fullBranchCount, resStat.totalBranchCount) == exp(branches), "Unexpected branch counts") + if (exp.contains(threads)) assert(resStat.threadCount == exp(threads), "Unexpected thread count") + if (exp.contains(queuedTasks)) assert(resStat.queuedTaskCount == exp(queuedTasks), "Unexpected queued task count") + if (exp.contains(queries)) assert((resStat.brQueryNum, resStat.testQueryNum, resStat.cexCacheHit) == exp(queries), "Unexpected query counts") } } } @@ -184,5 +209,9 @@ class Playground extends TestGS { val gs = new ImpCPSGS val rtOpt = "--thread=1 --solver=z3" - testGS(gs, TestPrg(branch, "branch1", "@f", symArg(2), rtOpt, nPath(4))) -} \ No newline at end of file + //testGS(gs, TestPrg(branch, "branch1", "@f", symArg(2), rtOpt, + // nPath(4) ++ expectBlocks(7, 7) ++ branches(0, 3, 3) ++ threads(1) ++ queuedTasks(0) ++ queries(6, 4, 3))) + + testGS(gs, TestPrg(structReturnLong, "structReturnLongTest", "@main", noArg, rtOpt, nPath(1))) + testGS(gs, TestPrg(heapFunptr, "heapFunptr", "@main", noArg, rtOpt, nPath(1)++status(0))), +} From eb33f0fcc907897427d9c7391a882e4b8debe024 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 02:25:49 -0400 Subject: [PATCH 04/11] fix clang targeting x86; adapt external function gen to imp engine --- .github/workflows/scala.yml | 4 ++-- benchmarks/llvm/Makefile | 2 +- headers/gensym/runtime.hpp | 1 + runtime/runtime.cpp | 1 + src/main/scala/gensym/External.scala | 23 ++++++++++------------ src/main/scala/gensym/ImpSymExeState.scala | 9 ++++++++- src/test/scala/gensym/TestGS.scala | 17 ++++++++++------ 7 files changed, 34 insertions(+), 23 deletions(-) diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml index 7483171c3..732161e42 100644 --- a/.github/workflows/scala.yml +++ b/.github/workflows/scala.yml @@ -71,8 +71,8 @@ jobs: run: | cd third-party/wasmfx-tools cargo build --release - #- name: Generate models - # run: sbt 'runMain gensym.GenerateExternal' + - name: Generate models + run: sbt 'runMain gensym.GenerateExternal' - name: Run tests run: | sbt 'testOnly gensym.TestImpCPSGS' diff --git a/benchmarks/llvm/Makefile b/benchmarks/llvm/Makefile index 986160301..f2fce34d5 100644 --- a/benchmarks/llvm/Makefile +++ b/benchmarks/llvm/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +CC := clang-11 --target=x86_64-unknown-linux-gnu FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL) diff --git a/headers/gensym/runtime.hpp b/headers/gensym/runtime.hpp index dfb8476c2..43260201f 100644 --- a/headers/gensym/runtime.hpp +++ b/headers/gensym/runtime.hpp @@ -189,6 +189,7 @@ Value bv_zext(Value, std::size_t); Value trunc(Value, int, int); Value ite(Value, Value, Value); Value ptr_add(Value, Value); +Value structV_at(Value, std::size_t); Value make_CPSFunV(CPSFunc); std::monostate cps_apply(Value, State, Args, Cont); diff --git a/runtime/runtime.cpp b/runtime/runtime.cpp index 1a2579aa6..fcc02d011 100644 --- a/runtime/runtime.cpp +++ b/runtime/runtime.cpp @@ -183,6 +183,7 @@ Value bv_zext(Value value, std::size_t bw) { return Bridge::wrap(::bv_zext(Bridg Value trunc(Value value, int from, int to) { return Bridge::wrap(::trunc(Bridge::unwrap(value), from, to)); } Value ite(Value condition, Value then_value, Value else_value) { return Bridge::wrap(::ite(Bridge::unwrap(condition), Bridge::unwrap(then_value), Bridge::unwrap(else_value))); } Value ptr_add(Value pointer, Value offset) { return Bridge::wrap(::ptr_add(Bridge::unwrap(pointer), Bridge::unwrap(offset))); } +Value structV_at(Value value, std::size_t index) { return Bridge::wrap(::structV_at(Bridge::unwrap(value), static_cast(index))); } struct PublicCPSValue final : ::LocV { CPSFunc function; diff --git a/src/main/scala/gensym/External.scala b/src/main/scala/gensym/External.scala index 8a8c2c465..dd29f9c92 100644 --- a/src/main/scala/gensym/External.scala +++ b/src/main/scala/gensym/External.scala @@ -6,6 +6,7 @@ import lms.core.virtualize import lms.macros.SourceContext import lms.core.stub.{While => _, _} +import gensym.imp._ import gensym.llvm._ import gensym.llvm.IR._ import gensym.IRUtils._ @@ -19,9 +20,8 @@ import scala.collection.mutable.{Map => MutableMap, Set => MutableSet} // external/intrinsic functions with only slightly backend difference. // Can we generate them from our Scala DSL? -/* @virtualize -trait GenExternal extends ImpSymExeDefs { +trait GenExternal extends ImpSymExeDefs with FileSysDefs { trait Auto def info(msg: String) = unchecked("INFO(\"[FS] \" << \"" + msg + "\")") def info_obj(p: Rep[_], l: String = ""): Rep[Unit] = unchecked("INFO(\"", if (l == "") "" else l + ": ", "\" << ", p, ")") @@ -51,24 +51,26 @@ trait GenExternal extends ImpSymExeDefs { tk: (Rep[SS], Rep[FS]) => Rep[T], fk: (Rep[SS], Rep[FS]) => Rep[T]) = { unchecked("INFO(\"symExecBrFs: tCond is symbolic: \" << ", tCond, "->toString())") val ssf = ss.fork - val tpcSat = checkPC(ss.addPC(tCond).pc) - val fpcSat = checkPC(ssf.addPC(fCond).pc) + ss.addPC(tCond) + ssf.addPC(fCond) + val tpcSat = checkPC(ss.pc) + val fpcSat = checkPC(ssf.pc) if (tpcSat && fpcSat) { unchecked("INFO(\"symExecBrFs: both satisfiable\")") Coverage.incPath(1) // false branch - fk(ssf.addPC(fCond), FS.dcopy(fs)) + fk(ssf, FS.dcopy(fs)) // true branch - tk(ss.addPC(tCond), fs) + tk(ss, fs) // TODO: add second stage ++ operation <2022-08-19, David Deng> // // This version would lose result on non CPS versions // resF ++ resT } else if (tpcSat) { unchecked("INFO(\"symExecBrFs: only true satisfiable\")") - tk(ss.addPC(tCond), fs) + tk(ss, fs) } else { unchecked("INFO(\"symExecBrFs: only false satisfiable\")") - fk(ssf.addPC(fCond), fs) + fk(ssf, fs) } } @@ -622,7 +624,6 @@ trait GenExternal extends ImpSymExeDefs { res } } -*/ @virtualize trait ExternalUtil { self: BasicDefs with ValueDefs with SAIOps => @@ -650,7 +651,6 @@ trait ExternalUtil { self: BasicDefs with ValueDefs with SAIOps => } } -/* class ExternalGSDriver(folder: String = "./headers/gensym") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q => import java.io.{File, PrintStream} @@ -734,13 +734,10 @@ class ExternalGSDriver(folder: String = "./headers/gensym") extends SAISnippet[I () } } -*/ -/* object GenerateExternal { def main(args: Array[String]): Unit = { val code = new ExternalGSDriver code.genHeader } } -*/ diff --git a/src/main/scala/gensym/ImpSymExeState.scala b/src/main/scala/gensym/ImpSymExeState.scala index 1379ebb1f..9c25f32b6 100644 --- a/src/main/scala/gensym/ImpSymExeState.scala +++ b/src/main/scala/gensym/ImpSymExeState.scala @@ -90,6 +90,8 @@ trait ImpSymExeDefs extends SAIOps with BasicDefs with ValueDefs with Opaques wi if (isStruct == 0) reflectRead[Value]("ss-lookup-addr", ss, addr, size)(ss) else reflectRead[Value]("ss-lookup-addr-struct", ss, addr, size)(ss) } + def lookupSeq(addr: Rep[Value], count: Rep[Int]): Rep[List[Value]] = + reflectRead[List[Value]]("ss-lookup-addr-seq", ss, addr, count)(ss) //def arrayLookup(base: Rep[Value], offset: Rep[Value], eSize: Int, k: Rep[Cont]): Rep[Unit] = // "ss-array-lookup".reflectWith[Unit](ss, base, offset, eSize, k) @@ -99,6 +101,8 @@ trait ImpSymExeDefs extends SAIOps with BasicDefs with ValueDefs with Opaques wi def update(a: Rep[Value], v: Rep[Value], sz: Int): Rep[Unit] = reflectCtrl[Unit]("ss-update", ss, a, v, sz) @deprecated("Use update with size", "now and forever") def update(a: Rep[Value], v: Rep[Value]): Rep[Unit] = reflectCtrl[Unit]("ss-update", ss, a, v) + def updateSeq(a: Rep[Value], vs: Rep[List[Value]]): Rep[SS] = + reflectCtrl[SS]("ss-update-seq", ss, a, vs) def allocStack(n: Int, align: Int): Rep[Unit] = reflectWrite[Unit]("ss-alloc-stack", ss, new Mut[Int](n))(ss) @@ -121,7 +125,10 @@ trait ImpSymExeDefs extends SAIOps with BasicDefs with ValueDefs with Opaques wi def updateArg: Rep[Unit] = reflectWrite[Unit]("ss-arg", ss)(ss) def initErrorLoc: Rep[Unit] = reflectWrite[Unit]("ss-init-error-loc", ss)(ss) def getErrorLoc: Rep[Value] = reflectRead[Value]("ss-get-error-loc", ss)(ss) - def setErrorLoc(v: Rep[IntV]): Rep[Unit] = ss.update(ss.getErrorLoc, v, 4) + def setErrorLoc(v: Rep[IntV]): Rep[SS] = reflectCtrl[SS]("ss-update", ss, ss.getErrorLoc, v, 4) + + def getFs: Rep[FS] = reflectRead[FS]("ss-get-fs", ss)(ss) + def setFs(fs: Rep[FS]): Rep[Unit] = reflectWrite[Unit]("ss-set-fs", ss, fs)(ss) def addIncomingBlock(ctx: Ctx): Rep[Unit] = reflectWrite[Unit]("ss-add-incoming-block", ss, Counter.block.get(ctx.toString))(ss) diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index 5c238e4d6..02531f113 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -155,8 +155,7 @@ class TestImpCPSGS extends TestGS { class TestImpCPSGS_Z3 extends TestGS { val gs = new ImpCPSGS - //val cases = (TestCases.all ++ filesys ++ varArg).map { t => - val cases = (TestCases.all).map { t => + val cases = (TestCases.all ++ filesys ++ varArg).map { t => t.copy(runOpt = t.runOpt ++ Seq("--solver=z3")) } testGS(gs, cases) @@ -209,9 +208,15 @@ class Playground extends TestGS { val gs = new ImpCPSGS val rtOpt = "--thread=1 --solver=z3" - //testGS(gs, TestPrg(branch, "branch1", "@f", symArg(2), rtOpt, - // nPath(4) ++ expectBlocks(7, 7) ++ branches(0, 3, 3) ++ threads(1) ++ queuedTasks(0) ++ queries(6, 4, 3))) - testGS(gs, TestPrg(structReturnLong, "structReturnLongTest", "@main", noArg, rtOpt, nPath(1))) - testGS(gs, TestPrg(heapFunptr, "heapFunptr", "@main", noArg, rtOpt, nPath(1)++status(0))), + val cases = (TestCases.filesys).map { t => + t.copy(runOpt = t.runOpt ++ Seq("--solver=z3")) + } + testGS(gs, cases) + + // FIXME: + //testGS(gs, TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0))) + //testGS(gs, TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0))) + //testGS(gs, TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0))) + //testGS(gs, TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0))) } From 1a9d45dede3491eed31affe4478c0f6b057cb042 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 02:42:16 -0400 Subject: [PATCH 05/11] update clang to target x86 --- .devcontainer/Dockerfile | 1 + benchmarks/external-lib/Makefile | 3 ++- benchmarks/llvm/Makefile | 3 ++- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 6701ffecb..40db3a478 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -57,6 +57,7 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ perl \ minisat \ clang-11 \ + libc6-dev-amd64-cross \ unzip \ build-essential \ && rm -rf /var/lib/apt/lists/* diff --git a/benchmarks/external-lib/Makefile b/benchmarks/external-lib/Makefile index 68f03b9fd..877b821bb 100644 --- a/benchmarks/external-lib/Makefile +++ b/benchmarks/external-lib/Makefile @@ -1,6 +1,7 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +# GenSym's filesystem model follows the x86-64 Linux ABI (not the container host ABI). +CC := clang-11 --target=x86_64-unknown-linux-gnu --sysroot=/usr/x86_64-linux-gnu FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c -S KLEE_FLAGS := -D KLEE -g diff --git a/benchmarks/llvm/Makefile b/benchmarks/llvm/Makefile index f2fce34d5..53996f6ae 100644 --- a/benchmarks/llvm/Makefile +++ b/benchmarks/llvm/Makefile @@ -1,6 +1,7 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 --target=x86_64-unknown-linux-gnu +# Keep input IR on the x86-64 Linux ABI even when the devcontainer runs on ARM. +CC := clang-11 --target=x86_64-unknown-linux-gnu --sysroot=/usr/x86_64-linux-gnu FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL) From e57b684b542d7de50038c927db6d25b179d53846 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 02:54:22 -0400 Subject: [PATCH 06/11] update makefile to make it robust to arch --- .devcontainer/Dockerfile | 4 +++- benchmarks/demo-benchmarks/Makefile | 6 +++--- benchmarks/external-lib/Makefile | 7 +++---- benchmarks/klee-examples/Makefile | 5 +++-- benchmarks/klee-posix-fs/Makefile | 4 ++-- benchmarks/llvm/Makefile | 7 +++---- benchmarks/llvm/new_multipath/Makefile | 17 +++++++++-------- benchmarks/oopsla20/Makefile | 18 +++++++++--------- benchmarks/opt-experiments/Makefile | 6 +++--- benchmarks/pepm22/ccbse/Makefile | 5 +++-- benchmarks/pepm22/concolic/conc/Makefile | 3 ++- benchmarks/perf-mon/Makefile | 6 +++--- benchmarks/test-comp/array-examples/Makefile | 4 ++-- benchmarks/test-comp/array-programs/Makefile | 4 ++-- src/test/scala/gensym/TestGS.scala | 5 +---- 15 files changed, 51 insertions(+), 50 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 40db3a478..9c4bc264a 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -57,9 +57,11 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ perl \ minisat \ clang-11 \ - libc6-dev-amd64-cross \ unzip \ build-essential \ + && if [ "$(dpkg --print-architecture)" != "amd64" ]; then \ + apt-get install -y --no-install-recommends libc6-dev-amd64-cross; \ + fi \ && rm -rf /var/lib/apt/lists/* # ── Rust (required for third-party/wasmfx-tools) ───────────────────────────── diff --git a/benchmarks/demo-benchmarks/Makefile b/benchmarks/demo-benchmarks/Makefile index 625ebcbfa..ec5439449 100644 --- a/benchmarks/demo-benchmarks/Makefile +++ b/benchmarks/demo-benchmarks/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +include ../llvm-toolchain.mk FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL) @@ -21,13 +21,13 @@ klee: $(KLEE_TARGET) klee-exe: $(KLEE_REPLAY_TARGET) $(KLEE_TARGET): %.bc : %.c - $(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< $(KLEE_REPLAY_TARGET): %-replay : %.c $(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) diff --git a/benchmarks/external-lib/Makefile b/benchmarks/external-lib/Makefile index 877b821bb..1c8762a4b 100644 --- a/benchmarks/external-lib/Makefile +++ b/benchmarks/external-lib/Makefile @@ -1,7 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -# GenSym's filesystem model follows the x86-64 Linux ABI (not the container host ABI). -CC := clang-11 --target=x86_64-unknown-linux-gnu --sysroot=/usr/x86_64-linux-gnu +include ../llvm-toolchain.mk FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c -S KLEE_FLAGS := -D KLEE -g @@ -22,13 +21,13 @@ klee: $(KLEE_TARGET) klee-exe: $(KLEE_REPLAY_TARGET) $(KLEE_TARGET): %-klee.ll : %.c - $(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< $(KLEE_REPLAY_TARGET): %-replay : %.c $(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) *.ll diff --git a/benchmarks/klee-examples/Makefile b/benchmarks/klee-examples/Makefile index a10e52ced..074ff6c6c 100644 --- a/benchmarks/klee-examples/Makefile +++ b/benchmarks/klee-examples/Makefile @@ -1,13 +1,14 @@ SRC_FILES := $(wildcard ./*.c) +include ../llvm-toolchain.mk all: for SRC in $(SRC_FILES) ; do \ - clang-11 $$SRC -O0 -emit-llvm -S -fno-discard-value-names ; \ + $(LLVM_CC) $$SRC -O0 -emit-llvm -S -fno-discard-value-names ; \ done allO1: for SRC in $(SRC_FILES) ; do \ - clang-11 $$SRC -O1 -emit-llvm -S -fno-discard-value-names -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__ ; \ + $(LLVM_CC) $$SRC -O1 -emit-llvm -S -fno-discard-value-names -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__ ; \ done clean: diff --git a/benchmarks/klee-posix-fs/Makefile b/benchmarks/klee-posix-fs/Makefile index 38e1289d3..1eeac31b2 100644 --- a/benchmarks/klee-posix-fs/Makefile +++ b/benchmarks/klee-posix-fs/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./fd_init.c ./fd.c ./fd_64.c ./gensym.c ./test.c) -CC := clang-11 +include ../llvm-toolchain.mk FLAGS := -emit-llvm -O0 -disable-O0-optnone -c #FLAGS := -emit-llvm -Os -c @@ -24,7 +24,7 @@ gensym: $(GS_LINK_TARGET) #klee-exe: $(KLEE_REPLAY_TARGET) $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< $(GS_LINK_TARGET): $(GS_TARGET) llvm-link-11 -S $(GS_TARGET) -o klee_lib_64.ll diff --git a/benchmarks/llvm/Makefile b/benchmarks/llvm/Makefile index 53996f6ae..5621bebf3 100644 --- a/benchmarks/llvm/Makefile +++ b/benchmarks/llvm/Makefile @@ -1,7 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -# Keep input IR on the x86-64 Linux ABI even when the devcontainer runs on ARM. -CC := clang-11 --target=x86_64-unknown-linux-gnu --sysroot=/usr/x86_64-linux-gnu +include ../llvm-toolchain.mk FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL) @@ -22,13 +21,13 @@ klee: $(KLEE_TARGET) klee-exe: $(KLEE_REPLAY_TARGET) $(KLEE_TARGET): %.bc : %.c - $(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< $(KLEE_REPLAY_TARGET): %-replay : %.c $(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) *.ll diff --git a/benchmarks/llvm/new_multipath/Makefile b/benchmarks/llvm/new_multipath/Makefile index f35eadeed..c27de2533 100644 --- a/benchmarks/llvm/new_multipath/Makefile +++ b/benchmarks/llvm/new_multipath/Makefile @@ -1,13 +1,14 @@ +include ../../llvm-toolchain.mk + all: - clang multi_path_1024_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1024_sym.ll - clang multi_path_65536_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_65536_sym.ll - clang multi_path_1048576_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1048576_sym.ll - clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1024_klee.c -o multi_path_1024_klee.bc - clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee.c -o multi_path_65536_klee.bc - clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee_single.c -o multi_path_65536_klee_single.bc - clang -I /home/kraks/research/klee_experiment/klee-2.1/include -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1048576_klee.c -o multi_path_1048576_klee.bc + $(LLVM_CC) multi_path_1024_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1024_sym.ll + $(LLVM_CC) multi_path_65536_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_65536_sym.ll + $(LLVM_CC) multi_path_1048576_sym.c -g -O0 -emit-llvm -S -fno-discard-value-names -o multi_path_1048576_sym.ll + $(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1024_klee.c -o multi_path_1024_klee.bc + $(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee.c -o multi_path_65536_klee.bc + $(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_65536_klee_single.c -o multi_path_65536_klee_single.bc + $(LLVM_CC) -I $(KLEE_INCL) -g -Xclang -disable-O0-optnone -c -emit-llvm multi_path_1048576_klee.c -o multi_path_1048576_klee.bc clean: rm *.bc rm *.ll - diff --git a/benchmarks/oopsla20/Makefile b/benchmarks/oopsla20/Makefile index 33a845f41..862a82d95 100644 --- a/benchmarks/oopsla20/Makefile +++ b/benchmarks/oopsla20/Makefile @@ -1,20 +1,20 @@ KLEE_INCLUDE = ../../../../klee_experiment/klee-2.1/include +include ../llvm-toolchain.mk all: generate_sse generate_sse: - clang-11 multipath_1024_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1024_sym.ll - clang-11 multipath_65536_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_65536_sym.ll - clang-11 multipath_1048576_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1048576_sym.ll - clang-11 maze_test.c -O0 -emit-llvm -S -fno-discard-value-names -o maze_test.ll + $(LLVM_CC) multipath_1024_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1024_sym.ll + $(LLVM_CC) multipath_65536_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_65536_sym.ll + $(LLVM_CC) multipath_1048576_sym.c -O0 -emit-llvm -S -fno-discard-value-names -o multipath_1048576_sym.ll + $(LLVM_CC) maze_test.c -O0 -emit-llvm -S -fno-discard-value-names -o maze_test.ll generate_klee: - clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1024_klee.c -o multipath_1024_klee.bc - clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_65536_klee.c -o multipath_65536_klee.bc - clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1048576_klee.c -o multipath_1048576_klee.bc - clang-11 -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm maze_test_klee.c -o maze_test_klee.bc + $(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1024_klee.c -o multipath_1024_klee.bc + $(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_65536_klee.c -o multipath_65536_klee.bc + $(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm multipath_1048576_klee.c -o multipath_1048576_klee.bc + $(LLVM_CC) -I $(KLEE_INCLUDE) -g -Xclang -disable-O0-optnone -c -emit-llvm maze_test_klee.c -o maze_test_klee.bc clean: rm *.bc rm *.ll - diff --git a/benchmarks/opt-experiments/Makefile b/benchmarks/opt-experiments/Makefile index 625ebcbfa..ec5439449 100644 --- a/benchmarks/opt-experiments/Makefile +++ b/benchmarks/opt-experiments/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +include ../llvm-toolchain.mk FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL) @@ -21,13 +21,13 @@ klee: $(KLEE_TARGET) klee-exe: $(KLEE_REPLAY_TARGET) $(KLEE_TARGET): %.bc : %.c - $(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< $(KLEE_REPLAY_TARGET): %-replay : %.c $(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) diff --git a/benchmarks/pepm22/ccbse/Makefile b/benchmarks/pepm22/ccbse/Makefile index b5407d140..e8d88eec1 100644 --- a/benchmarks/pepm22/ccbse/Makefile +++ b/benchmarks/pepm22/ccbse/Makefile @@ -1,15 +1,16 @@ SRC_FILES := $(wildcard ./*.c) KLEE_INCLUDE := ../../../../klee_experiment/klee-2.1/include +include ../../llvm-toolchain.mk all: llsc llsc: for SRC in $(SRC_FILES) ; do \ - clang-11 $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \ + $(LLVM_CC) $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \ done klee: for SRC in $(SRC_FILES) ; do \ - clang-11 -D KLEE -I $(KLEE_INCLUDE) -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone $$SRC ; \ + $(LLVM_CC) -D KLEE -I $(KLEE_INCLUDE) -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone $$SRC ; \ done clean: diff --git a/benchmarks/pepm22/concolic/conc/Makefile b/benchmarks/pepm22/concolic/conc/Makefile index c16a25abc..e8775d067 100644 --- a/benchmarks/pepm22/concolic/conc/Makefile +++ b/benchmarks/pepm22/concolic/conc/Makefile @@ -1,9 +1,10 @@ SRC_FILES := $(wildcard ./*.c) +include ../../../llvm-toolchain.mk all: llsc llsc: for SRC in $(SRC_FILES) ; do \ - clang-11 $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \ + $(LLVM_CC) $$SRC -O0 -emit-llvm -S -disable-O0-optnone -fno-discard-value-names ; \ done clean: diff --git a/benchmarks/perf-mon/Makefile b/benchmarks/perf-mon/Makefile index 2cf6a0001..7705c63e7 100644 --- a/benchmarks/perf-mon/Makefile +++ b/benchmarks/perf-mon/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +include ../llvm-toolchain.mk FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL) @@ -21,13 +21,13 @@ klee: $(KLEE_TARGET) klee-exe: $(KLEE_REPLAY_TARGET) $(KLEE_TARGET): %.bc : %.c - $(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $< $(KLEE_REPLAY_TARGET): %-replay : %.c $(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest $(GS_TARGET): %.ll : %.c Makefile - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) diff --git a/benchmarks/test-comp/array-examples/Makefile b/benchmarks/test-comp/array-examples/Makefile index 0f80f6edb..13996e07c 100644 --- a/benchmarks/test-comp/array-examples/Makefile +++ b/benchmarks/test-comp/array-examples/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +include ../../llvm-toolchain.mk FLAGS := -emit-llvm -O2 -Xclang -disable-O0-optnone -c -fno-vectorize GS_FLAGS := -fno-discard-value-names -S @@ -12,7 +12,7 @@ all: gensym gensym: $(GS_TARGET) $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(GS_TARGET) diff --git a/benchmarks/test-comp/array-programs/Makefile b/benchmarks/test-comp/array-programs/Makefile index 0f80f6edb..13996e07c 100644 --- a/benchmarks/test-comp/array-programs/Makefile +++ b/benchmarks/test-comp/array-programs/Makefile @@ -1,6 +1,6 @@ SRC_FILES := $(wildcard ./*.c) -CC := clang-11 +include ../../llvm-toolchain.mk FLAGS := -emit-llvm -O2 -Xclang -disable-O0-optnone -c -fno-vectorize GS_FLAGS := -fno-discard-value-names -S @@ -12,7 +12,7 @@ all: gensym gensym: $(GS_TARGET) $(GS_TARGET): %.ll : %.c - $(CC) $(GS_FLAGS) $(FLAGS) -o $@ $< + $(LLVM_CC) $(GS_FLAGS) $(FLAGS) -o $@ $< clean: $(RM) -rf $(GS_TARGET) diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index 02531f113..b7c43ae7b 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -209,10 +209,7 @@ class Playground extends TestGS { val rtOpt = "--thread=1 --solver=z3" - val cases = (TestCases.filesys).map { t => - t.copy(runOpt = t.runOpt ++ Seq("--solver=z3")) - } - testGS(gs, cases) + testGS(gs, TestPrg(aliasing, "aliasingTest", "@main", noArg, rtOpt, nPath(1))) // FIXME: //testGS(gs, TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0))) From 2d0f394422aa863276d89e1025150e05b0427211 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 02:55:11 -0400 Subject: [PATCH 07/11] add missing file --- benchmarks/llvm-toolchain.mk | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 benchmarks/llvm-toolchain.mk diff --git a/benchmarks/llvm-toolchain.mk b/benchmarks/llvm-toolchain.mk new file mode 100644 index 000000000..a6d3d74e4 --- /dev/null +++ b/benchmarks/llvm-toolchain.mk @@ -0,0 +1,18 @@ +# GenSym models the x86-64 Linux ABI. Keep LLVM input on that ABI while +# compiling the generated C++ runtime natively for the host architecture. +GENSYM_HOST_ARCH ?= $(shell uname -m) +GENSYM_LLVM_TARGET ?= x86_64-unknown-linux-gnu +GENSYM_LLVM_SYSROOT ?= /usr/x86_64-linux-gnu + +CC := clang-11 + +ifneq ($(filter x86_64 amd64,$(GENSYM_HOST_ARCH)),) +LLVM_TARGET_FLAGS := +else +ifeq ($(wildcard $(GENSYM_LLVM_SYSROOT)/include),) +$(error Missing x86-64 cross headers at $(GENSYM_LLVM_SYSROOT)/include; rebuild the devcontainer) +endif +LLVM_TARGET_FLAGS := --target=$(GENSYM_LLVM_TARGET) --sysroot=$(GENSYM_LLVM_SYSROOT) +endif + +LLVM_CC = $(CC) $(LLVM_TARGET_FLAGS) From 7d5da7542a408aef97a04cd812cbf51ecf1ffad5 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 03:04:36 -0400 Subject: [PATCH 08/11] update makefile; first time library compilation is non failure --- src/main/scala/gensym/Driver.scala | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/main/scala/gensym/Driver.scala b/src/main/scala/gensym/Driver.scala index 56b7c87d0..be52d528f 100644 --- a/src/main/scala/gensym/Driver.scala +++ b/src/main/scala/gensym/Driver.scala @@ -100,6 +100,9 @@ abstract class GenericGSDriver[A: Manifest, B: Manifest] |runtime: |\t$$(MAKE) -C $$(RUNTIME_DIR) | + |$$(RUNTIME_LIB): | runtime + |\t@test -f $$@ || { echo "runtime build did not produce $$@" >&2; exit 1; } + | |.SECONDEXPANSION: | |$$(OBJECTS): $$$$(patsubst $$(BUILD_DIR)/%.o,$$(SRC_DIR)/%.cpp,$$$$@) | runtime @@ -110,7 +113,7 @@ abstract class GenericGSDriver[A: Manifest, B: Manifest] |\tmkdir -p $$(@D) |\t$$(CC) -${config.mainFileOpt} -c -o $$@ $$< $$(CXXFLAGS) | - |$$(TARGET): $$(OBJECTS) $$(BUILD_DIR)/$${TARGET}.o $$(RUNTIME_LIB) | runtime + |$$(TARGET): $$(OBJECTS) $$(BUILD_DIR)/$${TARGET}.o $$(RUNTIME_LIB) |\t$$(CC) $$(OPT) -o $$@ $$(OBJECTS) $$(BUILD_DIR)/$${TARGET}.o $$(LDFLAGS) -Wl,--start-group $$(LDLIBS) $$(RUNTIME_LIB) -Wl,--end-group | |clean: From a1933be13b76a190e7cf74ff6692e6817fe17e1f Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 03:15:44 -0400 Subject: [PATCH 09/11] install llvm 11 --- .devcontainer/Dockerfile | 1 + .github/workflows/scala.yml | 2 +- src/test/scala/gensym/TestCases.scala | 9 ++++----- src/test/scala/gensym/TestGS.scala | 10 ++++------ 4 files changed, 10 insertions(+), 12 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 9c4bc264a..5ada5ca43 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -57,6 +57,7 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ perl \ minisat \ clang-11 \ + llvm-11 \ unzip \ build-essential \ && if [ "$(dpkg --print-architecture)" != "amd64" ]; then \ diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml index 732161e42..3250a4b79 100644 --- a/.github/workflows/scala.yml +++ b/.github/workflows/scala.yml @@ -32,7 +32,7 @@ jobs: run: | sudo apt-get update sudo DEBIAN_FRONTEND=noninteractive apt-get install -y git g++ cmake bison flex libboost-all-dev 2to3 python-is-python3 - sudo DEBIAN_FRONTEND=noninteractive apt-get install -y perl minisat curl gnupg2 locales clang-11 wget + sudo DEBIAN_FRONTEND=noninteractive apt-get install -y perl minisat curl gnupg2 locales clang-11 llvm-11 wget - name: Generate test files (LLVM IR) run: | cd benchmarks/llvm diff --git a/src/test/scala/gensym/TestCases.scala b/src/test/scala/gensym/TestCases.scala index 01ed9d86c..95a9c2d88 100644 --- a/src/test/scala/gensym/TestCases.scala +++ b/src/test/scala/gensym/TestCases.scala @@ -167,11 +167,10 @@ object TestCases { TestPrg(stdinTest, "stdinTest", "@main", noArg, "--sym-stdin 10", nPath(2)++status(0)), TestPrg(ioctlTest, "ioctlTest", "@main", noArg, "--add-sym-file A", nPath(1)++status(0)), - // FIXME: temporally commented klee-related tests because it only works for x86 - //TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0)), - //TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0)), - //TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0)), - //TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)), + TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0)), + TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0)), + TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0)), + TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)), ) lazy val coreutils: List[TestPrg] = List( diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index b7c43ae7b..ed66d4fb2 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -208,12 +208,10 @@ class Playground extends TestGS { val gs = new ImpCPSGS val rtOpt = "--thread=1 --solver=z3" - - testGS(gs, TestPrg(aliasing, "aliasingTest", "@main", noArg, rtOpt, nPath(1))) + testGS(gs, TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, rtOpt, nPath(2)++status(0))) // FIXME: - //testGS(gs, TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0))) - //testGS(gs, TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0))) - //testGS(gs, TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0))) - //testGS(gs, TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0))) + testGS(gs, TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, rtOpt, nPath(2)++status(0))) + testGS(gs, TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, rtOpt, nPath(2)++status(0))) + testGS(gs, TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, rtOpt, nPath(10)++status(0))) } From e980b333ea73c082883491a0b39770fdbfb96f20 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 03:29:17 -0400 Subject: [PATCH 10/11] reorg tests --- src/test/scala/gensym/TestCases.scala | 8 ++++++-- src/test/scala/gensym/TestGS.scala | 9 +++------ 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/test/scala/gensym/TestCases.scala b/src/test/scala/gensym/TestCases.scala index 95a9c2d88..a27d64b48 100644 --- a/src/test/scala/gensym/TestCases.scala +++ b/src/test/scala/gensym/TestCases.scala @@ -58,6 +58,9 @@ object TestPrg { import TestPrg._ object TestCases { + val arch = System.getProperty("os.arch") + val isX86_64 = arch == "x86_64" || arch == "amd64" + val concrete: List[TestPrg] = List( //TestPrg(add, "addTest", "@main", noArg, noOpt, nPath(1)), //TestPrg(power, "powerTest", "@main", noArg, noOpt, nPath(1)), @@ -146,6 +149,8 @@ object TestCases { TestPrg(printfTest, "printfTest", "@main", noArg, noOpt, nPath(1)++status(0)) ) + val kleefs: List[TestPrg] = + if (isX86_64) List(TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0))) else List() val filesys: List[TestPrg] = List( TestPrg(openTest, "openTest", "@main", noArg, "--add-sym-file A", nPath(1)++status(0)), TestPrg(openSymTest, "openSymTest", "@main", noArg, "--add-sym-file A --add-sym-file B", nPath(3)++status(0)), @@ -170,8 +175,7 @@ object TestCases { TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, noOpt, nPath(2)++status(0)), TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, noOpt, nPath(2)++status(0)), TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, noOpt, nPath(2)++status(0)), - TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)), - ) + ) ++ kleefs lazy val coreutils: List[TestPrg] = List( TestPrg(echo_linked, "echo_linked_posix", "@main", noMainFileOpt, "--argv=./echo.bc --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)), diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index ed66d4fb2..2df2dc7f6 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -148,6 +148,7 @@ class TestImpCPSGS extends TestGS { testGS(gs, TestPrg(assumeTest, "assumeTestSymUninit", "@main", noArg, rtOpt, nPath(1)++status(0))) testGS(gs, TestPrg(flexAddr, "flexAddrSymUninit", "@main", noArg, rtOpt, nPath(1)++status(0))) testGS(gs, TestPrg(printfTest, "printfTestSymUninit", "@main", noArg, rtOpt, nPath(1)++status(0))) + // FIXME: faultyBstTestSymUninit on CI produces 176 paths (vs 642) // testGS(gs, TestPrg(faultyBst, "faultyBstTestSymUninit", "@main", noArg, rtOpt, nPath(642))) Global.config.symbolicUninit = false @@ -206,12 +207,8 @@ class Playground extends TestGS { import gensym.llvm.parser.Parser._ Global.config.enableOpt val gs = new ImpCPSGS - val rtOpt = "--thread=1 --solver=z3" - testGS(gs, TestPrg(kleefsminiTest, "kleefsmini", "@main", noArg, rtOpt, nPath(2)++status(0))) - // FIXME: - testGS(gs, TestPrg(kleefsminiPackedTest, "kleefsminiPackedTest", "@main", noArg, rtOpt, nPath(2)++status(0))) - testGS(gs, TestPrg(kleefsglobalTest, "kleefsminiglobal", "@main", noArg, rtOpt, nPath(2)++status(0))) - testGS(gs, TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, rtOpt, nPath(10)++status(0))) + val cases = TestCases.symbolicLarge + testGS(gs, cases) } From 76d4d5d70081727d85304dee8e4b66f3b17372ff Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Sat, 15 Aug 2026 16:49:07 -0400 Subject: [PATCH 11/11] remove uesless files --- src/main/scala/gensym/engines/ImpEngine.scala | 411 -------------- .../scala/gensym/engines/PureCPSEngine.scala | 393 -------------- .../scala/gensym/engines/PureEngine.scala | 504 ------------------ .../scala/gensym/states/SymExeState.scala | 194 ------- 4 files changed, 1502 deletions(-) delete mode 100644 src/main/scala/gensym/engines/ImpEngine.scala delete mode 100644 src/main/scala/gensym/engines/PureCPSEngine.scala delete mode 100644 src/main/scala/gensym/engines/PureEngine.scala delete mode 100644 src/main/scala/gensym/states/SymExeState.scala diff --git a/src/main/scala/gensym/engines/ImpEngine.scala b/src/main/scala/gensym/engines/ImpEngine.scala deleted file mode 100644 index 607c75ad3..000000000 --- a/src/main/scala/gensym/engines/ImpEngine.scala +++ /dev/null @@ -1,411 +0,0 @@ -package gensym.imp - -/* -import lms.core._ -import lms.core.Backend._ -import lms.core.virtualize -import lms.macros.SourceContext -import lms.core.stub.{While => _, Global => _, _} - -import gensym._ -import gensym.llvm._ -import gensym.llvm.IR._ -import gensym.llvm.parser.Parser._ -import gensym.IRUtils._ -import gensym.Constants._ -import gensym.{EngineBase, Config, Ctx, Counter} -import gensym.lmsx._ - -import scala.collection.JavaConverters._ -import scala.collection.immutable.{List => StaticList, Map => StaticMap} - -@virtualize -trait ImpGSEngine extends ImpSymExeDefs with EngineBase { - type BFTy = Rep[Ref[SS] => List[(SS, Value)]] - type FFTy = Rep[(Ref[SS], List[Value]) => List[(SS, Value)]] - - def symExecBr(ss: Rep[SS], tCond: Rep[Value], fCond: Rep[Value], - tBlockLab: String, fBlockLab: String)(implicit ctx: Ctx): Rep[List[(SS, Value)]] = { - val tBrFunName = getRealBlockFunName(Ctx(ctx.funName, tBlockLab)) - val fBrFunName = getRealBlockFunName(Ctx(ctx.funName, fBlockLab)) - val curBlockId = Counter.block.get(ctx.toString) - "sym_exec_br".reflectWith[List[(SS, Value)]](ss, curBlockId, tCond, fCond, - unchecked[String](tBrFunName), unchecked[String](fBrFunName)) - } - - def eval(v: LLVMValue, ty: LLVMType, ss: Rep[SS], argTypes: Option[List[LLVMType]] = None)(implicit ctx: Ctx): Rep[Value] = - v match { - case LocalId(x) => ss.lookup(x) - case IntConst(n) => IntV(n, ty.asInstanceOf[IntType].size) - case FloatConst(f) => FloatV(f, ty.asInstanceOf[FloatType].size) - case FloatLitConst(l) => FloatV(l, 80) - case BitCastExpr(from, const, to) => eval(const, to, ss) - case BoolConst(b) => b match { - case true => IntV(1, 1) - case false => IntV(0, 1) - } - case GlobalId(id) if symDefMap.contains(id) => - System.out.println(s"Alias: $id => ${symDefMap(id).const}") - eval(symDefMap(id).const, ty, ss) - case GlobalId(id) if funMap.contains(id) && ExternalFun.shouldRedirect(id) => - val t = funMap(id).header.returnType - ExternalFun.get(id, Some(t), argTypes).get - case GlobalId(id) if funMap.contains(id) => - if (!FunFuns.contains(id)) compile(funMap(id)) - wrapFunV(FunFuns(id)) - case GlobalId(id) if funDeclMap.contains(id) => - val t = funDeclMap(id).header.returnType - ExternalFun.get(id, Some(t), argTypes).getOrElse { - compile(funDeclMap(id), t, argTypes.get) - wrapFunV(FunFuns(getMangledFunctionName(funDeclMap(id), argTypes.get))) - } - case GlobalId(id) if globalDefMap.contains(id) => - heapEnv(id)() - case GlobalId(id) if globalDeclMap.contains(id) => - System.out.println(s"Warning: globalDecl $id is ignored") - ty match { - case PtrType(_, _) => NullLoc() - case _ => NullPtr[Value] - } - case GetElemPtrExpr(_, baseType, ptrType, const, typedConsts) => - // typedConst are not all int, could be local id - val vs = typedConsts.map(tv => eval(tv.const, tv.ty, ss)) - val offset = calculateOffset(ptrType, vs) - eval(const, ptrType, ss).asRepOf[LocV] + offset - case IntToPtrExpr(from, value, to) => eval(value, from, ss) - case PtrToIntExpr(from, value, IntType(toSize)) => - val v = eval(value, from, ss) - if (ARCH_WORD_SIZE == toSize) v else v.trunc(ARCH_WORD_SIZE, toSize) - case FCmpExpr(pred, ty1, ty2, lhs, rhs) if ty1 == ty2 => evalFloatOp2(pred.op, lhs, rhs, ty1, ss) - case ICmpExpr(pred, ty1, ty2, lhs, rhs) if ty1 == ty2 => evalIntOp2(pred.op, lhs, rhs, ty1, ss) - case InlineASM() => NullPtr[Value] - case ZeroInitializerConst => - System.out.println("Warning: Evaluate zeroinitialize in body") - NullPtr[Value] // FIXME: use uninitValue - case NullConst => NullLoc() - case NoneConst => NullPtr[Value] - } - - def evalIntOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType, ss: Rep[SS])(implicit ctx: Ctx): Rep[Value] = - IntOp2(op, eval(lhs, ty, ss), eval(rhs, ty, ss)) - - def evalFloatOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType, ss: Rep[SS])(implicit ctx: Ctx): Rep[Value] = - FloatOp2(op, eval(lhs, ty, ss), eval(rhs, ty, ss)) - - def execValueInst(inst: ValueInstruction, ss: Rep[SS], k: (Rep[SS], Rep[Value]) => Rep[List[(SS, Value)]])(implicit ctx: Ctx): Rep[List[(SS, Value)]] = { - inst match { - // Memory Access Instructions - case AllocaInst(ty, align) => - val typeSize = ty.size - val sz = ss.stackSize - ss.allocStack(typeSize, align.n) - k(ss, LocV(sz, LocV.kStack, typeSize.toLong)) - case LoadInst(valTy, ptrTy, value, align) => - val isStruct = getRealType(valTy) match { - case Struct(types) => 1 - case _ => 0 - } - val v = eval(value, ptrTy, ss) - k(ss, ss.lookup(v, valTy.size, isStruct)) - case GetElemPtrInst(_, baseType, ptrType, ptrValue, typedValues) => - val vs = typedValues.map(tv => eval(tv.value, tv.ty, ss)) - val offset = calculateOffset(ptrType, vs) - val v = eval(ptrValue, ptrType, ss).asRepOf[LocV] + offset - k(ss, v) - // Arith Unary Operations - case FNegInst(ty, op) => k(ss, evalFloatOp2("fsub", FloatConst(-0.0), op, ty, ss)) - // Arith Binary Operations - case AddInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("add", lhs, rhs, ty, ss)) - case SubInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("sub", lhs, rhs, ty, ss)) - case MulInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("mul", lhs, rhs, ty, ss)) - case SDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("sdiv", lhs, rhs, ty, ss)) - case UDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("udiv", lhs, rhs, ty, ss)) - case FAddInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fadd", lhs, rhs, ty, ss)) - case FSubInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fsub", lhs, rhs, ty, ss)) - case FMulInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fmul", lhs, rhs, ty, ss)) - case FDivInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fdiv", lhs, rhs, ty, ss)) - /* Backend Work Needed */ - case URemInst(ty, lhs, rhs) => k(ss, evalIntOp2("urem", lhs, rhs, ty, ss)) - case SRemInst(ty, lhs, rhs) => k(ss, evalIntOp2("srem", lhs, rhs, ty, ss)) - - // Bitwise Operations - /* Backend Work Needed */ - case ShlInst(ty, lhs, rhs) => k(ss, evalIntOp2("shl", lhs, rhs, ty, ss)) - case LshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("lshr", lhs, rhs, ty, ss)) - case AshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("ashr", lhs, rhs, ty, ss)) - case AndInst(ty, lhs, rhs) => k(ss, evalIntOp2("and", lhs, rhs, ty, ss)) - case OrInst(ty, lhs, rhs) => k(ss, evalIntOp2("or", lhs, rhs, ty, ss)) - case XorInst(ty, lhs, rhs) => k(ss, evalIntOp2("xor", lhs, rhs, ty, ss)) - - // Conversion Operations - /* Backend Work Needed */ - case ZExtInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).zExt(size)) - case SExtInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).sExt(size)) - case TruncInst(from@IntType(fromSz), value, IntType(toSz)) => - k(ss, eval(value, from, ss).trunc(fromSz, toSz)) - case FpExtInst(from, value, to) => - k(ss, eval(value, from, ss)) - case FpToUIInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).fromFloatToUInt(size)) - case FpToSIInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).fromFloatToSInt(size)) - case UiToFPInst(from, value, to) => - k(ss, eval(value, from, ss).fromUIntToFloat) - case SiToFPInst(from, value, to) => - k(ss, eval(value, from, ss).fromSIntToFloat) - case PtrToIntInst(from, value, IntType(toSize)) => - val v = eval(value, from, ss) - k(ss, if (ARCH_WORD_SIZE == toSize) v else v.trunc(ARCH_WORD_SIZE, toSize)) - case IntToPtrInst(from, value, to) => - k(ss, eval(value, from, ss)) - case BitCastInst(from, value, to) => - k(ss, eval(value, to, ss)) - - // Aggregate Operations - /* Backend Work Needed */ - case ExtractValueInst(ty, struct, indices) => - val idxList = indices.asInstanceOf[List[IntConst]].map(x => x.n) - val idx = calculateOffsetStatic(ty, idxList) - // v is expected to be StructV in backend - val v = eval(struct, ty, ss) - k(ss, v.structAt(idx)) - - // Other operations - case FCmpInst(pred, ty, lhs, rhs) => k(ss, evalFloatOp2(pred.op, lhs, rhs, ty, ss)) - case ICmpInst(pred, ty, lhs, rhs) => k(ss, evalIntOp2(pred.op, lhs, rhs, ty, ss)) - case CallInst(ty, f, args) => - val argValues: List[LLVMValue] = extractValues(args) - val argTypes: List[LLVMType] = extractTypes(args) - val fv = eval(f, VoidType, ss, Some(argTypes)) - val vs = argValues.zip(argTypes).map { - case (v, t) => eval(v, t, ss) - } - ss.push - val stackSize = ss.stackSize - val res = fv[Ref](ss, List(vs: _*)) - res.flatMap { case sv => - val s: Rep[Ref[SS]] = sv._1 - s.pop(stackSize) - k(s, sv._2) - } - case PhiInst(ty, incs) => - def selectValue(bb: Rep[BlockLabel], vs: List[() => Rep[Value]], labels: List[BlockLabel]): Rep[Value] = { - if (bb == labels(0) || labels.length == 1) vs(0)() - else selectValue(bb, vs.tail, labels.tail) - } - val incsValues: List[LLVMValue] = incs.map(_.value) - val incsLabels: List[BlockLabel] = incs.map(i => Counter.block.get(ctx.withBlock(i.label))) - val vs = incsValues.map(v => () => eval(v, ty, ss)) - k(ss, selectValue(ss.incomingBlock, vs, incsLabels)) - case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) if Global.config.iteSelect => - k(ss, ITE(eval(cndVal, cndTy, ss), eval(thnVal, thnTy, ss), eval(elsVal, elsTy, ss))) - case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) => - val cnd = eval(cndVal, cndTy, ss) - // FIXME: `fun` should result in a local function in scope, but now it generates code elsewhere. - // a workaround is to use topFun to lift it to a global function - val repK = topFun(k) - if (cnd.isConc) { - if (cnd.int == 1) repK(ss, eval(thnVal, thnTy, ss)) - else repK(ss, eval(elsVal, elsTy, ss)) - } else { - // TODO: check cond via solver - val s1 = ss.fork - ss.addPC(cnd) - s1.addPC(!cnd) - Coverage.incPath(1) - repK(ss, eval(thnVal, thnTy, ss)) ++ repK(s1, eval(elsVal, elsTy, s1)) - } - } - } - - // Note: Comp[E, Rep[Value]] vs Comp[E, Rep[Option[Value]]]? - def execTerm(inst: Terminator)(implicit ss: Rep[SS], ctx: Ctx): Rep[List[(SS, Value)]] = { - inst match { - // FIXME: unreachable - case Unreachable => IntV(-1) - case RetTerm(ty, v) => - v match { - case Some(value) => eval(value, ty, ss) - case None => NullPtr[Value] - } - case BrTerm(lab) if (cfg.pred(ctx.funName, lab).size == 1) => - execBlockEager(findBlock(ctx.funName, lab).get, ss)(Ctx(ctx.funName, lab)) - case BrTerm(lab) => - ss.addIncomingBlock(ctx) - execBlock(ctx.funName, lab, ss) - case CondBrTerm(ty, cnd, thnLab, elsLab) => - Counter.setBranchNum(ctx, 2) - ss.addIncomingBlock(ctx) - val cndVal = eval(cnd, ty, ss) - if (cndVal.isConc) { - if (cndVal.int == 1) { - Coverage.incBranch(ctx, 0) - execBlock(ctx.funName, thnLab, ss) - } else { - Coverage.incBranch(ctx, 1) - execBlock(ctx.funName, elsLab, ss) - } - } else { - symExecBr(ss, cndVal, !cndVal, thnLab, elsLab) - } - case SwitchTerm(cndTy, cndVal, default, swTable) => - Counter.setBranchNum(ctx, swTable.size+1) - def switch(v: Rep[Long], s: Rep[SS], table: List[LLVMCase]): Rep[List[(SS, Value)]] = { - if (table.isEmpty) { - Coverage.incBranch(ctx, swTable.size) - execBlock(ctx.funName, default, s) - } else { - if (v == table.head.n) { - Coverage.incBranch(ctx, swTable.size - table.size) - execBlock(ctx.funName, table.head.label, s) - } else switch(v, s, table.tail) - } - } - - val nPath: Var[Int] = var_new(0) - def switchSym(v: Rep[Value], s: Rep[SS], table: List[LLVMCase]): Rep[List[(SS, Value)]] = - if (table.isEmpty) { - if (checkPC(s.pc)) { - nPath += 1 - val new_ss = if (1 == nPath) s else s.fork - Coverage.incBranch(ctx, swTable.size) - execBlock(ctx.funName, default, new_ss) - } else List[(SS, Value)]() - } else { - val st = s.copy - val headPC = IntOp2("eq", v, IntV(table.head.n)) - s.addPC(headPC) - val lt = if (checkPC(s.pc)) { - nPath += 1 - val new_ss = if (1 == nPath) s else s.fork - Coverage.incBranch(ctx, swTable.size - table.size) - execBlock(ctx.funName, table.head.label, new_ss) - } else List[(SS, Value)]() - st.addPC(!headPC) - val lf = switchSym(v, st, table.tail) - lt ++ lf - } - - ss.addIncomingBlock(ctx) - val v = eval(cndVal, cndTy, ss) - if (v.isConc) switch(v.int, ss, swTable) - else { - val r = switchSym(v, ss, swTable) - if (nPath > 0) Coverage.incPath(nPath - 1) - r - } - } - } - - def execInst(inst: Instruction, ss: Rep[SS], k: Rep[SS] => Rep[List[(SS, Value)]])(implicit ctx: Ctx): Rep[List[(SS, Value)]] = { - inst match { - case AssignInst(x, valInst) => - execValueInst(valInst, ss, { - case (s, v) => - s.assign(x, v) - k(s) - }) - case StoreInst(ty1, val1, ty2, val2, align) => - val v1 = eval(val1, ty1, ss) - val v2 = eval(val2, ty2, ss) - ss.update(v2, v1, ty1.size) - k(ss) - case CallInst(ty, f, args) => - val argValues: List[LLVMValue] = extractValues(args) - val argTypes: List[LLVMType] = extractTypes(args) - val fv = eval(f, VoidType, ss, Some(argTypes)) - val vs = argValues.zip(argTypes).map { - case (v, t) => eval(v, t, ss) - } - ss.push - val stackSize = ss.stackSize - val res: Rep[List[(SS, Value)]] = fv[Ref](ss, List(vs: _*)) - res.flatMap { case sv => - val s = sv._1 - s.pop(stackSize) - k(s) - } - } - } - - def execBlock(funName: String, label: String, s: Rep[SS]): Rep[List[(SS, Value)]] = - execBlock(funName, findBlock(funName, label).get, s) - - def execBlock(funName: String, block: BB, s: Rep[SS]): Rep[List[(SS, Value)]] = { - info("jump to block: " + block.label.get) - getBBFun(funName, block)(s) - } - - def execBlockEager(block: BB, s: Rep[SS])(implicit ctx: Ctx): Rep[List[(SS, Value)]] = { - def runInst(insts: List[Instruction], t: Terminator, s: Rep[SS]): Rep[List[(SS, Value)]] = - insts match { - case Nil => execTerm(t)(s, ctx) - case i::inst => execInst(i, s, s1 => runInst(inst, t, s1))(ctx) - } - s.coverBlock(ctx) - runInst(block.ins, block.term, s) - } - - override def repBlockFun(b: BB)(implicit ctx: Ctx): BFTy = { - def runBlock(ss: Rep[Ref[SS]]): Rep[List[(SS, Value)]] = { - info("running block: " + ctx.funName + " - " + b.label.get) - execBlockEager(b, ss) - } - topFun(runBlock(_)) - } - - override def repFunFun(f: FunctionDef): FFTy = { - def runFun(ss: Rep[Ref[SS]], args: Rep[List[Value]]): Rep[List[(SS, Value)]] = { - implicit val ctx = Ctx(f.id, f.blocks(0).label.get) - val params: List[String] = extractNames(f.header.params) - info("running function: " + f.id) - ss.assign(params, args) - execBlockEager(f.blocks(0), ss) - } - topFun(runFun(_, _)) - } - - override def repExternFun(f: FunctionDecl, retTy: LLVMType, argTypes: List[LLVMType]): FFTy = { - def generateNativeCall(ss: Rep[Ref[SS]], args: Rep[List[Value]]): Rep[List[(SS, Value)]] = { - info("running native function: " + f.id) - val nativeArgs: List[Rep[Any]] = argTypes.zipWithIndex.map { - case (ty@PtrType(_, _), id) => ss.getPointerArg(args(id)).castToM(ty.toManifest) - case (ty@IntType(size), id) => ss.getIntArg(args(id)).castToM(ty.toManifest) - case (ty@FloatType(k), id) => ss.getFloatArg(args(id)).castToM(ty.toManifest) - case _ => throw new Exception("Unknown native argument type") - } - val ptrArgIndices: List[Int] = argTypes.zipWithIndex.filter { - case (ty, id) => ty.isInstanceOf[PtrType] - }.map(_._2) - val fv = NativeExternalFun(f.id.tail, Some(retTy)) - val nativeRet = fv(nativeArgs).castToM(retTy.toManifest) - ptrArgIndices.foreach { id => - ss.writebackPointerArg(nativeRet, args(id), nativeArgs(id).asRepOf[Ptr[Char]]) - } - val retVal = retTy match { - case IntType(size) => IntV(nativeRet.asInstanceOf[Rep[Long]], size) - case f@FloatType(_) => FloatV(nativeRet.asInstanceOf[Rep[Double]], f.size) - case _ => throw new Exception("Unknown native return type") - } - List[(SS, Value)](Tuple2(ss, retVal)) - } - topFun(generateNativeCall(_, _)) - } - - override def wrapFunV(f: FFTy): Rep[Value] = FunV[Ref](f) - - def exec(fname: String, args: Rep[List[Value]]): Rep[List[(SS, Value)]] = { - implicit val ctx = Ctx(fname, findFirstBlock(fname).label.get) - val preHeap: Rep[List[Value]] = List(precompileHeapLists(m::Nil):_*) - Coverage.incPath(1) - val ss = initState(preHeap.asRepOf[Mem]) - val fv = eval(GlobalId(fname), VoidType, ss) - ss.push - ss.updateArg - ss.initErrorLoc - fv[Ref](ss, args) - } -} -*/ \ No newline at end of file diff --git a/src/main/scala/gensym/engines/PureCPSEngine.scala b/src/main/scala/gensym/engines/PureCPSEngine.scala deleted file mode 100644 index 1a20a8004..000000000 --- a/src/main/scala/gensym/engines/PureCPSEngine.scala +++ /dev/null @@ -1,393 +0,0 @@ -package gensym - -/* -import lms.core._ -import lms.core.Backend._ -import lms.core.virtualize -import lms.macros.SourceContext -import lms.core.stub.{While => _, _} - -import gensym.llvm._ -import gensym.llvm.IR._ -import gensym.llvm.parser.Parser._ -import gensym.IRUtils._ -import gensym.Constants._ -import gensym.lmsx._ - -import scala.collection.JavaConverters._ -import scala.collection.immutable.{List => StaticList, Map => StaticMap} - -@virtualize -trait PureCPSGSEngine extends SymExeDefs with EngineBase { - type BFTy = Rep[(SS, Cont) => Unit] - type FFTy = Rep[(SS, List[Value], Cont) => Unit] - - def symExecBr(ss: Rep[SS], tCond: Rep[Value], fCond: Rep[Value], - tBlockLab: String, fBlockLab: String, k: Rep[Cont])(implicit ctx: Ctx): Rep[Unit] = { - val tBrFunName = getRealBlockFunName(Ctx(ctx.funName, tBlockLab)) - val fBrFunName = getRealBlockFunName(Ctx(ctx.funName, fBlockLab)) - val curBlockId = Counter.block.get(ctx.toString) - "sym_exec_br_k".reflectWriteWith[Unit](ss, curBlockId, tCond, fCond, - unchecked[String](tBrFunName), unchecked[String](fBrFunName), k)(Adapter.CTRL) - } - - def addIncomingBlockOpt(ss: Rep[SS], tos: StaticList[String])(implicit ctx: Ctx): Rep[SS] = - ss.addIncomingBlock(ctx) - /* - (tos.exists(to => findBlock(funName, to).get.hasPhi)) match { - case true => ss.addIncomingBlock(from) - case _ => ss - } - */ - - def eval(v: LLVMValue, ty: LLVMType, ss: Rep[SS], argTypes: Option[List[LLVMType]] = None)(implicit ctx: Ctx): Rep[Value] = - v match { - case LocalId(x) => ss.lookup(x) - case IntConst(n) => IntV(n, ty.asInstanceOf[IntType].size) - case FloatConst(f) => FloatV(f, ty.asInstanceOf[FloatType].size) - case FloatLitConst(l) => FloatV(l, 80) - case BitCastExpr(from, const, to) => eval(const, to, ss) - case BoolConst(b) => b match { - case true => IntV(1, 1) - case false => IntV(0, 1) - } - case GlobalId(id) if symDefMap.contains(id) => - System.out.println(s"Alias: $id => ${symDefMap(id).const}") - eval(symDefMap(id).const, ty, ss) - case GlobalId(id) if funMap.contains(id) && ExternalFun.shouldRedirect(id) => - val t = funMap(id).header.returnType - ExternalFun.get(id, Some(t), argTypes).get - case GlobalId(id) if funMap.contains(id) => - if (!FunFuns.contains(id)) compile(funMap(id)) - wrapFunV(FunFuns(id)) - case GlobalId(id) if funDeclMap.contains(id) => - val t = funDeclMap(id).header.returnType - ExternalFun.get(id, Some(t), argTypes).getOrElse { - compile(funDeclMap(id), t, argTypes.get) - wrapFunV(FunFuns(getMangledFunctionName(funDeclMap(id), argTypes.get))) - } - case GlobalId(id) if globalDefMap.contains(id) => - heapEnv(id)() - case GlobalId(id) if globalDeclMap.contains(id) => - System.out.println(s"Warning: globalDecl $id is ignored") - ty match { - case PtrType(_, _) => NullLoc() - case _ => NullPtr[Value] - } - case GetElemPtrExpr(_, baseType, ptrType, const, typedConsts) => - // typedConst are not all int, could be local id - val vs = typedConsts.map(tv => eval(tv.const, tv.ty, ss)) - val offset = calculateOffset(ptrType, vs) - eval(const, ptrType, ss).asRepOf[LocV] + offset - case IntToPtrExpr(from, value, to) => eval(value, from, ss) - case PtrToIntExpr(from, value, IntType(toSize)) => - val v = eval(value, from, ss) - if (ARCH_WORD_SIZE == toSize) v else v.trunc(ARCH_WORD_SIZE, toSize) - case FCmpExpr(pred, ty1, ty2, lhs, rhs) if ty1 == ty2 => evalFloatOp2(pred.op, lhs, rhs, ty1, ss) - case ICmpExpr(pred, ty1, ty2, lhs, rhs) if ty1 == ty2 => evalIntOp2(pred.op, lhs, rhs, ty1, ss) - case InlineASM() => NullPtr[Value] - case ZeroInitializerConst => - System.out.println("Warning: Evaluate zeroinitialize in body") - NullPtr[Value] // FIXME: use uninitValue - case NullConst => NullLoc() - case NoneConst => NullPtr[Value] - case UndefConst => IntV(0, ty.asInstanceOf[IntType].size) - case v => System.out.println(ty, v); ??? - } - - def evalIntOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType, ss: Rep[SS])(implicit ctx: Ctx): Rep[Value] = - IntOp2(op, eval(lhs, ty, ss), eval(rhs, ty, ss)) - - def evalFloatOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType, ss: Rep[SS])(implicit ctx: Ctx): Rep[Value] = - FloatOp2(op, eval(lhs, ty, ss), eval(rhs, ty, ss)) - - def execValueInst(inst: ValueInstruction, ss: Rep[SS], k: (Rep[SS], Rep[Value]) => Rep[Unit])(implicit ctx: Ctx): Rep[Unit] = { - //System.out.println(funName, inst) - inst match { - // Memory Access Instructions - case AllocaInst(ty, align) => - val typeSize = ty.size - val ss2 = ss.allocStack(typeSize, align.n) - k(ss2, LocV(ss2.stackSize - typeSize, LocV.kStack, typeSize.toLong)) - case LoadInst(valTy, ptrTy, value, align) => - val isStruct = getRealType(valTy) match { - case Struct(types) => 1 - case _ => 0 - } - val v = eval(value, ptrTy, ss) - k(ss, ss.lookup(v, valTy.size, isStruct)) - case GetElemPtrInst(_, baseType, ptrType, ptrValue, typedValues) => - val vs = typedValues.map(tv => eval(tv.value, tv.ty, ss)) - val offset = calculateOffset(ptrType, vs) - val v = eval(ptrValue, ptrType, ss).asRepOf[LocV] + offset - k(ss, v) - // Arith Unary Operations - case FNegInst(ty, op) => k(ss, evalFloatOp2("fsub", FloatConst(-0.0), op, ty, ss)) - // Arith Binary Operations - case AddInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("add", lhs, rhs, ty, ss)) - case SubInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("sub", lhs, rhs, ty, ss)) - case MulInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("mul", lhs, rhs, ty, ss)) - case SDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("sdiv", lhs, rhs, ty, ss)) - case UDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("udiv", lhs, rhs, ty, ss)) - case FAddInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fadd", lhs, rhs, ty, ss)) - case FSubInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fsub", lhs, rhs, ty, ss)) - case FMulInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fmul", lhs, rhs, ty, ss)) - case FDivInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fdiv", lhs, rhs, ty, ss)) - /* Backend Work Needed */ - case URemInst(ty, lhs, rhs) => k(ss, evalIntOp2("urem", lhs, rhs, ty, ss)) - case SRemInst(ty, lhs, rhs) => k(ss, evalIntOp2("srem", lhs, rhs, ty, ss)) - - // Bitwise Operations - /* Backend Work Needed */ - case ShlInst(ty, lhs, rhs) => k(ss, evalIntOp2("shl", lhs, rhs, ty, ss)) - case LshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("lshr", lhs, rhs, ty, ss)) - case AshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("ashr", lhs, rhs, ty, ss)) - case AndInst(ty, lhs, rhs) => k(ss, evalIntOp2("and", lhs, rhs, ty, ss)) - case OrInst(ty, lhs, rhs) => k(ss, evalIntOp2("or", lhs, rhs, ty, ss)) - case XorInst(ty, lhs, rhs) => k(ss, evalIntOp2("xor", lhs, rhs, ty, ss)) - - // Conversion Operations - /* Backend Work Needed */ - case ZExtInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).zExt(size)) - case SExtInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).sExt(size)) - case TruncInst(from@IntType(fromSz), value, IntType(toSz)) => - k(ss, eval(value, from, ss).trunc(fromSz, toSz)) - case FpExtInst(from, value, to) => - k(ss, eval(value, from, ss)) - case FpToUIInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).fromFloatToUInt(size)) - case FpToSIInst(from, value, IntType(size)) => - k(ss, eval(value, from, ss).fromFloatToSInt(size)) - case UiToFPInst(from, value, to) => - k(ss, eval(value, from, ss).fromUIntToFloat) - case SiToFPInst(from, value, to) => - k(ss, eval(value, from, ss).fromSIntToFloat) - case PtrToIntInst(from, value, IntType(toSize)) => - val v = eval(value, from, ss) - k(ss, if (ARCH_WORD_SIZE == toSize) v else v.trunc(ARCH_WORD_SIZE, toSize)) - case IntToPtrInst(from, value, to) => - k(ss, eval(value, from, ss)) - case BitCastInst(from, value, to) => - k(ss, eval(value, to, ss)) - - // Aggregate Operations - /* Backend Work Needed */ - case ExtractValueInst(ty, struct, indices) => - val idxList = indices.asInstanceOf[List[IntConst]].map(x => x.n) - val idx = calculateOffsetStatic(ty, idxList) - // v is expected to be StructV in backend - val v = eval(struct, ty, ss) - k(ss, v.structAt(idx)) - - // Other operations - case FCmpInst(pred, ty, lhs, rhs) => k(ss, evalFloatOp2(pred.op, lhs, rhs, ty, ss)) - case ICmpInst(pred, ty, lhs, rhs) => k(ss, evalIntOp2(pred.op, lhs, rhs, ty, ss)) - case CallInst(ty, f, args) => - val argValues: List[LLVMValue] = extractValues(args) - val argTypes: List[LLVMType] = extractTypes(args) - val fv = eval(f, VoidType, ss, Some(argTypes)) - val vs = argValues.zip(argTypes).map { case (v, t) => eval(v, t, ss) } - def fK(s: Rep[SS], v: Rep[Value]): Rep[Unit] = k(s.pop(ss.stackSize), v) - fv[Id](ss.push, List(vs: _*), ContOpt[Id](fK)) - case PhiInst(ty, incs) => - def selectValue(bb: Rep[BlockLabel], vs: List[() => Rep[Value]], labels: List[BlockLabel]): Rep[Value] = { - if (bb == labels(0) || labels.length == 1) vs(0)() - else selectValue(bb, vs.tail, labels.tail) - } - val incsValues: List[LLVMValue] = incs.map(_.value) - val incsLabels: List[BlockLabel] = incs.map(i => Counter.block.get(ctx.withBlock(i.label))) - val vs = incsValues.map(v => () => eval(v, ty, ss)) - k(ss, selectValue(ss.incomingBlock, vs, incsLabels)) - case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) if Global.config.iteSelect => - k(ss, ITE(eval(cndVal, cndTy, ss), eval(thnVal, thnTy, ss), eval(elsVal, elsTy, ss))) - case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) => - val cnd = eval(cndVal, cndTy, ss) - val repK = fun(k) - if (cnd.isConc) { - if (cnd.int == 1) repK(ss, eval(thnVal, thnTy, ss)) - else repK(ss, eval(elsVal, elsTy, ss)) - } else { - // TODO: check cond via solver - Coverage.incPath(1) - repK(ss, eval(thnVal, thnTy, ss.addPC(cnd))) - repK(ss, eval(elsVal, elsTy, ss.fork.addPC(!cnd))) - } - } - } - - def asyncExecBlock(funName: String, lab: String, ss: Rep[SS], k: Rep[Cont]): Rep[Unit] = { - val block = Adapter.g.reifyHere(Unwrap(execBlock(funName, lab, ss, k))) - val (rdKeys, wrKeys) = Adapter.g.getEffKeys(block) - Wrap[Unit](Adapter.g.reflectEffectSummaryHere("async_exec_block", Unwrap(ss.getSSid), block)((rdKeys, wrKeys + Adapter.CTRL))) - } - - def execTerm(inst: Terminator, k: Rep[Cont])(implicit ss: Rep[SS], ctx: Ctx): Rep[Unit] = { - inst match { - // FIXME: unreachable - case Unreachable => k(ss, IntV(-1)) - case RetTerm(ty, v) => - val ret = v match { - case Some(value) => eval(value, ty, ss) - case None => NullPtr[Value] - } - k(ss, ret) - case BrTerm(lab) if (cfg.pred(ctx.funName, lab).size == 1) => - execBlockEager(findBlock(ctx.funName, lab).get, ss, k)(Ctx(ctx.funName, lab)) - case BrTerm(lab) => - execBlock(ctx.funName, lab, addIncomingBlockOpt(ss, StaticList(lab)), k) - case CondBrTerm(ty, cnd, thnLab, elsLab) => - Counter.setBranchNum(ctx, 2) - val cndVal = eval(cnd, ty, ss) - // FIXME: using addIncomingBlockOpt triggers some issue of recursive functions - val ss1 = ss.addIncomingBlock(ctx) - if (cndVal.isConc) { - if (cndVal.int == 1) { - Coverage.incBranch(ctx, 0) - asyncExecBlock(ctx.funName, thnLab, ss1, k) - } - else { - Coverage.incBranch(ctx, 1) - asyncExecBlock(ctx.funName, elsLab, ss1, k) - } - } else { - symExecBr(ss1, cndVal, !cndVal, thnLab, elsLab, k) - } - case SwitchTerm(cndTy, cndVal, default, swTable) => - Counter.setBranchNum(ctx, swTable.size+1) - def switch(v: Rep[Long], s: Rep[SS], table: List[LLVMCase]): Rep[Unit] = - if (table.isEmpty) { - Coverage.incBranch(ctx, swTable.size) - execBlock(ctx.funName, default, s, k) - } else { - if (v == table.head.n) { - Coverage.incBranch(ctx, swTable.size - table.size) - execBlock(ctx.funName, table.head.label, s, k) - } else switch(v, s, table.tail) - } - - val nPath: Var[Int] = var_new(0) - def switchSym(v: Rep[Value], s: Rep[SS], table: List[LLVMCase]): Rep[Unit] = - if (table.isEmpty) { - if (checkPC(s.pc)) { - nPath += 1 - val new_ss = if (1 == nPath) s else s.fork - Coverage.incBranch(ctx, swTable.size) - execBlock(ctx.funName, default, new_ss, k) - } - } else { - val headPC = IntOp2("eq", v, IntV(table.head.n)) - if (checkPC(s.pc.addPC(headPC))) { - nPath += 1 - val new_ss = if (1 == nPath) s else s.fork - Coverage.incBranch(ctx, swTable.size - table.size) - execBlock(ctx.funName, table.head.label, new_ss.addPC(headPC), k) - } - switchSym(v, s.addPC(!headPC), table.tail) - } - - val ss1 = addIncomingBlockOpt(ss, default::swTable.map(_.label)) - val v = eval(cndVal, cndTy, ss1) - if (v.isConc) switch(v.int, ss1, swTable) - else { - switchSym(v, ss1, swTable) - if (nPath > 0) Coverage.incPath(nPath - 1) - () - } - } - } - - def execInst(inst: Instruction, ss: Rep[SS], k: Rep[SS] => Rep[Unit])(implicit ctx: Ctx): Rep[Unit] = { - //System.out.println(funName, inst) - inst match { - case AssignInst(x, valInst) => - execValueInst(valInst, ss, { case (s, v) => k(s.assign(x, v)) }) - case StoreInst(ty1, val1, ty2, val2, align) => - val v1 = eval(val1, ty1, ss) - val v2 = eval(val2, ty2, ss) - k(ss.update(v2, v1, ty1.size)) - case CallInst(ty, f, args) => - val argValues: List[LLVMValue] = extractValues(args) - val argTypes: List[LLVMType] = extractTypes(args) - val fv = eval(f, VoidType, ss, Some(argTypes)) - val vs = argValues.zip(argTypes).map { case (v, t) => eval(v, t, ss) } - def fK(s: Rep[SS], v: Rep[Value]): Rep[Unit] = k(s.pop(ss.stackSize)) - fv[Id](ss.push, List(vs: _*), ContOpt[Id](fK)) - } - } - - def execBlock(funName: String, label: String, s: Rep[SS], k: Rep[Cont]): Rep[Unit] = - execBlock(funName, findBlock(funName, label).get, s, k) - - def execBlock(funName: String, block: BB, s: Rep[SS], k: Rep[Cont]): Rep[Unit] = { - info("jump to block: " + block.label.get) - getBBFun(funName, block)(s, k) - } - - def execBlockEager(block: BB, s: Rep[SS], k: Rep[Cont])(implicit ctx: Ctx): Rep[Unit] = { - def runInst(insts: List[Instruction], t: Terminator, s: Rep[SS], k: Rep[Cont]): Rep[Unit] = - insts match { - case Nil => execTerm(t, k)(s, ctx) - case i::inst => execInst(i, s, s1 => runInst(inst, t, s1, k))(ctx) - } - runInst(block.ins, block.term, s.coverBlock(ctx), k) - } - - override def repBlockFun(b: BB)(implicit ctx: Ctx): BFTy = { - def runBlock(ss: Rep[SS], k: Rep[Cont]): Rep[Unit] = { - info("running block: " + ctx) - execBlockEager(b, ss, k) - } - topFun(runBlock(_, _)) - } - - override def repFunFun(f: FunctionDef): FFTy = { - def runFun(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] = { - implicit val ctx = Ctx(f.id, f.blocks(0).label.get) - val params: List[String] = extractNames(f.header.params) - info("running function: " + f.id) - execBlockEager(f.blocks(0), ss.assign(params, args), k) - } - topFun(runFun(_, _, _)) - } - - override def repExternFun(f: FunctionDecl, retTy: LLVMType, argTypes: List[LLVMType]): FFTy = { - def generateNativeCall(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] = { - info("running native function: " + f.id) - val nativeArgs: List[Rep[Any]] = argTypes.zipWithIndex.map { - case (ty@PtrType(_, _), id) => ss.getPointerArg(args(id)).castToM(ty.toManifest) - case (ty@IntType(size), id) => ss.getIntArg(args(id)).castToM(ty.toManifest) - case (ty@FloatType(k), id) => ss.getFloatArg(args(id)).castToM(ty.toManifest) - case _ => throw new Exception("Unknown native argument type") - } - val ptrArgIndices: List[Int] = argTypes.zipWithIndex.filter { - case (ty, id) => ty.isInstanceOf[PtrType] - }.map(_._2) - val fv = NativeExternalFun(f.id.tail, Some(retTy)) - val nativeRet = fv(nativeArgs).castToM(retTy.toManifest) - val retSs = ptrArgIndices.foldLeft(ss) { case (state, id) => - state.writebackPointerArg(nativeRet, args(id), nativeArgs(id).asRepOf[Ptr[Char]]) - } - val retVal = retTy match { - case IntType(size) => IntV(nativeRet.asInstanceOf[Rep[Long]], size) - case f@FloatType(_) => FloatV(nativeRet.asInstanceOf[Rep[Double]], f.size) - case _ => throw new Exception("Unknown native return type") - } - k(retSs, retVal) - } - topFun(generateNativeCall(_, _, _)) - } - - override def wrapFunV(f: FFTy): Rep[Value] = CPSFunV[Id](f) - - def exec(fname: String, args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] = { - implicit val ctx = Ctx(fname, findFirstBlock(fname).label.get) - val preHeap: Rep[List[Value]] = List(precompileHeapLists(m::Nil):_*) - Coverage.incPath(1) - val ss = initState(preHeap.asRepOf[Mem]) - val fv = eval(GlobalId(fname), VoidType, ss) - fv[Id](ss.push.updateArg.initErrorLoc, args, k) - } -} -*/ \ No newline at end of file diff --git a/src/main/scala/gensym/engines/PureEngine.scala b/src/main/scala/gensym/engines/PureEngine.scala deleted file mode 100644 index eb1872bca..000000000 --- a/src/main/scala/gensym/engines/PureEngine.scala +++ /dev/null @@ -1,504 +0,0 @@ -package gensym -/* -import lms.core._ -import lms.core.Backend._ -import lms.core.virtualize -import lms.macros.SourceContext -import lms.core.stub.{While => _, _} - -import gensym.llvm._ -import gensym.llvm.IR._ -import gensym.llvm.parser.Parser._ -import gensym.IRUtils._ -import gensym.Constants._ -import gensym.lmsx._ - -import gensym.structure.freer._ -import Eff._ -import Freer._ -import Handlers._ -import State._ - -import scala.collection.JavaConverters._ -import scala.collection.immutable.{List => StaticList, Map => StaticMap} - -@virtualize -trait GSEngine extends StagedNondet with SymExeDefs with EngineBase { - type BFTy = Rep[SS => List[(SS, Value)]] - type FFTy = Rep[(SS, List[Value]) => List[(SS, Value)]] - - def symExecBr(ss: Rep[SS], tCond: Rep[Value], fCond: Rep[Value], - tBlockLab: String, fBlockLab: String)(implicit ctx: Ctx): Rep[List[(SS, Value)]] = { - val tBrFunName = getRealBlockFunName(Ctx(ctx.funName, tBlockLab)) - val fBrFunName = getRealBlockFunName(Ctx(ctx.funName, fBlockLab)) - val curBlockId = Counter.block.get(ctx.toString) - "sym_exec_br".reflectWith[List[(SS, Value)]](ss, curBlockId, tCond, fCond, - unchecked[String](tBrFunName), unchecked[String](fBrFunName)) - } - - def eval(v: LLVMValue, ty: LLVMType, argTypes: Option[List[LLVMType]] = None)(implicit ctx: Ctx): Comp[E, Rep[Value]] = { - v match { - case LocalId(x) => - for { ss <- getState } yield ss.lookup(x) - case IntConst(n) => - ret(IntV(n, ty.asInstanceOf[IntType].size)) - case FloatConst(f) => ret(FloatV(f, ty.asInstanceOf[FloatType].size)) - case FloatLitConst(l) => ret(FloatV(l, 80)) - // case ArrayConst(cs) => - case BitCastExpr(from, const, to) => - eval(const, to) - case BoolConst(b) => b match { - case true => ret(IntV(1, 1)) - case false => ret(IntV(0, 1)) - } - case GlobalId(id) if symDefMap.contains(id) => - System.out.println(s"Alias: $id => ${symDefMap(id).const}") - for { - v <- eval(symDefMap(id).const, ty) - } yield v - case GlobalId(id) if funMap.contains(id) && ExternalFun.shouldRedirect(id) => - val t = funMap(id).header.returnType - ret(ExternalFun.get(id, Some(t), argTypes).get) - case GlobalId(id) if funMap.contains(id) => - if (!FunFuns.contains(id)) compile(funMap(id)) - ret(wrapFunV(FunFuns(id))) - case GlobalId(id) if funDeclMap.contains(id) => - val t = funDeclMap(id).header.returnType - val fv = ExternalFun.get(id, Some(t), argTypes).getOrElse { - compile(funDeclMap(id), t, argTypes.get) - wrapFunV(FunFuns(getMangledFunctionName(funDeclMap(id), argTypes.get))) - } - ret(fv) - case GlobalId(id) if globalDefMap.contains(id) => - ret(heapEnv(id)()) - case GlobalId(id) if globalDeclMap.contains(id) => - System.out.println(s"Warning: globalDecl $id is ignored") - ty match { - case PtrType(_, _) => ret(NullLoc()) - case _ => ret(NullPtr[Value]) - } - case GetElemPtrExpr(_, baseType, ptrType, const, typedConsts) => - // typedConst are not all int, could be local id - for { - vs <- mapM(typedConsts)(tv => eval(tv.const, tv.ty)) - lv <- eval(const, ptrType) - ss <- getState - } yield lv.asRepOf[LocV] + calculateOffset(ptrType, vs) - case IntToPtrExpr(from, value, to) => - for { v <- eval(value, from) } yield v - case PtrToIntExpr(from, value, IntType(toSize)) => - for { p <- eval(value, from) } yield - if (ARCH_WORD_SIZE == toSize) p - else p.trunc(ARCH_WORD_SIZE, toSize) - case FCmpExpr(pred, ty1, ty2, lhs, rhs) if ty1 == ty2 => evalFloatOp2(pred.op, lhs, rhs, ty1) - case ICmpExpr(pred, ty1, ty2, lhs, rhs) if ty1 == ty2 => evalIntOp2(pred.op, lhs, rhs, ty1) - case InlineASM() => ret(NullPtr[Value]) - case ZeroInitializerConst => - System.out.println("Warning: Evaluate zeroinitialize in body") - ret(NullPtr[Value]) // FIXME: use uninitValue - case NullConst => ret(NullLoc()) - case NoneConst => ret(NullPtr[Value]) - case v => System.out.println(ty, v); ??? - } - } - - def evalIntOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType)(implicit ctx: Ctx): Comp[E, Rep[Value]] = - for { v1 <- eval(lhs, ty); v2 <- eval(rhs, ty) } yield IntOp2(op, v1, v2) - - def evalFloatOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType)(implicit ctx: Ctx): Comp[E, Rep[Value]] = - { - for { v1 <- eval(lhs, ty); v2 <- eval(rhs, ty) } yield FloatOp2(op, v1, v2) - } - - def execValueInst(inst: ValueInstruction)(implicit ctx: Ctx): Comp[E, Rep[Value]] = { - inst match { - // Memory Access Instructions - case AllocaInst(ty, align) => - val typeSize = ty.size - for { - ss <- getState - ss2 <- ret(ss.allocStack(typeSize, align.n)) - _ <- putState(ss2) - } yield LocV(ss2.stackSize - typeSize, LocV.kStack, typeSize.toLong) - case LoadInst(valTy, ptrTy, value, align) => - val isStruct = getRealType(valTy) match { - case Struct(types) => 1 - case _ => 0 - } - for { - v <- eval(value, ptrTy) - ss <- getState - } yield ss.lookup(v, valTy.size, isStruct) - case GetElemPtrInst(_, baseType, ptrType, ptrValue, typedValues) => - for { - vs <- mapM(typedValues)(tv => eval(tv.value, tv.ty)) - lv <- eval(ptrValue, ptrType) - ss <- getState - } yield lv.asRepOf[LocV] + calculateOffset(ptrType, vs) - // Arith Unary Operations - case FNegInst(ty, op) => evalFloatOp2("fsub", FloatConst(-0.0), op, ty) - // Arith Binary Operations - case AddInst(ty, lhs, rhs, _) => evalIntOp2("add", lhs, rhs, ty) - case SubInst(ty, lhs, rhs, _) => evalIntOp2("sub", lhs, rhs, ty) - case MulInst(ty, lhs, rhs, _) => evalIntOp2("mul", lhs, rhs, ty) - case SDivInst(ty, lhs, rhs) => evalIntOp2("sdiv", lhs, rhs, ty) - case UDivInst(ty, lhs, rhs) => evalIntOp2("udiv", lhs, rhs, ty) - case FAddInst(ty, lhs, rhs) => evalFloatOp2("fadd", lhs, rhs, ty) - case FSubInst(ty, lhs, rhs) => evalFloatOp2("fsub", lhs, rhs, ty) - case FMulInst(ty, lhs, rhs) => evalFloatOp2("fmul", lhs, rhs, ty) - case FDivInst(ty, lhs, rhs) => evalFloatOp2("fdiv", lhs, rhs, ty) - /* Backend Work Needed */ - case URemInst(ty, lhs, rhs) => evalIntOp2("urem", lhs, rhs, ty) - case SRemInst(ty, lhs, rhs) => evalIntOp2("srem", lhs, rhs, ty) - - // Bitwise Operations - /* Backend Work Needed */ - case ShlInst(ty, lhs, rhs) => evalIntOp2("shl", lhs, rhs, ty) - case LshrInst(ty, lhs, rhs) => evalIntOp2("lshr", lhs, rhs, ty) - case AshrInst(ty, lhs, rhs) => evalIntOp2("ashr", lhs, rhs, ty) - case AndInst(ty, lhs, rhs) => evalIntOp2("and", lhs, rhs, ty) - case OrInst(ty, lhs, rhs) => evalIntOp2("or", lhs, rhs, ty) - case XorInst(ty, lhs, rhs) => evalIntOp2("xor", lhs, rhs, ty) - - // Conversion Operations - /* Backend Work Needed */ - case ZExtInst(from, value, IntType(size)) => - for { v <- eval(value, from) } yield v.zExt(size) - case SExtInst(from, value, IntType(size)) => - for { v <- eval(value, from) } yield v.sExt(size) - case TruncInst(from@IntType(fromSz), value, IntType(toSz)) => - for { v <- eval(value, from) } yield v.trunc(fromSz, toSz) - case FpExtInst(from, value, to) => - for { v <- eval(value, from) } yield v - case FpToUIInst(from, value, IntType(size)) => - for { v <- eval(value, from) } yield v.fromFloatToUInt(size) - case FpToSIInst(from, value, IntType(size)) => - for { v <- eval(value, from) } yield v.fromFloatToSInt(size) - case UiToFPInst(from, value, to) => - for { v <- eval(value, from) } yield v.fromUIntToFloat - case SiToFPInst(from, value, to) => - for { v <- eval(value, from) } yield v.fromSIntToFloat - case PtrToIntInst(from, value, to) => - for { v <- eval(value, from) } yield - if (ARCH_WORD_SIZE == to.asInstanceOf[IntType].size) v - else v.trunc(ARCH_WORD_SIZE, to.asInstanceOf[IntType].size) - case IntToPtrInst(from, value, to) => - for { v <- eval(value, from) } yield v - case BitCastInst(from, value, to) => eval(value, to) - - // Aggregate Operations - /* Backend Work Needed */ - case ExtractValueInst(ty, struct, indices) => - /* - Struct is tricky. Consider the following code snippet - a: - %call = call { i64, i64 } @get_stat_atime(%struct.stat* %2) - %5 = extractvalue { i64, i64 } %call, 0 - - as a result, b should return a backend Struct value - b: - %retval = alloca %struct.timespec, align 8 - %3 = bitcast %struct.timespec* %retval to { i64, i64 }* - %4 = load { i64, i64 }, { i64, i64 }* %3, align 8 - ret { i64, i64 } %4 - */ - val idxList = indices.asInstanceOf[List[IntConst]].map(x => x.n) - val idx = calculateOffsetStatic(ty, idxList) - for { - // v is expected to be StructV in backend - v <- eval(struct, ty) - } yield v.structAt(idx) - - // Other operations - case FCmpInst(pred, ty, lhs, rhs) => evalFloatOp2(pred.op, lhs, rhs, ty) - case ICmpInst(pred, ty, lhs, rhs) => evalIntOp2(pred.op, lhs, rhs, ty) - case CallInst(ty, f, args) => - val argValues: List[LLVMValue] = extractValues(args) - val argTypes: List[LLVMType] = extractTypes(args) - for { - fv <- eval(f, VoidType, Some(argTypes)) - vs <- mapM2Tup(argValues)(argTypes)(eval(_, _, None)) - _ <- pushFrame - s <- getState - v <- reflect(fv[Id](s, List(vs:_*))) - _ <- popFrame(s.stackSize) - } yield v - - case PhiInst(ty, incs) => - def selectValue(bb: Rep[BlockLabel], vs: List[Rep[Value]], labels: List[BlockLabel]): Rep[Value] = { - if (bb == labels(0) || labels.length == 1) vs(0) - else selectValue(bb, vs.tail, labels.tail) - } - val incsValues: List[LLVMValue] = incs.map(_.value) - val incsLabels: List[BlockLabel] = incs.map(i => Counter.block.get(ctx.withBlock(i.label))) - for { - vs <- mapM(incsValues)(eval(_, ty)) - s <- getState - } yield selectValue(s.incomingBlock, vs, incsLabels) - case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) if Global.config.iteSelect => - for { - cnd <- eval(cndVal, cndTy) - tv <- eval(thnVal, thnTy) - ev <- eval(elsVal, elsTy) - } yield ITE(cnd, tv, ev) - case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) => - // TODO: check cond via solver - for { - cnd <- eval(cndVal, cndTy) - s <- getState - v <- reflect { - if (cnd.isConc) { - if (cnd.int == 1) reify(s)(eval(thnVal, thnTy)) - else reify(s)(eval(elsVal, elsTy)) - } else { - Coverage.incPath(1) - reify(s) { - (for { - _ <- updatePC(cnd) - v <- eval(thnVal, thnTy) - } yield v) - } ++ reify(s.fork) { - (for { - _ <- updatePC(!cnd) - v <- eval(elsVal, elsTy) - } yield v) - } - } - } - } yield v - } - } - - // Note: Comp[E, Rep[Value]] vs Comp[E, Rep[Option[Value]]]? - def execTerm(inst: Terminator)(implicit ctx: Ctx): Comp[E, Rep[Value]] = { - inst match { - // FIXME: unreachable - case Unreachable => ret(IntV(-1)) - case RetTerm(ty, v) => - v match { - case Some(value) => eval(value, ty) - case None => ret(NullPtr[Value]) - } - case BrTerm(lab) if (cfg.pred(ctx.funName, lab).size == 1) => - execBlockEager(findBlock(ctx.funName, lab).get)(Ctx(ctx.funName, lab)) - case BrTerm(lab) => - for { - _ <- updateIncomingBlock(ctx) - v <- execBlock(ctx.funName, lab) - } yield v - case CondBrTerm(ty, cnd, thnLab, elsLab) => - Counter.setBranchNum(ctx, 2) - for { - _ <- updateIncomingBlock(ctx) - ss <- getState - cndVal <- eval(cnd, ty) - u <- reflect { - if (cndVal.isConc) { - if (cndVal.int == 1) reify(ss){ Coverage.incBranch(ctx, 0); execBlock(ctx.funName, thnLab) } - else reify(ss) { Coverage.incBranch(ctx, 1); execBlock(ctx.funName, elsLab) } - } else { - symExecBr(ss, cndVal, !cndVal, thnLab, elsLab) - /* - val tpcSat = checkPC(ss.pc + cndVal.toSMTBool) - val fpcSat = checkPC(ss.pc + cndVal.toSMTBoolNeg) - val b1 = for { - _ <- updatePC(cndVal.toSMTBool) - v <- execBlock(funName, thnLab) - } yield v - val b2 = for { - _ <- updatePC(cndVal.toSMTBoolNeg) - v <- execBlock(funName, elsLab) - } yield v - if (tpcSat && fpcSat) { - Coverage.incPath(1) - if (ThreadPool.canPar) { - val asyncb1: Rep[Future[List[(SS, Value)]]] = ThreadPool.async { _ => reify(ss) { b1 } } - val rb2 = reify(ss) { b2 } // must reify b2 before get the async, order matters here - ThreadPool.get(asyncb1) ++ rb2 - } else reify(ss) { b1 ⊕ b2 } - } else if (tpcSat) { - reify(ss) { b1 } - } else if (fpcSat) { - reify(ss) { b2 } - } else { - List[(SS, Value)]() - } - */ - } - } - } yield u - case SwitchTerm(cndTy, cndVal, default, swTable) => - Counter.setBranchNum(ctx, swTable.size+1) - def switch(v: Rep[Long], s: Rep[SS], table: List[LLVMCase]): Rep[List[(SS, Value)]] = - if (table.isEmpty) { - Coverage.incBranch(ctx, swTable.size) - execBlock(ctx.funName, default, s) - } else { - if (v == table.head.n) { - Coverage.incBranch(ctx, swTable.size - table.size) - execBlock(ctx.funName, table.head.label, s) - } else switch(v, s, table.tail) - } - - val nPath: Var[Int] = var_new(0) - def switchSym(v: Rep[Value], s: Rep[SS], table: List[LLVMCase]): Rep[List[(SS, Value)]] = - if (table.isEmpty) - if (checkPC(s.pc)) { - nPath += 1 - val new_ss = if (1 == nPath) s else s.fork - Coverage.incBranch(ctx, swTable.size) - reify(new_ss) { execBlock(ctx.funName, default) } - } else List[(SS, Value)]() - else { - val headPC = IntOp2("eq", v, IntV(table.head.n)) - val m = reflect { - if (checkPC(s.pc.addPC(headPC))) { - nPath += 1 - val new_ss = if (1 == nPath) s else s.fork - Coverage.incBranch(ctx, swTable.size - table.size) - reify(new_ss)(for { - _ <- updatePC(headPC) - u <- execBlock(ctx.funName, table.head.label) - } yield u) - } else List[(SS, Value)]() - } - val next = reflect { switchSym(v, s.addPC(!headPC), table.tail) } - reify(s) { m ⊕ next } - } - - for { - _ <- updateIncomingBlock(ctx) - v <- eval(cndVal, cndTy) - s <- getState - r <- reflect { - if (v.isConc) switch(v.int, s, swTable) - else { - val r = switchSym(v, s, swTable) - if (nPath > 0) Coverage.incPath(nPath - 1) - r - } - } - } yield r - } - } - - def execInst(inst: Instruction)(implicit ctx: Ctx): Comp[E, Rep[Unit]] = { - inst match { - case AssignInst(x, valInst) => - for { - v <- execValueInst(valInst) - _ <- stackUpdate(x, v) - } yield () - case StoreInst(ty1, val1, ty2, val2, align) => - for { - v1 <- eval(val1, ty1) - v2 <- eval(val2, ty2) - _ <- updateMem(v2, v1, ty1.size) - } yield () - case CallInst(ty, f, args) => - val argValues: List[LLVMValue] = extractValues(args) - val argTypes: List[LLVMType] = extractTypes(args) - for { - fv <- eval(f, VoidType, Some(argTypes)) - vs <- mapM2Tup(argValues)(argTypes)(eval(_, _, None)) - _ <- pushFrame - s <- getState - v <- reflect(fv[Id](s, List(vs:_*))) - _ <- popFrame(s.stackSize) - } yield () - } - } - - def execBlock(funName: String, label: String, s: Rep[SS]): Rep[List[(SS, Value)]] = - getBBFun(funName, findBlock(funName, label).get)(s) - - def execBlock(funName: String, label: String): Comp[E, Rep[Value]] = - execBlock(funName, findBlock(funName, label).get) - - def execBlock(funName: String, block: BB): Comp[E, Rep[Value]] = - for { - s <- getState - v <- { - info("jump to block: " + block.label.get) - reflect(getBBFun(funName, block)(s)) - } - } yield v - - def execBlockEager(b: BB)(implicit ctx: Ctx): Comp[E, Rep[Value]] = { - val runInstList: Comp[E, Rep[Value]] = for { - _ <- coverNewBlock(ctx) - _ <- mapM(b.ins)(execInst(_)) - v <- execTerm(b.term) - } yield v - runInstList - } - - override def repBlockFun(b: BB)(implicit ctx: Ctx): BFTy = { - def runBlock(ss: Rep[SS]): Rep[List[(SS, Value)]] = { - info("running block: " + ctx.funName + " - " + b.label.get) - reify[Value](ss)(execBlockEager(b)) - } - topFun(runBlock(_)) - } - - override def repFunFun(f: FunctionDef): FFTy = { - def runFun(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] = { - implicit val ctx = Ctx(f.id, f.blocks(0).label.get) - val params: List[String] = extractNames(f.header.params) - info("running function: " + f.id) - val m: Comp[E, Rep[Value]] = for { - _ <- stackUpdate(params, args) - s <- getState - v <- execBlockEager(f.blocks(0)) - } yield v - reify(ss)(m) - } - topFun(runFun(_, _)) - } - - override def repExternFun(f: FunctionDecl, retTy: LLVMType, argTypes: List[LLVMType]): FFTy = { - def generateNativeCall(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] = { - info("running native function: " + f.id) - val nativeArgs: List[Rep[Any]] = argTypes.zipWithIndex.map { - case (ty@PtrType(_, _), id) => ss.getPointerArg(args(id)).castToM(ty.toManifest) - case (ty@IntType(size), id) => ss.getIntArg(args(id)).castToM(ty.toManifest) - case (ty@FloatType(k), id) => ss.getFloatArg(args(id)).castToM(ty.toManifest) - case _ => throw new Exception("Unknown native argument type") - } - val ptrArgIndices: List[Int] = argTypes.zipWithIndex.filter { - case (ty, id) => ty.isInstanceOf[PtrType] - }.map(_._2) - val fv = NativeExternalFun(f.id.tail, Some(retTy)) - val nativeRet = fv(nativeArgs).castToM(retTy.toManifest) - val retVal = retTy match { - case IntType(size) => IntV(nativeRet.asInstanceOf[Rep[Long]], size) - case f@FloatType(_) => FloatV(nativeRet.asInstanceOf[Rep[Double]], f.size) - case _ => throw new Exception("Unknown native return type") - } - val m: Comp[E, Rep[Value]] = mapM(ptrArgIndices) { id => - writebackPointerArg(nativeRet, args(id), nativeArgs(id).asRepOf[Ptr[Char]]) - }.map { _ => retVal } - reify(ss)(m) - } - topFun(generateNativeCall(_, _)) - } - - override def wrapFunV(f: FFTy): Rep[Value] = FunV[Id](f) - - def exec(fname: String, args: Rep[List[Value]]): Rep[List[(SS, Value)]] = { - implicit val ctx = Ctx(fname, findFirstBlock(fname).label.get) - val preHeap: Rep[List[Value]] = List(precompileHeapLists(m::Nil):_*) - val heap0 = preHeap.asRepOf[Mem] - val comp = for { - fv <- eval(GlobalId(fname), VoidType) - _ <- pushFrame - _ <- initializeArg - _ <- initializeErrorLoc - s <- getState - v <- reflect(fv[Id](s, args)) - } yield v - Coverage.incPath(1) - reify[Value](initState(heap0))(comp) - } -} -*/ \ No newline at end of file diff --git a/src/main/scala/gensym/states/SymExeState.scala b/src/main/scala/gensym/states/SymExeState.scala deleted file mode 100644 index af6e331e0..000000000 --- a/src/main/scala/gensym/states/SymExeState.scala +++ /dev/null @@ -1,194 +0,0 @@ -package gensym -/* -import lms.core._ -import lms.core.Backend._ -import lms.core.virtualize -import lms.macros.SourceContext -import lms.core.stub.{While => _, _} - -import gensym.llvm._ -import gensym.llvm.IR._ -import gensym.lmsx._ -import gensym.structure.freer._ -import Eff._ -import Freer._ -import Handlers._ -import State._ - -import scala.collection.immutable.{List => StaticList, Map => StaticMap, Set => StaticSet} -import scala.collection.mutable.{Map => MutableMap, Set => MutableSet} - -/* Naming convention for IR nodes: - - If the node can be and should be handled by the default case of the codegen, - i.e. directly emitting the IR name and arguments sequentially, - we shall use underscore `_` as the delimiter in the IR name, e.g. `proj_LocV`. - - If the node requires additional care in the codegen, - we should use dash `-` as the delimiter in the IR name, e.g. `ss-lookup-stack`. - The reason is that in common codegen targets (such as C/C++/Scala), `-` is - not a valid use of identifiers. - */ - -@virtualize -trait SymExeDefs extends SAIOps with StagedNondet with BasicDefs with ValueDefs with FileSysDefs with Opaques with Coverage { - type E = State[Rep[SS], *] ⊗ (Nondet ⊗ ∅) - type Cont = PCont[Id] - - override def usingPureEngine: Boolean = true - - trait Future[T] - - object ThreadPool { - def enqueue[T: Manifest](f: Rep[Unit] => Rep[T]): Rep[Future[T]] = { - val block = Adapter.g.reify(x => Unwrap(f(Wrap[Unit](x)))) - Wrap[Future[T]](Adapter.g.reflectWrite("tp-enqueue", block)(Adapter.CTRL)) - } - def async[T: Manifest](f: Rep[Unit] => Rep[T]): Rep[Future[T]] = { - val block = Adapter.g.reify(x => Unwrap(f(Wrap[Unit](x)))) - Wrap[Future[T]](Adapter.g.reflectWrite("tp-async", block)(Adapter.CTRL)) - } - def get[T: Manifest](f: Rep[Future[T]]): Rep[T] = - "tp-future-get".reflectWriteWith[T](f)(Adapter.CTRL) - - def canPar: Rep[Boolean] = "can-par".reflectWriteWith[Boolean]()(Adapter.CTRL) - } - - def reify[T: Manifest](s: Rep[SS])(comp: Comp[E, Rep[T]]): Rep[List[(SS, T)]] = { - val p1: Comp[Nondet ⊗ ∅, (Rep[SS], Rep[T])] = - State.runState[Nondet ⊗ ∅, Rep[SS], Rep[T]](s)(comp) - val p2: Comp[Nondet ⊗ ∅, Rep[(SS, T)]] = p1.map(a => a) - val p3: Comp[∅, Rep[List[(SS, T)]]] = runRepNondet[(SS, T)](p2) - p3 - } - - def reflect[T: Manifest](res: Rep[List[(SS, T)]]): Comp[E, Rep[T]] = { - for { - ssu <- select[E, (SS, T)](res) - _ <- put[Rep[SS], E](ssu._1) - } yield ssu._2 - } - - implicit class PCOps(pc: Rep[PC]) { - def addPC(e: Rep[Value]): Rep[PC] = "add-pc".reflectWith[PC](pc, e) - } - - class SSOps(ss: Rep[SS]) { - private def assignSeq(xs: List[Int], vs: Rep[List[Value]]): Rep[SS] = - "ss-assign-seq".reflectWith[SS](ss, xs, vs) - - def lookup(x: String)(implicit ctx: Ctx): Rep[Value] = - "ss-lookup-env".reflectWith[Value](ss, varId(x)) - def assign(x: String, v: Rep[Value])(implicit ctx: Ctx): Rep[SS] = - "ss-assign".reflectWith[SS](ss, varId(x), v) - def assign(xs: List[String], vs: Rep[List[Value]])(implicit ctx: Ctx): Rep[SS] = - assignSeq(xs.map(varId(_)), vs) - def lookup(addr: Rep[Value], size: Int = 1, isStruct: Int = 0): Rep[Value] = { - require(size > 0) - if (isStruct == 0) "ss-lookup-addr".reflectWith[Value](ss, addr, size) - else "ss-lookup-addr-struct".reflectWith[Value](ss, addr, size) - } - def lookupSeq(addr: Rep[Value], count: Rep[Int]): Rep[List[Value]] = "ss-lookup-addr-seq".reflectWith[List[Value]](ss, addr, count) - - //def arrayLookup(base: Rep[Value], offset: Rep[Value], eSize: Int, k: Rep[Cont]): Rep[Unit] = - // "ss-array-lookup".reflectWith[Unit](ss, base, offset, eSize, k) - //def arrayLookup(base: Rep[Value], offset: Rep[Value], eSize: Int): Rep[List[(SS, Value)]] = - // "ss-array-lookup".reflectWith[List[(SS, Value)]](ss, base, offset, eSize) - - def update(a: Rep[Value], v: Rep[Value], sz: Int): Rep[SS] = "ss-update".reflectWith[SS](ss, a, v, sz) - @deprecated("Use update with size", "now and forever") - def update(a: Rep[Value], v: Rep[Value]): Rep[SS] = "ss-update".reflectWith[SS](ss, a, v) - def updateSeq(a: Rep[Value], v: Rep[List[Value]]): Rep[SS] = "ss-update-seq".reflectWith[SS](ss, a, v) - def allocStack(n: Int, align: Int): Rep[SS] = "ss-alloc-stack".reflectWith[SS](ss, n) - - def heapLookup(addr: Rep[Addr]): Rep[Value] = "ss-lookup-heap".reflectWith[Value](ss, addr) - def heapSize: Rep[Int] = "ss-heap-size".reflectWith[Int](ss) - def heapAppend(vs: Rep[List[Value]]) = "ss-heap-append".reflectWith[SS](ss, vs) - - def stackSize: Rep[Int] = "ss-stack-size".reflectWith[Int](ss) - def freshStackAddr: Rep[Addr] = stackSize - - def push: Rep[SS] = "ss-push".reflectWith[SS](ss) - def pop(keep: Rep[Int]): Rep[SS] = "ss-pop".reflectWith[SS](ss, keep) - def addPC(e: Rep[Value]): Rep[SS] = "ss-addpc".reflectWith[SS](ss, e) - def addPCSet(es: Rep[List[Value]]): Rep[SS] = "ss-addpcset".reflectWith[SS](ss, es) - def pc: Rep[PC] = "get-pc".reflectWith[PC](ss) - def copyPC: Rep[PC] = "ss-copy-pc".reflectCtrlWith[PC](ss) // hack - def updateArg: Rep[SS] = "ss-arg".reflectWith[SS](ss) - def initErrorLoc: Rep[SS] = "ss-init-error-loc".reflectWith[SS](ss) - def getErrorLoc: Rep[Value] = "ss-get-error-loc".reflectWith[Value](ss) - def setErrorLoc(v: Rep[IntV]): Rep[SS] = ss.update(ss.getErrorLoc, v, 4) - - def addIncomingBlock(ctx: Ctx): Rep[SS] = "ss-add-incoming-block".reflectWith[SS](ss, Counter.block.get(ctx.toString)) - def coverBlock(ctx: Ctx): Rep[SS] = "ss-cover-block".reflectCtrlWith[SS](ss, Counter.block.get(ctx.toString)) - def incomingBlock: Rep[BlockLabel] = "ss-incoming-block".reflectWith[BlockLabel](ss) - - def fork: Rep[SS] = "ss-fork".reflectCtrlWith[SS](ss) - - def getSSid: Rep[Long] = "ss-getssid".reflectWith[Long](ss) - - def getFs: Rep[FS] = "ss-get-fs".reflectCtrlWith[FS](ss) - def setFs(fs: Rep[FS]): Unit = "ss-set-fs".reflectCtrlWith[FS](ss, fs) - - // Note: getIntArg/getFloatArg/getPointerArg may potentially call solver - def getIntArg(x : Rep[Value]): Rep[Long] = "ss-get-int-arg".reflectWith[Long](ss, x) - def getFloatArg(x : Rep[Value]): Rep[Double] = "ss-get-float-arg".reflectWith[Double](ss, x) - def getPointerArg(x : Rep[Value]): Rep[Ptr[Char]] = "ss-get-pointer-arg".reflectWith[Ptr[Char]](ss, x) - def writebackPointerArg(res: Rep[Any], addr:Rep[Value], x: Rep[Ptr[Char]]): Rep[SS] = - "ss-writeback-pointer-arg".reflectWith[SS](ss, res, addr, x) - } - - implicit class SSOpsOpt(ss: Rep[SS]) extends SSOps(ss) { - private def lookupOpt(x: Int, s: Backend.Def, default: => Rep[Value], bound: Int): Rep[Value] = - if (bound == 0) default - else s match { - case gNode("ss-assign", StaticList(ss0, bConst(y), v: bExp)) if y == x => Wrap[Value](v) - case gNode("ss-assign-seq", StaticList(ss0, bConst(vars: StaticList[Int]), vals: bExp)) => - val idx = vars.indexOf(x) - if (idx != -1) (Wrap[List[Value]](vals): Rep[List[Value]])(idx) - else lookupOpt(x, ss0, default, bound-1) - case gNode("ss-assign", StaticList(ss0, _, _)) => lookupOpt(x, ss0, default, bound-1) - case gNode("ss-alloc-stack", StaticList(ss0, _)) => lookupOpt(x, ss0, default, bound-1) - case gNode("ss-update", StaticList(ss0, _, _, _)) => lookupOpt(x, ss0, default, bound-1) - case gNode("ss-add-incoming-block", StaticList(ss0, _)) => lookupOpt(x, ss0, default, bound-1) - // TODO: update-seq? - case _ => default - } - - override def lookup(x: String)(implicit ctx: Ctx): Rep[Value] = - if (Global.config.opt) lookupOpt(varId(x), Unwrap(ss), super.lookup(x), 30) - else super.lookup(x) - - override def stackSize: Rep[Int] = - if (Global.config.opt) { - Unwrap(ss) match { - case gNode("ss-alloc-stack", StaticList(ss0: bExp, bConst(inc: Int))) => Wrap[SS](ss0).stackSize + inc - case gNode("ss-assign", StaticList(ss0: bExp, _, _)) => Wrap[SS](ss0).stackSize - case _ => super.stackSize - } - } else { super.stackSize } - } - - def putState(s: Rep[SS]): Comp[E, Rep[Unit]] = for { _ <- put[Rep[SS], E](s) } yield () - def getState: Comp[E, Rep[SS]] = get[Rep[SS], E] - - def updateState(f: Rep[SS] => Rep[SS]): Comp[E, Rep[Unit]] = - for { - ss <- getState - _ <- putState(f(ss)) - } yield () - - def heapAppend(vs: Rep[List[Value]]): Comp[E, Rep[Unit]] = updateState(_.heapAppend(vs)) - def stackUpdate(xs: List[String], vs: Rep[List[Value]])(implicit ctx: Ctx): Comp[E, Rep[Unit]] = updateState(_.assign(xs, vs)) - def stackUpdate(x: String, v: Rep[Value])(implicit ctx: Ctx): Comp[E, Rep[Unit]] = updateState(_.assign(x, v)) - def pushFrame: Comp[E, Rep[Unit]] = updateState(_.push) - def popFrame(keep: Rep[Int]): Comp[E, Rep[Unit]] = updateState(_.pop(keep)) - def updateMem(k: Rep[Value], v: Rep[Value], sz: Int): Comp[E, Rep[Unit]] = updateState(_.update(k, v, sz)) - def updatePCSet(x: Rep[List[Value]]): Comp[E, Rep[Unit]] = updateState(_.addPCSet(x)) - def updatePC(x: Rep[Value]): Comp[E, Rep[Unit]] = updateState(_.addPC(x)) - def updateIncomingBlock(ctx: Ctx): Comp[E, Rep[Unit]] = updateState(_.addIncomingBlock(ctx)) - def coverNewBlock(ctx: Ctx): Comp[E, Rep[Unit]] = updateState(_.coverBlock(ctx)) - def initializeArg: Comp[E, Rep[Unit]] = updateState(_.updateArg) - def initializeErrorLoc: Comp[E, Rep[Unit]] = updateState(_.initErrorLoc) - - def writebackPointerArg(res: Rep[Any], addr: Rep[Value], x: Rep[Ptr[Char]]): Comp[E, Rep[Unit]] = updateState(_.writebackPointerArg(res, addr, x)) -} -*/ \ No newline at end of file