Specification Improvements

src/main/antlr4/Specifications.g4

@@ -18,16 +18,17 @@ relies: 'Rely:' expr (COMMA expr)*;
 guarantees: 'Guarantee:' expr (COMMA expr)*;
 
 directFunctions: 'DIRECT functions:' directFunction (COMMA directFunction)*;
-directFunction: 'memory_load' size=nat endian #memoryLoad
-              | 'memory_store' size=nat endian #memoryStore
-              | 'gamma_load' size=nat #gammaLoad
-              | 'gamma_store' size=nat #gammaStore
-              | 'zero_extend' size1=nat UNDERSCORE size2=nat #zeroExtend
-              | 'sign_extend' size1=nat UNDERSCORE size2=nat #signExtend
-              | BV OPNAME size=nat #bvOp
+directFunction: MEMORY_LOAD_DIRECT #memoryLoad
+              | MEMORY_STORE_DIRECT #memoryStore
+              | GAMMA_LOAD_DIRECT #gammaLoad
+              | GAMMA_STORE_DIRECT #gammaStore
+              | ZERO_EXTEND_DIRECT #zeroExtend
+              | SIGN_EXTEND_DIRECT #signExtend
+              | BVOP_DIRECT #bvOp
               ;
 
-subroutine: 'Subroutine:' id requires* ensures*;
+subroutine: 'Subroutine:' id modifies? requires* ensures*;
+modifies: 'Modifies:' id (COMMA id)*;
 requires: 'Requires:' expr #parsedRequires
         | 'Requires DIRECT:' QUOTESTRING #directRequires
         ;
@@ -41,7 +42,6 @@ arrayAccess: id '[' nat ']';
 id : ID;
 nat: (DIGIT)+ ;
 bv: value=nat BVSIZE;
-endian: LE | BE;
 
 // based upon boogie grammar: https://boogie-docs.readthedocs.io/en/latest/LangRef.html#grammar
 expr : impliesExpr ( EQUIV_OP impliesExpr )* ;
@@ -70,7 +70,25 @@ atomExpr : boolLit #boolLitExpr
 QUOTE : '"';
 QUOTESTRING : QUOTE (~( '"' | '\n' | '\r'))+ QUOTE;
 
-BV: 'bv';
+BVOP_DIRECT: BV OPNAME DIGIT+;
+
+MEMORY_LOAD_DIRECT: MEMORY_LOAD DIGIT+ ENDIAN;
+MEMORY_STORE_DIRECT: MEMORY_STORE DIGIT+ ENDIAN;
+GAMMA_LOAD_DIRECT: GAMMA_LOAD DIGIT+;
+GAMMA_STORE_DIRECT: GAMMA_STORE DIGIT+;
+ZERO_EXTEND_DIRECT: ZERO_EXTEND DIGIT+ UNDERSCORE DIGIT+;
+SIGN_EXTEND_DIRECT: SIGN_EXTEND DIGIT+ UNDERSCORE DIGIT+;
+
+fragment MEMORY_LOAD: 'memory_load';
+fragment MEMORY_STORE: 'memory_store';
+fragment GAMMA_LOAD: 'gamma_load';
+fragment GAMMA_STORE: 'gamma_store';
+fragment ZERO_EXTEND: 'zero_extend';
+fragment SIGN_EXTEND: 'sign_extend';
+
+ENDIAN: LE | BE;
+
+fragment BV: 'bv';
 
 LONG: 'long';
 SHORT: 'short';
@@ -88,7 +106,7 @@ ELSE: 'else';
 DIV_OP : 'div';
 MOD_OP : 'mod';
 
-BVSIZE: BV DIGIT DIGIT?;
+BVSIZE: BV DIGIT+;
 
 ID : NON_DIGIT ( NON_DIGIT | DIGIT )* ;
 NON_DIGIT : ( [A-Z] | [a-z] | '\'' | '~' | '#' | '$' | '^' | '_' | '.' | '?' | '`') ;
@@ -115,13 +133,11 @@ SUB_OP : '-';
 MUL_OP : '*';
 
 COLON: ':';
-UNDERSCORE: '_';
-LE: '_le';
-BE: '_be';
-
-
+fragment UNDERSCORE: '_';
+fragment LE: '_le';
+fragment BE: '_be';
 
-OPNAME : AND
+fragment OPNAME : AND
        | OR
        | ADD
        | MUL
