Make all generated Boogie declarations extern

src/main/scala/boogie/BProgram.scala

@@ -6,6 +6,12 @@ case class BProgram(declarations: List[BDeclaration]) {
 
 trait BDeclaration {
   def toBoogie: List[String] = List(toString)
+  val extern: Boolean
+  val externString: String = if (extern) {
+    " {:extern}"
+  } else {
+    ""
+  }
 }
 
 case class BProcedure(
@@ -19,12 +25,13 @@ case class BProcedure(
     freeEnsures: List[BExpr],
     freeRequires: List[BExpr],
     modifies: Set[BVar],
-    body: List[BCmdOrBlock]
+    body: List[BCmdOrBlock],
+    override val extern: Boolean,
 ) extends BDeclaration
     with Ordered[BProcedure] {
   override def compare(that: BProcedure): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
-    val header = s"procedure $name(${in.map(_.withType).mkString(", ")})"
+    val header = s"procedure$externString $name(${in.map(_.withType).mkString(", ")})"
     val returns = if (out.nonEmpty) {
       s" returns (${out.map(_.withType).mkString(", ")})"
     } else {
@@ -41,7 +48,7 @@ case class BProcedure(
     val freeRequiresStrs = freeRequires.map(r => s"  free requires $r;")
     val freeEnsuresStrs = freeEnsures.map(e => s"  free ensures $e;")
     val locals = body.flatMap(l => l.locals).distinct.sorted
-    val localDefs = locals.map(l => "  " + BVarDecl(l).toString)
+    val localDefs = locals.map(l => "  " + BVarDecl(l, false).toString)
     val bodyStr = if (body.nonEmpty) {
       List("{") ++ localDefs ++ body.flatMap(x => x.toBoogie).map(s => "  " + s) ++ List("}")
     } else {
@@ -61,10 +68,11 @@ case class BProcedure(
 }
 
 case class BAxiom(body: BExpr) extends BDeclaration {
+  override val extern: Boolean = false
   override def toString: String = s"axiom $body;"
 }
 
-case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar, body: Option[BExpr])
+case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar, body: Option[BExpr], override val extern: Boolean)
     extends BDeclaration
     with Ordered[BFunction] {
   override def compare(that: BFunction): Int = name.compare(that.name)
@@ -75,7 +83,7 @@ case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar,
       s" {:bvbuiltin \"$bvbuiltin\"}"
     }
     val inString = in.map(_.withType).mkString(", ")
-    val declString = s"function$bvbuiltinString $name($inString) returns (${out.withType})"
+    val declString = s"function$externString$bvbuiltinString $name($inString) returns (${out.withType})"
     body match {
       case Some(b) => List(declString + " {", "  " + b.toString, "}", "")
       case None    => List(declString + ";")
@@ -88,16 +96,17 @@ case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar,
   }
 }
 
-case class BVarDecl(variable: BVar) extends BDeclaration with Ordered[BVarDecl] {
+case class BVarDecl(variable: BVar, override val extern: Boolean) extends BDeclaration with Ordered[BVarDecl] {
   def compare(that: BVarDecl): Int = variable.compare(that.variable)
   override def toString: String = if (variable.scope == Scope.Const) {
-    s"const $variable: ${variable.getType};"
+    s"const$externString $variable: ${variable.getType};"
   } else {
-    s"var $variable: ${variable.getType};"
+    s"var$externString $variable: ${variable.getType};"
   }
 }
 
 case class BConstAxiomPair(const: BVarDecl, axiom: BAxiom) extends BDeclaration with Ordered[BConstAxiomPair] {
+  override val extern = false
   override def compare(that: BConstAxiomPair): Int = const.compare(that.const)
   override def toString: String = const.toString + "\n" + axiom.toString
 }

src/main/scala/translating/IRToBoogie.scala

@@ -35,12 +35,12 @@ class IRToBoogie(var program: Program, var spec: Specification) {
   def translate: BProgram = {
     val readOnlyMemory = memoryToCondition(program.readOnlyMemory)
     val procedures = program.procedures.map(f => translateProcedure(f, readOnlyMemory))
-    val defaultGlobals = List(BVarDecl(mem), BVarDecl(Gamma_mem))
+    val defaultGlobals = List(BVarDecl(mem, true), BVarDecl(Gamma_mem, true))
     val globalVars = procedures.flatMap(p => p.globals ++ p.freeRequires.flatMap(_.globals) ++ p.freeEnsures.flatMap(_.globals) ++ p.ensures.flatMap(_.globals) ++ p.requires.flatMap(_.globals))
-    val globalDecls = (globalVars.map(b => BVarDecl(b)) ++ defaultGlobals).distinct.sorted.toList
+    val globalDecls = (globalVars.map(b => BVarDecl(b, true)) ++ defaultGlobals).distinct.sorted.toList
 
     val globalConsts: List[BConstAxiomPair] =
-      globals.map(g => BConstAxiomPair(BVarDecl(g.toAddrVar), g.toAxiom)).toList.sorted
+      globals.map(g => BConstAxiomPair(BVarDecl(g.toAddrVar, true), g.toAxiom)).toList.sorted
 
     val guaranteeReflexive = BProcedure(
       "guarantee_reflexive",
@@ -53,7 +53,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       List(),
       List(),
       Set(mem, Gamma_mem),
-      guaranteesReflexive.map(g => BAssert(g))
+      guaranteesReflexive.map(g => BAssert(g)),
+      true
     )
 
     val rgProcs = genRely(relies, readOnlyMemory) :+ guaranteeReflexive
@@ -82,15 +83,15 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     } else {
       reliesUsed
     }
-    val relyProc = BProcedure("rely", List(), List(), relyEnsures, List(), List(), List(), readOnlyMemory, List(), Set(mem, Gamma_mem), List())
-    val relyTransitive = BProcedure("rely_transitive", List(), List(), reliesUsed, List(), List(), List(), List(), List(), Set(mem, Gamma_mem), List(BProcedureCall("rely", List(), List()), BProcedureCall("rely", List(), List())))
-    val relyReflexive = BProcedure("rely_reflexive", List(), List(), List(), List(), List(), List(), List(), List(), Set(), reliesReflexive.map(r => BAssert(r)))
+    val relyProc = BProcedure("rely", List(), List(), relyEnsures, List(), List(), List(), readOnlyMemory, List(), Set(mem, Gamma_mem), List(), true)
+    val relyTransitive = BProcedure("rely_transitive", List(), List(), reliesUsed, List(), List(), List(), List(), List(), Set(mem, Gamma_mem), List(BProcedureCall("rely", List(), List()), BProcedureCall("rely", List(), List())), true)
+    val relyReflexive = BProcedure("rely_reflexive", List(), List(), List(), List(), List(), List(), List(), List(), Set(), reliesReflexive.map(r => BAssert(r)), true)
     List(relyProc, relyTransitive, relyReflexive)
   }
 
   def functionOpToDefinition(f: FunctionOp): BFunction = {
     f match {
-      case b: BVFunctionOp => BFunction(b.name, b.bvbuiltin, b.in, b.out, None)
+      case b: BVFunctionOp => BFunction(b.name, b.bvbuiltin, b.in, b.out, None, true)
       case m: MemoryLoadOp =>
         val memVar = BMapVar("memory", MapBType(BitVecBType(m.addressSize), BitVecBType(m.valueSize)), Scope.Parameter)
         val indexVar = BParam("index", BitVecBType(m.addressSize))
@@ -112,7 +113,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
           BinaryBExpr(BVCONCAT, next, concat)
         }
 
-        BFunction(m.fnName, "", in, out, Some(body))
+        BFunction(m.fnName, "", in, out, Some(body), true)
       case g: GammaLoadOp =>
         val gammaMapVar = BMapVar("gammaMap", MapBType(BitVecBType(g.addressSize), BoolBType), Scope.Parameter)
         val indexVar = BParam("index", BitVecBType(g.addressSize))
@@ -130,7 +131,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
           BinaryBExpr(BoolAND, next, and)
         }
 
-        BFunction(g.fnName, "", in, out, Some(body))
+        BFunction(g.fnName, "", in, out, Some(body), true)
       case m: MemoryStoreOp =>
         val memType = MapBType(BitVecBType(m.addressSize), BitVecBType(m.valueSize))
         val memVar = BMapVar("memory", memType, Scope.Parameter)
@@ -160,7 +161,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
           (update: MapUpdate, next: (BExpr, BExpr)) => MapUpdate(update, next._1, next._2)
         }
 
-        BFunction(m.fnName, "", in, out, Some(body))
+        BFunction(m.fnName, "", in, out, Some(body), true)
       case g: GammaStoreOp =>
         val gammaMapType = MapBType(BitVecBType(g.addressSize), BoolBType)
         val gammaMapVar = BMapVar("gammaMap", gammaMapType, Scope.Parameter)
@@ -187,7 +188,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
           (update: MapUpdate, next: (BExpr, BExpr)) => MapUpdate(update, next._1, next._2)
         }
 
-        BFunction(g.fnName, "", in, out, Some(body))
+        BFunction(g.fnName, "", in, out, Some(body), true)
       case l: LOp =>
         val memoryVar = BParam("memory", l.memoryType)
         val indexVar = BParam("index", l.indexType)
@@ -213,7 +214,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
             IfThenElse(guard, LPred, ite)
           }
         }
