Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplification pass #256

Open
wants to merge 113 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
113 commits
Select commit Hold shift + click to select a range
182c9e8
refactor call to a statement & add unreachable and return jumps
ailrst Aug 19, 2024
3711e4d
move transforms out of RunUtils.scala
ailrst Aug 19, 2024
fd56c9a
remove old cfg
ailrst Aug 9, 2024
bd6b2ad
update docs
ailrst Aug 19, 2024
96b9028
pe based expr evaluator
ailrst Aug 19, 2024
d264b97
interpreter test
ailrst Aug 19, 2024
a3bf83b
rewrite interpreter in functional style
ailrst Aug 22, 2024
74c4bc2
cleanup call/return
ailrst Aug 22, 2024
9e23558
cleanup memory ops to enter effects
ailrst Aug 22, 2024
7571aa3
tracing interpreter
ailrst Aug 26, 2024
f36c13e
compile with state monad
ailrst Aug 27, 2024
2c16c83
fix state monad interp
ailrst Aug 28, 2024
dd11175
indirect calls
ailrst Aug 28, 2024
c7b4a56
tracing interpreter
ailrst Aug 28, 2024
f64f904
breakpoints
ailrst Aug 28, 2024
897c565
improve breakpoints
ailrst Aug 29, 2024
cc97052
reorg
ailrst Aug 29, 2024
695b2d2
refactor with statemonad[s, either[v]]
ailrst Aug 29, 2024
00b482a
redo error handling
ailrst Aug 29, 2024
1a139d2
refactor call to a statement & add unreachable and return jumps
ailrst Aug 19, 2024
7e94536
move transforms out of RunUtils.scala
ailrst Aug 19, 2024
aae0064
remove old cfg
ailrst Aug 9, 2024
e2c0cd4
update docs
ailrst Aug 19, 2024
a3adee3
fix
ailrst Aug 30, 2024
4a92c99
fix externals
ailrst Aug 30, 2024
b994c99
disable IDE analyses if mainproc is external
ailrst Aug 30, 2024
b83c9ff
Merge branch 'call-statement' into interpreter
ailrst Aug 30, 2024
d6c5767
work on differential testing
ailrst Aug 30, 2024
2a03a23
hook for dynlinking
ailrst Sep 2, 2024
8b694c0
load full symtab
ailrst Sep 2, 2024
57ca6b3
update relf grammar
ailrst Sep 3, 2024
b276981
init bss
ailrst Sep 3, 2024
888d360
cleanup
ailrst Sep 3, 2024
0abf654
cleanup init trace
ailrst Sep 3, 2024
9192ce3
intrinsic stub and cleanup errors
ailrst Sep 3, 2024
5342358
init relocation table
ailrst Sep 3, 2024
87b0f86
pull stepper outside effects to fix interpreter composition again
ailrst Sep 4, 2024
f5a0590
cleanup
ailrst Sep 4, 2024
a6b58e8
cleanup
ailrst Sep 4, 2024
dd64c14
constprop test with interpreter
ailrst Sep 4, 2024
8be5cb6
interpreter docs
ailrst Sep 4, 2024
d2a2486
fix list
ailrst Sep 4, 2024
d06e268
paragraph
ailrst Sep 4, 2024
4ae3997
trap eval exceptions to monadic errors
ailrst Sep 4, 2024
4fc8ed2
improve interpretOne
ailrst Sep 4, 2024
8f966ce
notes on initialisation
ailrst Sep 4, 2024
f00b44b
simplify invoc funcs
ailrst Sep 4, 2024
ceef233
note missing features
ailrst Sep 5, 2024
cff6c97
run through all system tests
ailrst Sep 5, 2024
822c127
add resource limit
ailrst Sep 5, 2024
9b8f715
doc resource limit
ailrst Sep 5, 2024
648a41d
tweak doc
ailrst Sep 5, 2024
dfa7209
fix
ailrst Sep 5, 2024
38f871c
tweak interpretrlimit
ailrst Sep 5, 2024
6559180
basic malloc implementation
ailrst Sep 9, 2024
c6e938d
implement printf
ailrst Sep 10, 2024
285099b
cleanup intrins
ailrst Sep 10, 2024
aac7f5c
cleanup
ailrst Sep 23, 2024
1c2a5d5
Merge remote-tracking branch 'upstream/main' into interpreter
ailrst Sep 23, 2024
46ff66a
cleanup
ailrst Sep 23, 2024
f45015b
initial attempt at IR simplification
ailrst Sep 25, 2024
7769357
fixup analysis
ailrst Sep 25, 2024
533ccce
wl optim
ailrst Sep 25, 2024
febadbd
rename w ssa
ailrst Sep 25, 2024
4465cfb
tweak ssa
ailrst Sep 20, 2024
a6cc33f
change param to localvar
ailrst Sep 30, 2024
750d949
distinguish lvars and rvars in cilvisitor
ailrst Sep 30, 2024
c9c4181
transform ir and spec and loader to have params
ailrst Oct 1, 2024
f83fd74
cleanup spec param handling
ailrst Oct 2, 2024
3fce1c9
update visitor
ailrst Oct 2, 2024
eef39b9
add invariant check
ailrst Oct 2, 2024
9b87104
Merge branch 'procedure-call-abstraction' into xf
ailrst Oct 2, 2024
a21015c
fix test issues in merge
ailrst Oct 2, 2024
409c455
make simplify work with params
ailrst Oct 2, 2024
81fd5e4
improve dsa and params w liveness
ailrst Oct 4, 2024
8e99918
fix dsa, copyprop, cleanup
ailrst Oct 8, 2024
495e4f2
small fix
ailrst Oct 10, 2024
e567f77
rewrites
ailrst Oct 15, 2024
5c42e92
remove slices
ailrst Oct 16, 2024
41aa3d7
disable bad
ailrst Oct 16, 2024
24a12e3
attempt at condition lifting
ailrst Oct 17, 2024
8bf3e4d
cleanup
ailrst Oct 17, 2024
f75086e
add example
ailrst Oct 17, 2024
c26028e
add expr2smt
ailrst Oct 18, 2024
09eb1af
validate and improve expr lifting
ailrst Oct 18, 2024
8b4fd6f
transform order
ailrst Oct 18, 2024
bc48e00
cleanup and perf
ailrst Oct 19, 2024
f2adf72
add early proc trim and fix remove unreachable cfg maintenance
ailrst Oct 22, 2024
a6d302f
flow insensitive copyprop and single pass dsa
ailrst Oct 23, 2024
f313ed3
block coalescing
ailrst Oct 31, 2024
95744f7
booltobv1 and copyprop heuristic
ailrst Nov 1, 2024
70a22c1
WIP bitvector size type inference
ailrst Nov 1, 2024
760bc0a
copyprop completeness improvements
ailrst Nov 5, 2024
2b2a0a5
improvements to cond identification
ailrst Nov 6, 2024
6ea3b1a
improve shift/extend/extract removal
ailrst Nov 7, 2024
3beb84d
improve cond detection
ailrst Nov 7, 2024
7c0c98b
revert to old slice removal
ailrst Nov 7, 2024
a7d0754
cleanup
ailrst Nov 7, 2024
80491cb
validate and improve condition reduction
ailrst Nov 8, 2024
983597c
new prettyprinter
ailrst Nov 11, 2024
08af7a3
docs and cleanup
ailrst Nov 12, 2024
d3b8176
ccmp and rpo sort
ailrst Nov 13, 2024
0f9a756
Merge branch 'main' of github.com:UQ-PAC/bil-to-boogie-translator int…
ailrst Nov 13, 2024
a452165
work on adding param support to interpreter
ailrst Nov 29, 2024
b9c549c
multiple loggers
ailrst Dec 2, 2024
8dd5f0e
fix externalremover
ailrst Dec 3, 2024
21efc16
robustness and perf fixes (monad overflow)
ailrst Dec 3, 2024
797dc2b
Merge branch 'main' into simp-pass-main-merge
b-paul Dec 10, 2024
a824c07
prettyprinter
ailrst Dec 5, 2024
015edd3
Merge branch 'ilparser-serialiser' of github.com:ailrst/basil into si…
ailrst Dec 10, 2024
38f927b
run simplify after analysis
ailrst Dec 10, 2024
8329c11
Merge pull request #285 from UQ-PAC/simp-pass-main-merge
ailrst Dec 10, 2024
a082b35
dont try to <8bit initial memory regions
ailrst Dec 19, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
pull stepper outside effects to fix interpreter composition again
  • Loading branch information