@@ -149,32 +165,32 @@ OPNAME : AND
        | COMP
        ;
 
-AND : 'and';
-OR : 'or';
-ADD : 'add';
-MUL : 'mul';
-UDIV : 'udiv';
-UREM : 'urem';
-SHL : 'shl';
-LSHR : 'lshr';
-ULT : 'ult';
-NAND : 'nand';
-NOR : 'nor';
-XOR : 'xor';
-XNOR : 'xnor';
-SUB : 'sub';
-SREM : 'srem';
-SDIV : 'sdiv';
-SMOD : 'smod';
-ASHR : 'ashr';
-ULE : 'ule';
-UGT : 'ugt';
-UGE : 'uge';
-SLT : 'slt';
-SLE : 'sle';
-SGT : 'sgt';
-SGE : 'sge';
-COMP : 'comp';
+fragment AND : 'and';
+fragment OR : 'or';
+fragment ADD : 'add';
+fragment MUL : 'mul';
+fragment UDIV : 'udiv';
+fragment UREM : 'urem';
+fragment SHL : 'shl';
+fragment LSHR : 'lshr';
+fragment ULT : 'ult';
+fragment NAND : 'nand';
+fragment NOR : 'nor';
+fragment XOR : 'xor';
+fragment XNOR : 'xnor';
+fragment SUB : 'sub';
+fragment SREM : 'srem';
+fragment SDIV : 'sdiv';
+fragment SMOD : 'smod';
+fragment ASHR : 'ashr';
+fragment ULE : 'ule';
+fragment UGT : 'ugt';
+fragment UGE : 'uge';
+fragment SLT : 'slt';
+fragment SLE : 'sle';
+fragment SGT : 'sgt';
+fragment SGE : 'sge';
+fragment COMP : 'comp';
 
 // Ignored
 NEWLINE : '\r'? '\n' -> skip;

src/main/scala/boogie/BProgram.scala

