diff --git a/src/main/antlr4/Specifications.g4 b/src/main/antlr4/Specifications.g4 index 2b7b0ce4d..c476ebdb2 100644 --- a/src/main/antlr4/Specifications.g4 +++ b/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; diff --git a/src/main/scala/boogie/BProgram.scala b/src/main/scala/boogie/BProgram.scala index aeeee2bf7..bdee70e32 100644 --- a/src/main/scala/boogie/BProgram.scala +++ b/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 { diff --git a/src/main/scala/ir/Program.scala b/src/main/scala/ir/Program.scala index 4985188d3..6eb1d3713 100644 --- a/src/main/scala/ir/Program.scala +++ b/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 = { diff --git a/src/main/scala/ir/Visitor.scala b/src/main/scala/ir/Visitor.scala index f2e7133e0..8f330d6b5 100644 --- a/src/main/scala/ir/Visitor.scala +++ b/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) diff --git a/src/main/scala/specification/Specification.scala b/src/main/scala/specification/Specification.scala index 580dafbe6..3c3ffd7ff 100644 --- a/src/main/scala/specification/Specification.scala +++ b/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) diff --git a/src/main/scala/translating/SpecificationLoader.scala b/src/main/scala/translating/SpecificationLoader.scala index a41e82f62..9fe6d26cc 100644 --- a/src/main/scala/translating/SpecificationLoader.scala +++ b/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 } } diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 9faf3a533..5177703f9 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/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)