-        BFunction("L", "", List(memoryVar, indexVar), BParam(BoolBType), Some(body))
+        BFunction("L", "", List(memoryVar, indexVar), BParam(BoolBType), Some(body), true)
     }
   }
 
@@ -288,7 +289,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       freeEnsures,
       freeRequires,
       modifies.toSet,
-      body.toList
+      body.toList,
+      false
     )
   }
 

src/test/correct/arrays_simple/clang/arrays_simple.expected

@@ -1,38 +1,38 @@
-var Gamma_R0: bool;
-var Gamma_R31: bool;
-var Gamma_R8: bool;
-var Gamma_mem: [bv64]bool;
-var Gamma_stack: [bv64]bool;
-var R0: bv64;
-var R31: bv64;
-var R8: bv64;
-var mem: [bv64]bv8;
-var stack: [bv64]bv8;
-const $_IO_stdin_used_addr: bv64;
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_R31: bool;
+var {:extern} Gamma_R8: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} Gamma_stack: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} R31: bv64;
+var {:extern} R8: bv64;
+var {:extern} mem: [bv64]bv8;
+var {:extern} stack: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
 axiom ($_IO_stdin_used_addr == 1872bv64);
-function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
-function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
   (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
 }
 
-function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+function {:extern} gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
   gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
 }
 
