Skip to content

Commit e8bfa0c

Browse files
KraksKraks
committed
experiment generating models for external/intrinsic functions
1 parent 878dbc9 commit e8bfa0c

File tree

8 files changed

+71
-19
lines changed

8 files changed

+71
-19
lines changed

‎dev-clean/src/main/scala/sai/llsc/Driver.scala‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ class PureLLSC extends LLSC {
206206
val args: Rep[List[Value]] = SymV.makeSymVList(nSym)
207207
val res = exec(fname, args, false, 4)
208208
// FIXME: pass isCommandLine, symarg=4 seems doesn't work on mp1p?
209-
res.foreach { s => SS.checkPCToFile(s._1) }
209+
res.foreach { s => checkPCToFile(s._1) }
210210
()
211211
}
212212
}
@@ -219,7 +219,7 @@ class PureCPSLLSC extends LLSC {
219219
def snippet(u: Rep[Int]) = {
220220
val args: Rep[List[Value]] = SymV.makeSymVList(nSym)
221221
val k: Rep[Cont] = fun { case sv =>
222-
SS.checkPCToFile(sv._1); ()
222+
checkPCToFile(sv._1); ()
223223
}
224224
exec(fname, args, false, 4, k)
225225
}
@@ -243,7 +243,7 @@ class ImpLLSC extends LLSC {
243243
def snippet(u: Rep[Int]) = {
244244
val args: Rep[List[Value]] = SymV.makeSymVList(nSym)
245245
val res = exec(fname, args, false, 4)
246-
res.foreach { s => SS.checkPCToFile(s._1)}
246+
res.foreach { s => checkPCToFile(s._1)}
247247
()
248248
}
249249
}
@@ -256,7 +256,7 @@ class ImpVecLLSC extends LLSC {
256256
def snippet(u: Rep[Int]) = {
257257
val args: Rep[List[Value]] = SymV.makeSymVList(nSym)
258258
val res = exec(fname, args, false, 4)
259-
res.foreach { s => SS.checkPCToFile(s._1)}
259+
res.foreach { s => checkPCToFile(s._1)}
260260
()
261261
}
262262
}
@@ -269,7 +269,7 @@ class ImpCPSLLSC extends LLSC {
269269
def snippet(u: Rep[Int]) = {
270270
val args: Rep[List[Value]] = SymV.makeSymVList(nSym)
271271
val k: Rep[Cont] = fun { case sv =>
272-
SS.checkPCToFile(sv._1); ()
272+
checkPCToFile(sv._1); ()
273273
}
274274
exec(fname, args, false, 4, k)
275275
}

‎dev-clean/src/main/scala/sai/llsc/External.scala‎

Lines changed: 51 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,12 @@ import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
2828
// Can we generate them from our Scala DSL?
2929

3030
@virtualize
31-
trait GenExternal extends SymExeDefs with EngineBase {
32-
def sym_exit[T: Manifest](ss: Rep[SS], args: Rep[List[Value]]): Rep[T] = ???
31+
trait GenExternal extends SymExeDefs {
32+
// TODO: generating functions with proper names, instead of x1, x2 ...
33+
34+
// TODO: sym_exit return type in C should be void
35+
def sym_exit[T: Manifest](ss: Rep[SS], args: Rep[List[Value]]): Rep[T] =
36+
"sym_exit".reflectWith[T](ss, args)
3337

3438
def gen_llsc_assert[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = {
3539
val v = args(0)
@@ -44,4 +48,49 @@ trait GenExternal extends SymExeDefs with EngineBase {
4448
else k(ss1, IntV(1, 32))
4549
}
4650
}
51+
52+
def llsc_assert(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
53+
gen_llsc_assert[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
54+
55+
def llsc_assert_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
56+
gen_llsc_assert[Unit](ss, args, { case (s, v) => k(s, v) })
57+
}
58+
59+
class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q =>
60+
import java.io.{File, PrintStream}
61+
import scala.collection.mutable.HashMap
62+
63+
val funNameMap: HashMap[Int, String] = new HashMap()
64+
val blockNameMap: HashMap[Int, String] = new HashMap()
65+
66+
val codegen: GenericLLSCCodeGen = new GenericLLSCCodeGen {
67+
val codegenFolder: String = folder
68+
def funMap: HashMap[Int, String] = funNameMap
69+
def blockMap: HashMap[Int, String] = blockNameMap
70+
override def emitAll(g: Graph, name: String)(m1: Manifest[_], m2: Manifest[_]): Unit = {
71+
val ng = init(g)
72+
run(name, ng)
73+
emitln("/* LLSC - External utility functions and library modeling functions */")
74+
emitFunctions(stream)
75+
}
76+
}
77+
78+
def genHeader: Unit = {
79+
val mainStream = new PrintStream(s"$folder/external.hpp")
80+
val statics = Adapter.emitCommon1("header", codegen, mainStream)(manifest[Int], manifest[Unit])(x => Unwrap(wrapper(Wrap[Int](x))))
81+
mainStream.close
82+
}
83+
84+
def snippet(u: Rep[Int]) = {
85+
hardTopFun(llsc_assert(_, _))
86+
hardTopFun(llsc_assert_k(_, _, _))
87+
()
88+
}
89+
}
90+
91+
object TestGenerateExternal {
92+
def main(args: Array[String]): Unit = {
93+
val code = new ExternalLLSCDriver
94+
code.genHeader
95+
}
4796
}

‎dev-clean/src/main/scala/sai/llsc/engines/CPSEngine.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -357,7 +357,7 @@ trait ImpCPSLLSCEngine extends ImpSymExeDefs with EngineBase {
357357
Coverage.setBlockNum
358358
Coverage.incPath(1)
359359
Coverage.startMonitor
360-
val ss = SS.init(preHeap.asRepOf[Mem])
360+
val ss = initState(preHeap.asRepOf[Mem])
361361
if (!isCommandLine) {
362362
val fv = eval(GlobalId(fname), VoidType, ss)(fname)
363363
ss.push

‎dev-clean/src/main/scala/sai/llsc/engines/Engine.scala‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -292,8 +292,8 @@ trait LLSCEngine extends StagedNondet with SymExeDefs with EngineBase {
292292
} else {
293293
symExecBr(ss, cndVal.toSMTBool, cndVal.toSMTBoolNeg, thnLab, elsLab, funName)
294294
/*
295-
val tpcSat = SS.checkPC(ss.pc + cndVal.toSMTBool)
296-
val fpcSat = SS.checkPC(ss.pc + cndVal.toSMTBoolNeg)
295+
val tpcSat = checkPC(ss.pc + cndVal.toSMTBool)
296+
val fpcSat = checkPC(ss.pc + cndVal.toSMTBoolNeg)
297297
val b1 = for {
298298
_ <- updatePC(cndVal.toSMTBool)
299299
v <- execBlock(funName, thnLab)
@@ -471,6 +471,6 @@ trait LLSCEngine extends StagedNondet with SymExeDefs with EngineBase {
471471
Coverage.setBlockNum
472472
Coverage.incPath(1)
473473
Coverage.startMonitor
474-
reify[Value](SS.init(heap0))(comp)
474+
reify[Value](initState(heap0))(comp)
475475
}
476476
}

‎dev-clean/src/main/scala/sai/llsc/engines/ImpEngine.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -356,7 +356,7 @@ trait ImpLLSCEngine extends ImpSymExeDefs with EngineBase {
356356
Coverage.setBlockNum
357357
Coverage.incPath(1)
358358
Coverage.startMonitor
359-
val ss = SS.init(preHeap.asRepOf[Mem])
359+
val ss = initState(preHeap.asRepOf[Mem])
360360
if (!isCommandLine) {
361361
val fv = eval(GlobalId(fname), VoidType, ss)(fname)
362362
ss.push

‎dev-clean/src/main/scala/sai/llsc/engines/PureCPSEngine.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -335,7 +335,7 @@ trait PureCPSLLSCEngine extends SymExeDefs with EngineBase {
335335
Coverage.setBlockNum
336336
Coverage.incPath(1)
337337
Coverage.startMonitor
338-
val ss = SS.init(preHeap.asRepOf[Mem])
338+
val ss = initState(preHeap.asRepOf[Mem])
339339
if (!isCommandLine) {
340340
val fv = eval(GlobalId(fname), VoidType, ss)(fname)
341341
fv[Id](ss.push, args, k)

‎dev-clean/src/main/scala/sai/llsc/states/GenericDefs.scala‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -34,12 +34,10 @@ trait BasicDefs { self: SAIOps =>
3434
type PC = Set[SMTBool]
3535
type Id[T] = T
3636

37-
object SS {
38-
def init: Rep[SS] = "init-ss".reflectWriteWith[SS]()(Adapter.CTRL)
39-
def init(m: Rep[Mem]): Rep[SS] = "init-ss".reflectWriteWith[SS](m)(Adapter.CTRL)
40-
def checkPCToFile(s: Rep[SS]): Unit = "check_pc_to_file".reflectWriteWith[Unit](s)(Adapter.CTRL)
41-
def checkPC(pc: Rep[PC]): Rep[Boolean] = "check_pc".reflectWriteWith[Boolean](pc)(Adapter.CTRL)
42-
}
37+
def initState: Rep[SS] = "init-ss".reflectWriteWith[SS]()(Adapter.CTRL)
38+
def initState(m: Rep[Mem]): Rep[SS] = "init-ss".reflectWriteWith[SS](m)(Adapter.CTRL)
39+
def checkPCToFile(s: Rep[SS]): Unit = "check_pc_to_file".reflectWriteWith[Unit](s)(Adapter.CTRL)
40+
def checkPC(pc: Rep[PC]): Rep[Boolean] = "check_pc".reflectWriteWith[Boolean](pc)(Adapter.CTRL)
4341
}
4442

4543
trait Coverage { self: SAIOps =>
@@ -218,6 +216,8 @@ trait ValueDefs { self: SAIOps with BasicDefs =>
218216
def toSMTBool: Rep[SMTBool] = "to-SMT".reflectWith[SMTBool](v)
219217
def toSMTBoolNeg: Rep[SMTBool] = "to-SMTNeg".reflectWith[SMTBool](v)
220218

219+
def notNull: Rep[Boolean] = "not-null".reflectWith[Boolean](v)
220+
221221
def fp_toui(to: Int): Rep[Value] = "fp_toui".reflectWith[Value](v, to)
222222
def fp_tosi(to: Int): Rep[Value] = "fp_tosi".reflectWith[Value](v, to)
223223
def ui_tofp: Rep[Value] = "ui_tofp".reflectWith[Value](v)

‎dev-clean/src/main/scala/sai/lms/SAIOps.scala‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,9 @@ trait SAIOps extends Base
6464
def hardTopFun[A:Manifest,B:Manifest,C:Manifest](f: (Rep[A], Rep[B]) => Rep[C]): Rep[(A, B) => C] =
6565
Wrap[(A,B)=>C](__hardTopFun(f, 2, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1))))))
6666

67+
def hardTopFun[A:Manifest,B:Manifest,C:Manifest,D:Manifest](f: (Rep[A], Rep[B], Rep[C]) => Rep[D]): Rep[(A, B, C) => D] =
68+
Wrap[(A,B,C)=>D](__hardTopFun(f, 3, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)), Wrap[C](xn(2))))))
69+
6770
def __hardTopFun(f: AnyRef, arity: Int, gf: List[Backend.Exp] => Backend.Exp, decorator: String = ""): Backend.Exp = {
6871
val can = canonicalize(f)
6972
Adapter.funTable.find(_._2 == can) match {

0 commit comments

Comments
 (0)