ailrst committed Sep 4, 2024
commit 87b0f86d3632290c00a5a66a8df61a6b085ca18b
233 changes: 120 additions & 113 deletions src/main/scala/ir/eval/InterpretBasilIR.scala
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,116 @@ case object Eval {
}
}


class BASILInterpreter[S](f: Effects[S, InterpreterError]) extends Interpreter[S, InterpreterError](f) {

def interpretOne: State[S, Unit, InterpreterError] = for {
next <- f.getNext
_ <- (next match {
case CallIntrinsic(tgt) => LibcIntrinsic.intrinsics(tgt)(f)
case Run(c: Statement) => interpretStatement(f)(c)
case Run(c: Jump) => interpretJump(f)(c)
case Stopped() => State.pure(())
case ErrorStop(e) => State.pure(())
}).flatMapE((e: InterpreterError) => f.setNext(ErrorStop(e)))
} yield ()

def interpretJump[S, T <: Effects[S, InterpreterError]](f: T)(j: Jump): State[S, Unit, InterpreterError] = {
j match {
case gt: GoTo if gt.targets.size == 1 => {
f.setNext(Run(IRWalk.firstInBlock(gt.targets.head)))
}
case gt: GoTo =>
val assumes = gt.targets.flatMap(_.statements.headOption).collect { case a: Assume =>
a
}
for {
_ <-
if (assumes.size != gt.targets.size) {
State.setError((Errored(s"Some goto target missing guard $gt")))
} else {
State.pure(())
}
chosen: List[Assume] <- filterM((a: Assume) => Eval.evalBool(f)(a.body), assumes)

res <- chosen match {
case Nil => State.setError(Errored(s"No jump target satisfied $gt"))
case h :: Nil => f.setNext(Run(h))
case h :: tl => State.setError(Errored(s"More than one jump guard satisfied $gt"))
}
} yield (res)
case r: Return => f.doReturn()
case h: Unreachable => State.setError(EscapedControlFlow(h))
}
}

def interpretStatement[S, T <: Effects[S, InterpreterError]](f: T)(s: Statement): State[S, Unit, InterpreterError] = {
s match {
case assign: Assign => {
for {
rhs <- Eval.evalBV(f)(assign.rhs)
st <- f.storeVar(assign.lhs.name, assign.lhs.toBoogie.scope, Scalar(rhs))
n <- f.setNext(Run(s.successor))
} yield (st)
}
case assign: MemoryAssign =>
for {
index: BitVecLiteral <- Eval.evalBV(f)(assign.index)
value: BitVecLiteral <- Eval.evalBV(f)(assign.value)
_ <- Eval.storeBV(f)(assign.mem.name, Scalar(index), value, assign.endian)
n <- f.setNext(Run(s.successor))
} yield (n)
case assert: Assert =>
for {
b <- Eval.evalBool(f)(assert.body)
n <-
(if (!b) then {
f.setNext(FailedAssertion(assert))
} else {
f.setNext(Run(s.successor))
})
} yield (n)
case assume: Assume =>
for {
b <- Eval.evalBool(f)(assume.body)
n <-
(if (!b) {
State.setError(Errored(s"Assumption not satisfied: $assume"))
} else {
f.setNext(Run(s.successor))
})
} yield (n)
case dc: DirectCall =>
for {
n <-
if (dc.target.entryBlock.isDefined) {
val block = dc.target.entryBlock.get
f.call(dc.target.name, Run(block.statements.headOption.getOrElse(block.jump)), Run(dc.successor))
} else if (LibcIntrinsic.intrinsics.contains(dc.target.name)) {
f.call(dc.target.name, CallIntrinsic(dc.target.name), Run(dc.successor))
} else {
State.setError(EscapedControlFlow(dc))
}
} yield (n)
case ic: IndirectCall => {
if (ic.target == Register("R30", 64)) {
f.doReturn()
} else {
for {
addr <- Eval.evalBV(f)(ic.target)
fp <- f.evalAddrToProc(addr.value.toInt)
_ <- fp match {
case Some(fp) => f.call(fp.name, fp.call, Run(ic.successor))
case none => State.setError(EscapedControlFlow(ic))
}
} yield ()
}
}
case _: NOP => f.setNext(Run(s.successor))
}
}
}