-function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
   (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
 }
 
-function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
   memory[index]
 }
 
-function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
   memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
 }
 
-function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
-procedure rely();
+function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure {:extern} rely();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -73,7 +73,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure rely_transitive()
+procedure {:extern} rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -82,9 +82,9 @@ procedure rely_transitive()
   call rely();
 }
 
-procedure rely_reflexive();
+procedure {:extern} rely_reflexive();
 
-procedure guarantee_reflexive();
+procedure {:extern} guarantee_reflexive();
   modifies Gamma_mem, mem;
 
 procedure main()

src/test/correct/arrays_simple/clang_O2/arrays_simple.expected

@@ -1,14 +1,14 @@
-var Gamma_R0: bool;
-var Gamma_mem: [bv64]bool;
-var R0: bv64;
-var mem: [bv64]bv8;
-const $_IO_stdin_used_addr: bv64;
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} mem: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
 axiom ($_IO_stdin_used_addr == 1840bv64);
-function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
   memory[index]
 }
 
-procedure rely();
+procedure {:extern} rely();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -49,7 +49,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure rely_transitive()
+procedure {:extern} rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -58,9 +58,9 @@ procedure rely_transitive()
   call rely();
 }
 
-procedure rely_reflexive();
+procedure {:extern} rely_reflexive();
 
-procedure guarantee_reflexive();
+procedure {:extern} guarantee_reflexive();
   modifies Gamma_mem, mem;
 
 procedure main()

src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected

@@ -1,38 +1,38 @@
-var Gamma_R0: bool;
-var Gamma_R31: bool;
-var Gamma_R8: bool;
-var Gamma_mem: [bv64]bool;
-var Gamma_stack: [bv64]bool;
-var R0: bv64;
-var R31: bv64;
-var R8: bv64;
-var mem: [bv64]bv8;
-var stack: [bv64]bv8;
-const $_IO_stdin_used_addr: bv64;
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_R31: bool;
+var {:extern} Gamma_R8: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} Gamma_stack: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} R31: bv64;
+var {:extern} R8: bv64;
+var {:extern} mem: [bv64]bv8;
+var {:extern} stack: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
 axiom ($_IO_stdin_used_addr == 1872bv64);
-function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
-function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
   (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
 }
 
-function gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+function {:extern} gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
   gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
 }
 
-function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
   (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
 }
 
-function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
   memory[index]
 }
 
-function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
   memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
 }
 
-function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
-procedure rely();
+function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure {:extern} rely();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -73,7 +73,7 @@ procedure rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure rely_transitive()
+procedure {:extern} rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -82,9 +82,9 @@ procedure rely_transitive()
   call rely();
 }
 
-procedure rely_reflexive();
+procedure {:extern} rely_reflexive();
 
-procedure guarantee_reflexive();
+procedure {:extern} guarantee_reflexive();
   modifies Gamma_mem, mem;
 
 procedure main()