@@ -56,7 +56,8 @@ case class BProcedure(
     body.flatMap(c => c.functionOps).toSet ++ ensures.flatMap(c => c.functionOps).toSet ++ requires
       .flatMap(c => c.functionOps)
       .toSet ++ freeEnsures.flatMap(c => c.functionOps).toSet ++ freeRequires.flatMap(c => c.functionOps).toSet
-  def globals: Set[BVar] = body.flatMap(c => c.globals).toSet
+
+  def globals: Set[BVar] = body.flatMap(c => c.globals).toSet ++ modifies
 }
 
 case class BAxiom(body: BExpr) extends BDeclaration {

src/main/scala/ir/Program.scala

@@ -32,16 +32,20 @@ class Program(
     procedures = procedures.filter(f => reachableNames.contains(f.name))
   }
 
-  def setModifies(): Unit = {
-    //val procToModifies: mutable.Map[Procedure, mutable.Set[Global]] = mutable.Map()
+  def setModifies(specModifies: Map[String, List[String]]): Unit = {
+
     val procToCalls: mutable.Map[Procedure, Set[Procedure]] = mutable.Map()
     for (p <- procedures) {
-      //procToModifies(p) = mutable.Set()
-      //procToModifies(p).addAll(p.blocks.flatMap(_.modifies))
       p.modifies.addAll(p.blocks.flatMap(_.modifies))
       procToCalls(p) = p.calls
     }
 
+    for (p <- procedures) {
+      if (specModifies.contains(p.name)) {
+        p.modifies.addAll(specModifies(p.name).map(nameToGlobal))
+      }
+    }
+
     // very naive implementation but will work for now
     var hasChanged: Boolean = true
     while (hasChanged) {
@@ -58,39 +62,19 @@ class Program(
         }
       }
     }
+  }
 
-    /*
-    val visited: mutable.Set[Procedure] = mutable.Set()
-    val waiting: mutable.Set[Procedure] = mutable.Set()
-    val loops: mutable.Set[Set[Procedure]] = mutable.Set()
-    // need to add support for back edges - do a fixed point on them so all procedures in a loop have the same modifies
-    DFSVisit(mainProcedure, Vector(mainProcedure))
-    def DFSVisit(p: Procedure, path: Vector[Procedure]): Vector[Procedure] = {
-      val children = procToCalls(p)
-      if (visited.contains(p)) {
-        return path
-      }
-      if (waiting.contains(p)) {
-        val loopPath = path.slice(path.indexOf(p), path.size)
-        loops.add(loopPath.toSet)
-        return path
-        //throw new Exception("back edge in intraprocedural control flow graph, not currently supported")
-      }
-      waiting.add(p)
-      p.modifies.addAll(procToModifies(p))
-      for (child <- children) {
-        if (child != p) {
-          DFSVisit(child, path :+ p)
-        }
-      }
-      for (child <- children) {
-        p.modifies.addAll(child.modifies)
+  // this is very crude but the simplest thing for now until we have a more sophisticated specification system that can relate to the IR instead of the Boogie
+  def nameToGlobal(name: String): Global = {
+    if ((name.startsWith("R") || name.startsWith("V")) && (name.length == 2 || name.length == 3) && name.substring(1).forall(_.isDigit)) {
+      if (name.startsWith("R")) {
+        Register(name, BitVecType(64))
+      } else {
+        Register(name, BitVecType(128))
       }
-      waiting.remove(p)
-      visited.add(p)
-      path :+ p
+    } else {
+      Memory(name, 64, 8)
     }
-     */
   }
 
   def stackIdentification(): Unit = {

src/main/scala/ir/Visitor.scala

@@ -307,6 +307,8 @@ class Renamer(reserved: Set[String]) extends Visitor {
 class ExternalRemover(external: Set[String]) extends Visitor {
   override def visitProcedure(node: Procedure): Procedure = {
     if (external.contains(node.name)) {
+      // update the modifies set before removing the body
+      node.modifies.addAll(node.blocks.flatMap(_.modifies))
       node.blocks = ArrayBuffer()
     }
     super.visitProcedure(node)

src/main/scala/specification/Specification.scala

@@ -101,7 +101,8 @@ case class SubroutineSpec(
     requires: List[BExpr],
     requiresDirect: List[String],
     ensures: List[BExpr],
-    ensuresDirect: List[String]
+    ensuresDirect: List[String],
+    modifies: List[String]
 )
 
 case class ExternalFunction(name: String, offset: BigInt)

src/main/scala/translating/SpecificationLoader.scala

@@ -51,35 +51,41 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
   }
 
   def visitDirectFunction(ctx: DirectFunctionContext): FunctionOp = ctx match {
-    case m: MemoryLoadContext  => MemoryLoadOp(64, 8, visitEndian(m.endian), Integer.parseInt(m.size.getText))
-    case m: MemoryStoreContext => MemoryStoreOp(64, 8, visitEndian(m.endian), Integer.parseInt(m.size.getText))
+    case m: MemoryLoadContext =>
+      val suffix = m.getText.stripPrefix("memory_load")
+      val size = suffix.stripSuffix("_le").stripSuffix("_be")
+      val endian = suffix.stripPrefix(size)
+      MemoryLoadOp(64, 8, parseEndian(endian), Integer.parseInt(size))
+    case m: MemoryStoreContext =>
+      val suffix = m.getText.stripPrefix("memory_store")
+      val size = suffix.stripSuffix("_le").stripSuffix("_be")
+      val endian = suffix.stripPrefix(size)
+      MemoryStoreOp(64, 8, parseEndian(endian), Integer.parseInt(size))
     case g: GammaLoadContext =>
-      val size = Integer.parseInt(g.size.getText)
+      val sizeText = g.getText.stripPrefix("gamma_load")
+      val size = Integer.parseInt(sizeText)
       GammaLoadOp(64, size, size / 8)
     case g: GammaStoreContext =>
-      val size = Integer.parseInt(g.size.getText)
+      val sizeText = g.getText.stripPrefix("gamma_store")
+      val size = Integer.parseInt(sizeText)
       GammaStoreOp(64, size, size / 8)
     case z: ZeroExtendContext =>
-      val extension = Integer.parseInt(z.size1.getText)
-      val bodySize = Integer.parseInt(z.size2.getText)
-      BVFunctionOp(
-        s"zero_extend${extension}_$bodySize",
-        s"zero_extend $extension",
-        List(BParam(BitVecBType(bodySize))),
-        BParam(BitVecBType(bodySize + extension))
-      )
+      val suffix = z.getText.stripPrefix("zero_extend")
+      val sizes = suffix.split("_")
+      val extension = Integer.parseInt(sizes(0))
+      val bodySize = Integer.parseInt(sizes(1))
+      BVFunctionOp(s"zero_extend${extension}_$bodySize", s"zero_extend $extension", List(BParam(BitVecBType(bodySize))), BParam(BitVecBType(bodySize + extension)))
     case s: SignExtendContext =>
-      val extension = Integer.parseInt(s.size1.getText)
-      val bodySize = Integer.parseInt(s.size2.getText)
-      BVFunctionOp(
-        s"sign_extend${extension}_$bodySize",
-        s"sign_extend $extension",
-        List(BParam(BitVecBType(bodySize))),
-        BParam(BitVecBType(bodySize + extension))
-      )
+      val suffix = s.getText.stripPrefix("sign_extend")
+      val sizes = suffix.split("_")
+      val extension = Integer.parseInt(sizes(0))
+      val bodySize = Integer.parseInt(sizes(1))
+      BVFunctionOp(s"sign_extend${extension}_$bodySize", s"sign_extend $extension", List(BParam(BitVecBType(bodySize))), BParam(BitVecBType(bodySize + extension)))
     case b: BvOpContext =>
-      val size = Integer.parseInt(b.size.getText)
-      val op = b.OPNAME.getText
+      val body = b.getText.stripPrefix("bv")
+      val sizeText = body.replaceAll("\\D+","")
+      val size = Integer.parseInt(sizeText)
+      val op = body.stripSuffix(sizeText)
       val outType = op match {
         case "and" | "or" | "add" | "mul" | "udiv" | "urem" | "shl" | "lshr" | "nand" | "nor" | "xor" | "xnor" | "sub" |
             "srem" | "sdiv" | "smod" | "ashr" =>
@@ -94,7 +100,7 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
       BVFunctionOp(s"bv$op$size", s"bv$op", List(BParam(BitVecBType(size)), BParam(BitVecBType(size))), BParam(outType))
   }
 
-  def visitEndian(ctx: EndianContext): Endian = ctx.getText match {
+  def parseEndian(endian: String): Endian = endian match {
     case "_le" => Endian.LittleEndian
     case "_be" => Endian.BigEndian
   }
@@ -362,8 +368,13 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
       visitExpr(r.expr, nameToGlobals, params)
     }.toList
 
-    val ensures = ctx.ensures.asScala.collect { case e: ParsedEnsuresContext =>
-      visitExpr(e.expr, nameToGlobals, params)
+    val modifies = Option(ctx.modifies) match {
+      case Some(_) => visitModifies(ctx.modifies)
+      case None => List()
+    }
+
+    val ensures = ctx.ensures.asScala.collect {
+      case e: ParsedEnsuresContext => visitExpr(e.expr, nameToGlobals, params)
     }.toList
 
     val requiresDirect = ctx.requires.asScala.collect { case r: DirectRequiresContext =>
@@ -374,7 +385,11 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
       r.QUOTESTRING.getText.stripPrefix("\"").stripSuffix("\"")
     }.toList
 
-    SubroutineSpec(ctx.id.getText, requires, requiresDirect, ensures, ensuresDirect)
+    SubroutineSpec(ctx.id.getText, requires, requiresDirect, ensures, ensuresDirect, modifies)
+  }
+
+  def visitModifies(ctx: ModifiesContext): List[String] = {
+    ctx.id.asScala.map(_.getText).toList
   }
 
 }

src/main/scala/util/RunUtils.scala

@@ -91,18 +91,23 @@ object RunUtils {
     IRProgram = externalRemover.visitProgram(IRProgram)
     IRProgram = renamer.visitProgram(IRProgram)
 
-    if (performAnalysis) {
-      iterations += 1;
-      IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets)
-    }
-
     if (dumpIL) {
       dump_file(serialiseIL(IRProgram), "before-analysis.il")
     }
 
+
+    if (performAnalysis) {
+      iterations += 1;
+      IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets)
+      if (dumpIL) {
+        dump_file(serialiseIL(IRProgram), "after-analysis.il")
+      }
+    }
     IRProgram.stripUnreachableFunctions()
     IRProgram.stackIdentification()
-    IRProgram.setModifies()
+
+    val specModifies = specification.subroutines.map(s => s.name -> s.modifies).toMap
+    IRProgram.setModifies(specModifies)
 
     Logger.info("[!] Translating to Boogie")
     val boogieTranslator = IRToBoogie(IRProgram, specification)