object InterpFuns {

def initRelocTable[S, T <: Effects[S, InterpreterError]](s: T)(ctx: IRContext): State[S, Unit, InterpreterError] = {
Expand All @@ -244,7 +354,6 @@ object InterpFuns {

for ((fname, fun) <- LibcIntrinsic.intrinsics) {
val name = fname.takeWhile(c => c != '@')
println(name)
x = (name, FunPointer(BitVecLiteral(newAddr(), 64), name, CallIntrinsic(name))) :: x
}

Expand Down Expand Up @@ -340,117 +449,6 @@ object InterpFuns {
} yield (r)
}

def interpretJump[S, T <: Effects[S, InterpreterError]](f: T)(j: Jump): State[S, Unit, InterpreterError] = {
j match {
case gt: GoTo if gt.targets.size == 1 => {
f.setNext(Run(IRWalk.firstInBlock(gt.targets.head)))
}
case gt: GoTo =>
val assumes = gt.targets.flatMap(_.statements.headOption).collect { case a: Assume =>
a
}
for {
_ <-
if (assumes.size != gt.targets.size) {
State.setError((Errored(s"Some goto target missing guard $gt")))
} else {
State.pure(())
}
chosen: List[Assume] <- filterM((a: Assume) => Eval.evalBool(f)(a.body), assumes)

res <- chosen match {
case Nil => State.setError(Errored(s"No jump target satisfied $gt"))
case h :: Nil => f.setNext(Run(h))
case h :: tl => State.setError(Errored(s"More than one jump guard satisfied $gt"))
}
} yield (res)
case r: Return => f.doReturn()
case h: Unreachable => State.setError(EscapedControlFlow(h))
}
}

def interpretStatement[S, T <: Effects[S, InterpreterError]](f: T)(s: Statement): State[S, Unit, InterpreterError] = {
s match {
case assign: Assign => {
for {
rhs <- Eval.evalBV(f)(assign.rhs)
st <- f.storeVar(assign.lhs.name, assign.lhs.toBoogie.scope, Scalar(rhs))
n <- f.setNext(Run(s.successor))
} yield (st)
}
case assign: MemoryAssign =>
for {
index: BitVecLiteral <- Eval.evalBV(f)(assign.index)
value: BitVecLiteral <- Eval.evalBV(f)(assign.value)
_ <- Eval.storeBV(f)(assign.mem.name, Scalar(index), value, assign.endian)
n <- f.setNext(Run(s.successor))
} yield (n)
case assert: Assert =>
for {
b <- Eval.evalBool(f)(assert.body)
n <-
(if (!b) then {
f.setNext(FailedAssertion(assert))
} else {
f.setNext(Run(s.successor))
})
} yield (n)
case assume: Assume =>
for {
b <- Eval.evalBool(f)(assume.body)
n <-
(if (!b) {
State.setError(Errored(s"Assumption not satisfied: $assume"))
} else {
f.setNext(Run(s.successor))
})
} yield (n)
case dc: DirectCall =>
for {
n <-
if (dc.target.entryBlock.isDefined) {
val block = dc.target.entryBlock.get
f.call(dc.target.name, Run(block.statements.headOption.getOrElse(block.jump)), Run(dc.successor))
} else if (LibcIntrinsic.intrinsics.contains(dc.target.name)) {
f.call(dc.target.name, CallIntrinsic(dc.target.name), Run(dc.successor))
} else {
State.setError(EscapedControlFlow(dc))
}
} yield (n)
case ic: IndirectCall => {
if (ic.target == Register("R30", 64)) {
f.doReturn()
} else {
for {
addr <- Eval.evalBV(f)(ic.target)
fp <- f.evalAddrToProc(addr.value.toInt)
_ <- fp match {
case Some(fp) => f.call(fp.name, fp.call, Run(ic.successor))
case none => State.setError(EscapedControlFlow(ic))
}
} yield ()
}
}
case _: NOP => f.setNext(Run(s.successor))
}
}

def interpret[S, E, T <: Effects[S, E]](f: T, m: S): S = {
// run to fixed point
var o = m
var n = State.execute(o, f.interpretOne)
while (o != n) {
o = n
n = State.execute(o, f.interpretOne)
}
n
}

def interpretProg[S, T <: Effects[S, InterpreterError]](f: T)(p: Program, is: S): S = {
val begin = State.execute(is, initialiseProgram(f)(p))
interpret(f, begin)
}

def initBSS[S, T <: Effects[S, InterpreterError]](f: T)(p: IRContext): State[S, Unit, InterpreterError] = {
val bss = for {
first <- p.symbols.find(s => s.name == "__bss_start__").map(_.value)
Expand All @@ -475,9 +473,18 @@ object InterpFuns {
State.execute(is, st)
}

/* Intialise from ELF and Interpret program */
def interpretProg[S, T <: Effects[S, InterpreterError]](f: T)(p: IRContext, is: S): S = {
val begin = initProgState(f)(p, is)
interpret(f, begin)
val interp = BASILInterpreter(f)
interp.run(begin)
}

/* Interpret IR program */
def interpretProg[S, T <: Effects[S, InterpreterError]](f: T)(p: Program, is: S): S = {
val begin = State.execute(is, initialiseProgram(f)(p))
val interp = BASILInterpreter(f)
interp.run(begin)
}
}

Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/ir/eval/InterpretBreakpoints.scala
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ case class RememberBreakpoints[T, I <: Effects[T, InterpreterError]](val f: I, v
}, breaks)
}

override def interpretOne : State[(T, List[(BreakPoint, Option[T], List[(String, Expr, Expr)])]), Unit, InterpreterError] = for {
override def getNext: State[(T, List[(BreakPoint, Option[T], List[(String, Expr, Expr)])]), ExecutionContinuation, InterpreterError] = for {
v : ExecutionContinuation <- doLeft(f.getNext)
n <- v match {
case Run(s) => for {
Expand Down Expand Up @@ -68,7 +68,7 @@ case class RememberBreakpoints[T, I <: Effects[T, InterpreterError]](val f: I, v
} yield ()
case _ => State.pure(())
}
} yield ()
} yield (v)

}

Expand Down
38 changes: 24 additions & 14 deletions src/main/scala/ir/eval/Interpreter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -76,9 +76,7 @@ case object BasilValue {
/** Minimal language defining all state transitions in the interpreter, defined for the interpreter's concrete state T.
*/
trait Effects[T, E] {

// perform an execution step
def interpretOne: State[T, Unit, E]
/* expression eval */

def loadVar(v: String): State[T, BasilValue, E]

Expand Down Expand Up @@ -108,7 +106,6 @@ trait Effects[T, E] {
}

trait NopEffects[T, E] extends Effects[T, E] {
def interpretOne = State.pure(())
def loadVar(v: String) = State.pure(Scalar(FalseLiteral))
def loadMem(v: String, addrs: List[BasilValue]) = State.pure(List())
def evalAddrToProc(addr: Int) = State.pure(None)
Expand Down Expand Up @@ -418,16 +415,29 @@ object NormalInterpreter extends Effects[InterpreterState, InterpreterError] {
ms <- s.memoryState.doStore(vname, update)
} yield (s.copy(memoryState = ms))
})
}

trait Interpreter[S, E](val f: Effects[S, E]) {

def interpretOne: State[S, Unit, E]

def interpretOne: State[InterpreterState, Unit, InterpreterError] = for {
next <- getNext
_ <- (next match {
case CallIntrinsic(tgt) => LibcIntrinsic.intrinsics(tgt)(this)
case Run(c: Statement) => InterpFuns.interpretStatement(this)(c)
case Run(c: Jump) => InterpFuns.interpretJump(this)(c)
case Stopped() => State.pure(())
case ErrorStop(e) => State.pure(())
}).flatMapE((e: InterpreterError) => setNext(ErrorStop(e)))
} yield ()
@tailrec
final def run(begin: S): S = {
val c = for {
_ <- interpretOne
x <- f.getNext
continue = x match {
case Stopped() | ErrorStop(_) => false
case _ => true
}
} yield (continue)

val (fs,cont) = c.f(begin)

if (cont.contains(true)) then {
run(fs)
} else {
fs
}
}
}
17 changes: 4 additions & 13 deletions src/main/scala/ir/eval/InterpreterProduct.scala
Original file line number Diff line number Diff line change
Expand Up @@ -16,27 +16,23 @@ import scala.util.control.Breaks.{break, breakable}


def doLeft[L, T, V, E](f: State[L, V, E]) : State[(L, T), V, E] = for {
f <- State[(L, T), V, E]((s: (L, T)) => {
n <- State[(L, T), V, E]((s: (L, T)) => {
val r = f.f(s._1)
((r._1, s._2), r._2)
})
} yield (f)
} yield (n)

def doRight[L, T, V, E](f: State[T, V, E]) : State[(L, T), V, E] = for {
f <- State[(L, T), V, E]((s: (L, T)) => {
n <- State[(L, T), V, E]((s: (L, T)) => {
val r = f.f(s._2)
((s._1, r._1), r._2)
})
} yield (f)
} yield (n)

/**
* Runs two interpreters "inner" and "before" simultaneously, returning the value from inner, and ignoring before
*/
case class ProductInterpreter[L, T, E](val inner: Effects[L, E], val before: Effects[T, E]) extends Effects[(L, T), E] {
def interpretOne = for {
n <- doRight(before.interpretOne)
f <- doLeft(inner.interpretOne)
} yield ()

def loadVar(v: String) = for {
n <- doRight(before.loadVar(v))
Expand Down Expand Up @@ -88,11 +84,6 @@ case class ProductInterpreter[L, T, E](val inner: Effects[L, E], val before: Eff

case class LayerInterpreter[L, T, E](val inner: Effects[L, E], val before: Effects[(L, T), E]) extends Effects[(L, T), E] {

def interpretOne = for {
n <- (before.interpretOne)
f <- doLeft(inner.interpretOne)
} yield ()

def loadVar(v: String) = for {
n <- (before.loadVar(v))
f <- doLeft(inner.loadVar(v))
Expand Down
Loading