Rewrite IR Interpreter

build.sbt

@@ -29,7 +29,7 @@ lazy val root = project
     libraryDependencies += "org.scalameta" %% "munit" % "0.7.29" % Test
   )
 
-scalacOptions ++= Seq("-deprecation", "-feature")
+scalacOptions ++= Seq("-deprecation", "-unchecked", "-feature")
 
 Compile / PB.targets := Seq(
   scalapb.gen() -> (Compile / sourceManaged).value / "scalapb"

build.sc

@@ -22,6 +22,7 @@ object basil extends RootModule with ScalaModule with antlr.AntlrModule with Sca
 
   def scalaPBVersion = "0.11.15"
 
+  def scalacOptions = Seq("-deprecation", "-unchecked", "-feature")
 
   def mainClass = Some("Main")
 

docs/development/interpreter.md

@@ -0,0 +1,203 @@
+# BASIL IR Interpreter
+
+The interpreter is designed for testing, debugging, and validation of static analyses and code transforms. 
+This page describes first how it can be used for this purpose, and secondly its design.
+
+## Basic Usage
+
+The interpreter can be invoked from the command line, via the interpret flag, by default this prints a trace and checks that the interpreter
+exited on a non-error stop state.
+
+```shell
+./mill run -i src/test/correct/indirect_call/gcc/indirect_call.adt -r src/test/correct/indirect_call/gcc/indirect_call.relf --interpret
+[INFO]   Interpreter Trace:
+         StoreVar(#5,Local,0xfd0:bv64)
+         StoreMem(mem,HashMap(0xfd0:bv64 -> 0xf0:bv8, 0xfd6:bv64 -> 0x0:bv8, 0xfd2:bv64 -> 0x0:bv8, 0xfd3:bv64 -> 0x0:bv8, 0xfd4:bv64 -> 0x0:bv8, 0xfd7:bv64 -> 0x0:bv8, 0xfd5:bv64 -> 0x0:bv8, 0xfd1
+...
+[INFO]   Interpreter stopped normally.
+```
+
+The `--verbose` flag can also be used, which may print interpreter trace events as they are executed, but not this may not correspond to the actual 
+execution trace, and contain additional events not corresponding to the program.
+E.g. this shows the memory intialisation events that precede the program execution. This is mainly useful for debugging the interpreter.
+
+### Testing with Interpreter
+
+The interpreter is invoked with `interpret(p: IRContext)` to interpret normally and return an `InterpreterState` object
+containing the final state. 
+
+#### Traces
+
+There is also, `interpretTrace(p: IRContext)` which returns a tuple of `(InterpreterState, Trace(t: List[ExecEffect]))`,
+where the second argument contains a list of all the events generated by the interpreter in order.
+This is useful for asserting a stronger equivalence between program executions, but in most cases events describing "unobservable"
+behaviour, such as register accesses should be filtered out from this list before comparison.
+
+To see an example of this used to validate the constant prop analysis see [/src/test/scala/DifferentialAnalysis.scala](../../src/test/scala/DifferentialAnalysis.scala).
+
+#### BreakPoints
+
+Finally `interpretBreakPoints(p: IRContext, breakpoints: List[BreakPoint])` is used to 
+run an interpreter and perform additional actions at specified code points. For example, this may be invoked such as:
+
+```scala
+val watch = IRWalk.firstInProc((program.procedures.find(_.name == "main")).get).get
+val bp = BreakPoint("entrypoint",  BreakPointLoc.CMD(watch), BreakPointAction(saveState=true, stop=true, evalExprs=List(("R0", Register("R0", 64))), log=true))
+val res = interpretBreakPoints(program, List(bp))
+```
+
+The structure of a breakpoint is as follows:
+
+```scala
+case class BreakPoint(name: String = "", location: BreakPointLoc, action: BreakPointAction)
+
+// the place to perform the breakpoint action
+enum BreakPointLoc:
+  case CMD(c: Command)                      // at a command c
+  case CMDCond(c: Command, condition: Expr) // at a command c, when condition evaluates to TrueLiteral
+
+// describes what to do when the breakpoint is triggered
+case class BreakPointAction(
+    saveState: Boolean = true,                // stash the state of the interpreter
+    stop: Boolean = false,                    // stop the interpreter with an error state
+    evalExprs: List[(String, Expr)] = List(), // Evaluate the rhs of the list of expressions, and stash them (lhs is an arbitrary human-readable name)
+    log: Boolean = false                      // Print a log message about passing the breakpoint describing the results of this action
+)
+```
+
+To see an example of this used to validate the constant prop analysis see [/src/test/scala/InterpretTestConstProp.scala](../../src/test/scala/InterpretTestConstProp.scala).
+
+### Resource Limit
+
+This kills the interpreter in an error state once a specified instruction count is reached, to avoid the interpreter running forever on infinite loops. 
+
+It can be used simply with the function `interptretRLimit`, this automatically ignores the initialisation instructions.
+
+```scala
+def interpretRLimit(p: IRContext, instructionLimit: Int) : InterpreterState
+```
+
+It can also be combined with other interpreters as shown:
+
+```scala
+def interp(p: IRContext, instructionLimit: Int) : (InterpreterState, Trace) = {
+  val interpreter = LayerInterpreter(tracingInterpreter(NormalInterpreter), EffectsRLimit(instructionLimit))
+  val initialState = InterpFuns.initProgState(NormalInterpreter)(p, InterpreterState())
+  BASILInterpreter(interpreter).run((initialState, Trace(List())), 0)._1
+}
+```
+
+## Implementation / Code Structure
+
+### Summary
+
+-  [Bitvector.scala](../../src/main/scala/ir/eval/Bitvector.scala)
+    - Evaluation of bitvector operations, throws `IllegalArgumentException` on violation of contract
+      (e.g negative divisor, type mismatch)
+-  [ExprEval.scala](../../src/main/scala/ir/eval/ExprEval.scala)
+    - Evaluation of expressions, defined in terms of partial evaluation down to a Literal
+    - This can also be used to evaluate expressions in static analyses, by passing a function to query variable assignments and memory state from the value domain. 
+-  [Interpreter.scala](../../src/main/scala/ir/eval/Interpreter.scala)
+    - Definition of core `Effects[S, E]` and `Interpreter[S, E]` types describing state transitions in 
+      the interpreter
+    - Instantiation/definition of `Effects` for concrete state `InterpreterState`
+-  [InterpreterProduct.scala](../../src/main/scala/ir/eval/InterpreterProduct.scala)
+    - Definition of product and layering composition of generic `Effects[S, E]`s interpreters
+-  [InterpretBasilIR.scala](../../src/main/scala/ir/eval/InterpretBasilIR.scala)
+    - Definition of `Eval` object defining expression evaluation in terms of `Effects[S, InterpreterError]`
+    - Definition of `Interpreter` instance for BASIL IR, using a generic `Effects` instance and concrete state.
+    - Definition of ELF initialisation in terms of generic `Effects[S, InterpreterError]`
+-  [InterpretBreakpoints.scala](../../src/main/scala/ir/eval/InterpretBreakpoints.scala)
+    - Definition of a generic interpreter with a breakpoint checker layered on top
+-  [interpretRLimit.scala](../../src/main/scala/ir/eval/InterpretRLimit.scala)
+    - Definition of layered interpreter which terminates after a specified cycle count
+-  [InterpretTrace.scala](../../src/main/scala/ir/eval/InterpretTrace.scala)
+    - Definition of a generic interpreter which records a trace of calls to the `Effects[]` instance. 
+
+### Explanation
+
+The interpreter is structured for compositionality, at its core is the `Effects[S, E]` type, defined in [Interpreter.scala](../../src/main/scala/ir/eval/Interpreter.scala). 
+This type defines a small set of functions which describe all the possible state transformations, over a concrete state `S`, and error type `E` (always `InterpreterError` in practice). 
+
+This is implemented using the state Monad, `State[S,V,E]` where `S` is the state, `V` the value, and `E` the error type. 
+This is a flattened `State[S, Either[E]]`, defined in [util/functional.scala](../../src/main/scala/util/functional.scala).
+`Effects` methods return delayed computations, functions from an input state (`S`) to a resulting state and a value (`(S, Either[E, V])`). 
+These are sequenced using `flatMap` (monad bind), or the `for{} yield()` syntax sugar for flatMap. 
+
+This `Effects[S, E]` is instantiated for a given concrete state, the main example of which is `NormalInterpreter <: Effects[InterpreterState, InterpreterError]`,
+also defined in `Interpreter.scala`. The memory component of the state is abstracted further into the `MemoryState` object.
+
+The actual execution of code is defined on top of this, in the `Interpreter[S, E]` type, which takes an instance of the `Effects` by parameter, 
+and defines both the small step (`interpretOne`) over on instruction, and the fixed point to termination from some in initial state in `run()`.
+The fact that the stepping is defined outside the effects is important, as it allows concrete states, and state transitions over them to be 
+composed somewhat arbitrarily, and the interpretatation of the language compiled down to calls to resulting instance of `Effects`.
+
+This is defined in [InterpretBasilIR.scala](../../src/main/scala/ir/eval/InterpretBasilIR.scala). `BASILInterpreter` defines an 
+`Interpreter` over an arbitrary instance of `Effects[S, InterpreterError]`, encoding BASIL IR commands as effects. 
+This file also contains definitions of the initial memory state setup of the interpreter, based on the ELF sections and symbol table.
+
+### Composition of interpreters
+
+There are two ways to compose `Effects`, product and layer. Both produce an instance of `Effects[(L, R), E]`, 
+where `L` and `R` are the concrete state types of the two Effects being composed. 
+
+Product runs the two effects, over two different concrete state types, simultaneously without interaction. 
+
+Layer runs the `before` effect first, and passes its state to the `inner` effect whose value is returned. 
+
+```scala
+case class ProductInterpreter[L, T, E](val inner: Effects[L, E], val before: Effects[T, E]) extends Effects[(L, T), E] {
+case class LayerInterpreter[L, T, E](val inner: Effects[L, E], val before: Effects[(L, T), E])
+```
+
+Examples of using these are in the `interpretTrace` and `interpretWithBreakPoints` interpreters respectively.
+
+Note, this only works by the aforementioned requirement that all effect calls come from outside the `Effects[]`
+instance itself. In the simple case, the `Interpreter` instance is the only object calling `Effects`. 
+This means, `Effects` triggered by an inner `Effects[]` instance do not flow back to the `ProductInterpreter`, 
+but only appear from when `Interpreter` above the `ProductInterpreter` interprets the program via effect calls. 
+For this reason if, for example, `NormalInterpreter` makes effect calls they will not appear in a trace emitted by `interptretTrace`. 
+
+### Note on memory space initialisation 
+
+Most of the interpret functions are overloaded such that there is a version taking a program `interpret(p: Program)`, 
+and a version taking `IRContext`. The variant taking IRContext uses the ELF symbol information to initialise the 
+memory before interpretation. If you are interpreting a real program (i.e. not a synthetic example created through 
+the DSL), this is most likely required.
+
+We initialise:
+
+- The general interpreter state, stack and memory regions, stack pointer, a symbolic mapping from addresses functions
+- The initial and readonly memory sections stored in Program
+- The `.bss` section to zero
+- The relocation table. Each listed offset is stored an address to either a real procedure in the program, or a 
+  location storing a symbolic function pointer to an intrinsic function.
+
+`.bss` is generally the top of the initialised data, the ELF symbol `__bss_end__` being equal to the symbol `__end__`.
+Above this we can somewhat choose arbitrarily where to put things, usually the heap is above, followed by 
+dynamically linked symbols, then the stack. There is currently no stack overflow checking, or heap implemented in the 
+interpreter.
+
+Unfortunately these details are defined by the load-time linker and the system's linker script, and it is hard to find a good description
+of their behaviour. Some details are described here https://refspecs.linuxfoundation.org/elf/elf.pdf, and here 
+https://dl.acm.org/doi/abs/10.1145/2983990.2983996.
+
+### Missing features
+
+- There is functionality to implement external function calls via intrinsics written in Scala code, but currently only 
+  basic printf style functions are implemented as no-ops. These can be extended to use a file IO abstraction, where
+  a memory region is created for each file (e.g. stdout), with a variable to keep track of the current write-point
+  such that a file write operation stores to the write-point address, and increments it by the size of the store.
+  Importantly, an implementation of malloc() and free() is needed, which can implement a simple greedy allocation 
+  algorithm.
+- Despite the presence of procedure parameters in the current IR, they are not used for by the boogie translation and 
+  are hence similarly ignored in the interpreter.
+- The interpreter's immutable state representation is motivated by the ability to easily implement a sound approach
+  to non-determinism, e.g. to implement GoTos with guessing and rollback rather than look-ahead. This is more
+  useful for checking specification constructs than executing real programs, so is not yet implemented.
+- The trace does not clearly distinguish internal vs external calls, or observable 
+  and non-observable behaviour.
+- While the interpreter semantics supports memory regions, we do not initialise the memory regions (or the initial memory state) 
+  based on those present in the program, we simply assume a flat `mem` and `stack` memory partitioning.
+
+

docs/development/readme.md

@@ -5,6 +5,7 @@
 - [tool-installation](tool-installation.md) Guide to lifter, etc. tool installation
 - [scala](scala.md) Advice on Scala programming.
 - [cfg](cfg.md) Explanation of the old CFG datastructure 
+- [interpreter](interpreter.md) Explanation of IR interpreter
 
 
 ## Scala

docs/readme.md

@@ -12,6 +12,7 @@ To get started on development, see [development](development).
     - [editor-setup](development/editor-setup.md) Guide to basil development in IDEs 
     - [tool-installation](development/tool-installation.md) Guide to lifter, etc. tool installation
     - [cfg](development/cfg.md) Explanation of the old CFG datastructure 
+    - [interpreter](development/interpreter.md) Explanation of IR interpreter
 - [basil-ir](basil-ir.md) explanation of BASIL's intermediate representation
 - [compiler-explorer](compiler-explorer.md) guide to the compiler explorer basil interface
 - [il-cfg](il-cfg.md) explanation of the IL cfg iterator design

src/main/scala/analysis/Lattice.scala

@@ -1,7 +1,7 @@
 package analysis
 
 import ir._
-import analysis.BitVectorEval
+import ir.eval.BitVectorEval
 import util.Logger
 
 /** Basic lattice
@@ -244,4 +244,4 @@ class ConstantPropagationLatticeWithSSA extends PowersetLattice[BitVecLiteral] {
     apply(BitVectorEval.boogie_extract(high, low, _: BitVecLiteral), a)
 
   def concat(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_concat, a, b)
-}
+}

src/main/scala/analysis/MemoryRegionAnalysis.scala

@@ -1,6 +1,6 @@
 package analysis
 
-import analysis.BitVectorEval.isNegative
+import ir.eval.BitVectorEval.isNegative
 import analysis.solvers.SimpleWorklistFixpointSolver
 import ir.*
 import util.Logger

src/main/scala/analysis/RegionInjector.scala

@@ -1,6 +1,6 @@
 package analysis
 
-import analysis.BitVectorEval.isNegative
+import ir.eval.BitVectorEval.isNegative
 import ir.*
 import util.Logger
 

src/main/scala/analysis/UtilMethods.scala

@@ -1,6 +1,7 @@
 package analysis
 import ir.*
 import util.Logger
+import ir.eval.BitVectorEval
 
 /** Evaluate an expression in a hope of finding a global variable.
   *
@@ -12,62 +13,14 @@ import util.Logger
   *   The evaluated expression (e.g. 0x69632)
   */
 def evaluateExpression(exp: Expr, constantPropResult: Map[Variable, FlatElement[BitVecLiteral]]): Option[BitVecLiteral] = {
-  exp match {
-    case binOp: BinaryExpr =>
-      val lhs = evaluateExpression(binOp.arg1, constantPropResult)
-      val rhs = evaluateExpression(binOp.arg2, constantPropResult)
+  def value(v: Variable) = constantPropResult(v) match {
+    case FlatEl(value) => Some(value)
+    case _             => None
+  }
 
-      (lhs, rhs) match {
-        case (Some(l: BitVecLiteral), Some(r: BitVecLiteral)) =>
-          val result = binOp.op match {
-            case BVADD => BitVectorEval.smt_bvadd(l, r)
-            case BVSUB => BitVectorEval.smt_bvsub(l, r)
-            case BVMUL => BitVectorEval.smt_bvmul(l, r)
-            case BVUDIV => BitVectorEval.smt_bvudiv(l, r)
-            case BVSDIV => BitVectorEval.smt_bvsdiv(l, r)
-            case BVSREM => BitVectorEval.smt_bvsrem(l, r)
-            case BVUREM => BitVectorEval.smt_bvurem(l, r)
-            case BVSMOD => BitVectorEval.smt_bvsmod(l, r)
-            case BVAND => BitVectorEval.smt_bvand(l, r)
-            case BVOR => BitVectorEval.smt_bvxor(l, r)
-            case BVXOR => BitVectorEval.smt_bvxor(l, r)
-            case BVNAND => BitVectorEval.smt_bvnand(l, r)
-            case BVNOR => BitVectorEval.smt_bvnor(l, r)
-            case BVXNOR => BitVectorEval.smt_bvxnor(l, r)
-            case BVSHL => BitVectorEval.smt_bvshl(l, r)
-            case BVLSHR => BitVectorEval.smt_bvlshr(l, r)
-            case BVASHR => BitVectorEval.smt_bvashr(l, r)
-            case BVCOMP => BitVectorEval.smt_bvcomp(l, r)
-            case BVCONCAT => BitVectorEval.smt_concat(l, r)
-            case x => throw RuntimeException("Binary operation support not implemented: " + binOp.op)
-          }
-          Some(result)
-        case _ => None
-      }
-    case extend: ZeroExtend =>
-      evaluateExpression(extend.body, constantPropResult) match {
-        case Some(b: BitVecLiteral) => Some(BitVectorEval.smt_zero_extend(extend.extension, b))
-        case None                => None
-      }
-    case extend: SignExtend =>
-      evaluateExpression(extend.body, constantPropResult) match {
-        case Some(b: BitVecLiteral) => Some(BitVectorEval.smt_sign_extend(extend.extension, b))
-        case None => None
-      }
-    case e: Extract =>
-      evaluateExpression(e.body, constantPropResult) match {
-        case Some(b: BitVecLiteral) => Some(BitVectorEval.boogie_extract(e.end, e.start, b))
-        case None               => None
-      }
-    case variable: Variable =>
-      constantPropResult(variable) match {
-        case FlatEl(value) => Some(value)
-        case Top           => None
-        case Bottom        => None
-      }
-    case b: BitVecLiteral => Some(b)
-    case _ => //throw new RuntimeException("ERROR: CASE NOT HANDLED: " + exp + "\n")
-      None
+  ir.eval.evalBVExpr(exp, value) match {
+    case Right(v) => Some(v)
+    case Left(_) => None
   }
 }
 

src/main/scala/analysis/data_structure_analysis/LocalPhase.scala

@@ -1,6 +1,6 @@
 package analysis.data_structure_analysis
 
-import analysis.BitVectorEval.{bv2SignedInt, isNegative}
+import ir.eval.BitVectorEval.{bv2SignedInt, isNegative}
 import analysis.*
 import ir.*
 import specification.{ExternalFunction, SpecGlobal, SymbolTableEntry}

src/main/scala/analysis/data_structure_analysis/SymbolicAddressAnalysis.scala

@@ -1,6 +1,6 @@
 package analysis.data_structure_analysis
 
-import analysis.BitVectorEval.{bv2SignedInt, isNegative}
+import ir.eval.BitVectorEval.{bv2SignedInt, isNegative}
 import analysis.solvers.ForwardIDESolver
 import analysis.*
 import ir.*

src/main/scala/ir/Expr.scala

@@ -16,18 +16,22 @@ sealed trait Literal extends Expr {
   override def acceptVisit(visitor: Visitor): Literal = visitor.visitLiteral(this)
 }
 
-sealed trait BoolLit extends Literal
+sealed trait BoolLit extends Literal {
+  def value: Boolean
+}
 
 case object TrueLiteral extends BoolLit {
   override def toBoogie: BoolBLiteral = TrueBLiteral
   override def getType: IRType = BoolType
   override def toString: String = "true"
+  override def value = true
 }
 
 case object FalseLiteral extends BoolLit {
   override def toBoogie: BoolBLiteral = FalseBLiteral
   override def getType: IRType = BoolType
   override def toString: String = "false"
+  override def value = false
 }
 
 case class BitVecLiteral(value: BigInt, size: Int) extends Literal {