From 68aed948f2771f5d50cca134f84ac947fa7c653e Mon Sep 17 00:00:00 2001 From: l-kent Date: Mon, 9 Oct 2023 10:36:18 +1000 Subject: [PATCH 1/2] allows user to manually specify modifies section by adding 'Modifies: R0' etc. to subroutine specifications --- src/main/antlr4/Specifications.g4 | 3 +- src/main/scala/boogie/BProgram.scala | 2 +- src/main/scala/ir/Program.scala | 55 ++++++------------- src/main/scala/ir/Visitor.scala | 2 + .../scala/specification/Specification.scala | 2 +- .../translating/SpecificationLoader.scala | 11 +++- src/main/scala/util/RunUtils.scala | 6 +- 7 files changed, 37 insertions(+), 44 deletions(-) diff --git a/src/main/antlr4/Specifications.g4 b/src/main/antlr4/Specifications.g4 index 2b7b0ce4d..f33f53584 100644 --- a/src/main/antlr4/Specifications.g4 +++ b/src/main/antlr4/Specifications.g4 @@ -27,7 +27,8 @@ directFunction: 'memory_load' size=nat endian #memoryLoad | BV OPNAME size=nat #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 ; diff --git a/src/main/scala/boogie/BProgram.scala b/src/main/scala/boogie/BProgram.scala index 65d0fb2fa..f2b64f8ad 100644 --- a/src/main/scala/boogie/BProgram.scala +++ b/src/main/scala/boogie/BProgram.scala @@ -38,7 +38,7 @@ case class BProcedure(name: String, in: List[BVar], out: List[BVar], ensures: Li } override def toString: String = toBoogie.mkString("\n") def functionOps: Set[FunctionOp] = 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 4aeff086a..9da33d0ba 100644 --- a/src/main/scala/ir/Program.scala +++ b/src/main/scala/ir/Program.scala @@ -27,16 +27,20 @@ class Program(var procedures: ArrayBuffer[Procedure], var initialMemory: ArrayBu 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) { @@ -53,42 +57,19 @@ class Program(var procedures: ArrayBuffer[Procedure], var initialMemory: ArrayBu } } } + } - - - - /* - 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 bf9f912f6..c903663dd 100644 --- a/src/main/scala/ir/Visitor.scala +++ b/src/main/scala/ir/Visitor.scala @@ -303,6 +303,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 58a5bf756..72a617122 100644 --- a/src/main/scala/specification/Specification.scala +++ b/src/main/scala/specification/Specification.scala @@ -63,6 +63,6 @@ case class Specification(globals: Set[SpecGlobal], LPreds: Map[SpecGlobal, BExpr val controlled: Set[SpecGlobal] = controls.values.flatten.toSet } -case class SubroutineSpec(name: String, requires: List[BExpr], requiresDirect: List[String], ensures: List[BExpr], ensuresDirect: List[String]) +case class SubroutineSpec(name: String, requires: List[BExpr], requiresDirect: List[String], ensures: List[BExpr], 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 71d7a7258..ee46d4280 100644 --- a/src/main/scala/translating/SpecificationLoader.scala +++ b/src/main/scala/translating/SpecificationLoader.scala @@ -280,6 +280,11 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) { case r: ParsedRequiresContext => visitExpr(r.expr, nameToGlobals, params) }.toList + 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 @@ -292,7 +297,11 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) { case r: DirectEnsuresContext => 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 20c557a02..84fb653b7 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -85,11 +85,11 @@ object RunUtils { } } - - IRProgram.stripUnreachableFunctions() IRProgram.stackIdentification() - IRProgram.setModifies() + + val specModifies = specification.subroutines.map(s => s.name -> s.modifies).toMap + IRProgram.setModifies(specModifies) val boogieTranslator = IRToBoogie(IRProgram, specification) boogieTranslator.translate From c2a6e8ce9d437b6af4e117ec0d62a62fb77a11db Mon Sep 17 00:00:00 2001 From: l-kent Date: Mon, 9 Oct 2023 11:32:10 +1000 Subject: [PATCH 2/2] fix direct functions parsing issue --- src/main/antlr4/Specifications.g4 | 99 +++++++++++-------- .../translating/SpecificationLoader.scala | 38 ++++--- 2 files changed, 84 insertions(+), 53 deletions(-) diff --git a/src/main/antlr4/Specifications.g4 b/src/main/antlr4/Specifications.g4 index f33f53584..c476ebdb2 100644 --- a/src/main/antlr4/Specifications.g4 +++ b/src/main/antlr4/Specifications.g4 @@ -18,13 +18,13 @@ 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 modifies? requires* ensures*; @@ -42,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 )* ; @@ -71,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'; @@ -89,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] | '\'' | '~' | '#' | '$' | '^' | '_' | '.' | '?' | '`') ; @@ -116,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 @@ -150,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/translating/SpecificationLoader.scala b/src/main/scala/translating/SpecificationLoader.scala index ee46d4280..d19edb8f9 100644 --- a/src/main/scala/translating/SpecificationLoader.scala +++ b/src/main/scala/translating/SpecificationLoader.scala @@ -51,25 +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) + 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) + 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" => BitVecBType(size) @@ -83,7 +99,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 }