Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Propagate modifies clause through boogie program #115

Merged
merged 5 commits into from
Oct 19, 2023
Merged

Propagate modifies clause through boogie program #115

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ba35d19
propagate modifies clause through boogie program
ailrst Oct 18, 2023
20f4b81
update expected
ailrst Oct 18, 2023
a385218
fix spec file
ailrst Oct 18, 2023
bf23cec
make modifies clauses sorted, use set for improved efficiency here
Oct 18, 2023
c056454
update expected
Oct 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
10 changes: 5 additions & 5 deletions examples/simplified_http_parse_basic/example.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ DIRECT functions: gamma_load64, gamma_load8, memory_load8_le, bvult64, bvule64,


Subroutine: #free
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 0bv64)) == true";
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 1bv64)) == true";
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 2bv64)) == true";
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 3bv64)) == true";
Ensures DIRECT: "Gamma_R0 == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 0bv64)) == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 1bv64)) == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 2bv64)) == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 3bv64)) == true"
Ensures DIRECT: "Gamma_R0 == true"


Subroutine: main
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/boogie/BCmd.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ case class BAssume(body: BExpr, comment: Option[String] = None) extends BCmd {
override def globals: Set[BVar] = body.globals
}

case class ProcedureCall(name: String, lhss: Seq[BVar], params: Seq[BExpr], comment: Option[String] = None) extends BCmd {
case class BProcedureCall(name: String, lhss: Seq[BVar], params: Seq[BExpr], comment: Option[String] = None) extends BCmd {
override def toString: String = {
if (lhss.isEmpty) {
s"call $name();"
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/boogie/BProgram.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ case class BProcedure(
requiresDirect: List[String],
freeEnsures: List[BExpr],
freeRequires: List[BExpr],
modifies: Seq[BVar],
modifies: Set[BVar],
body: List[BCmdOrBlock]
) extends BDeclaration
with Ordered[BProcedure] {
Expand All @@ -32,7 +32,7 @@ case class BProcedure(
}
val semicolon = if body.nonEmpty then "" else ";"
val modifiesStr = if (modifies.nonEmpty) {
List(s" modifies ${modifies.mkString(", ")};")
List(s" modifies ${modifies.toSeq.sorted.mkString(", ")};")
} else {
List()
}
Expand Down
58 changes: 46 additions & 12 deletions src/main/scala/translating/IRToBoogie.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
List(),
List(),
List(),
Seq(mem, Gamma_mem),
Set(mem, Gamma_mem),
guaranteesReflexive.map(g => BAssert(g))
)

Expand All @@ -64,7 +64,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
val functionsUsed3 = functionsUsed2.flatMap(p => p.functionOps).map(p => functionOpToDefinition(p))
val functionsUsed = (functionsUsed2 ++ functionsUsed3).toList.sorted

val declarations = globalDecls ++ globalConsts ++ functionsUsed ++ rgProcs ++ procedures
val declarations = globalDecls ++ globalConsts ++ functionsUsed ++ pushUpModifiesFixedPoint(rgProcs ++ procedures)
BProgram(declarations)
}

Expand All @@ -82,9 +82,9 @@ class IRToBoogie(var program: Program, var spec: Specification) {
} else {
reliesUsed
}
val relyProc = BProcedure("rely", List(), List(), relyEnsures, List(), List(), List(), readOnlyMemory, List(), Seq(mem, Gamma_mem), List())
val relyTransitive = BProcedure("rely_transitive", List(), List(), reliesUsed, List(), List(), List(), List(), List(), Seq(mem, Gamma_mem), List(ProcedureCall("rely", List(), List()), ProcedureCall("rely", List(), List())))
val relyReflexive = BProcedure("rely_reflexive", List(), List(), List(), List(), List(), List(), List(), List(), Seq(), reliesReflexive.map(r => BAssert(r)))
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)))
List(relyProc, relyTransitive, relyReflexive)
}

Expand Down Expand Up @@ -217,14 +217,48 @@ class IRToBoogie(var program: Program, var spec: Specification) {
}
}

def pushUpModifiesFixedPoint(procedures: List[BProcedure]): List[BProcedure] = {
pushUpModifies(procedures) match {
case (true, proc) => pushUpModifiesFixedPoint(proc)
case (false, proc) => proc
}
}

def pushUpModifies(procedures: List[BProcedure]): (Boolean, List[BProcedure]) = {
var changed = false

val procs: List[BProcedure] = procedures.map(
procedure => {
val cmds: List[BCmd] = procedure.body.flatten {
case b: BBlock => b.body
case c: BCmd => Seq(c)
}

val modifies: Set[BVar] = procedure.modifies ++ cmds.collect{ case x: BProcedureCall => procedures.find(_.name == x.name)}
.flatten.flatMap(_.modifies)

if (procedure.modifies != procedure.modifies)
changed = true

procedure.copy(modifies = modifies)
}
)
(changed, procs)
}


def translateProcedure(p: Procedure, readOnlyMemory: List[BExpr]): BProcedure = {
val body = p.blocks.map(b => translateBlock(b))
// TODO don't hardcode Seq(mem, Gamma_mem) but this is necessary to work with adding rely() calls for now
val modifies: Seq[BVar] = {Seq(mem, Gamma_mem) ++ p.modifies

val callsRely: Boolean = body.flatten(_.body).exists(_ match
case BProcedureCall("rely", lhs, params, comment) => true
case _ => false)

val modifies: Seq[BVar] = p.modifies.toSeq
.flatMap {
case m: Memory => Seq(m.toBoogie, m.toGamma)
case r: Register => Seq(r.toBoogie, r.toGamma)
}}.distinct.sorted
}.distinct.sorted

val modifiedPreserve = modifies.collect { case m: BVar if modifiedCheck.contains(m) => m }
val modifiedPreserveEnsures: List[BExpr] = modifiedPreserve.map(m => BinaryBExpr(BoolEQ, m, Old(m))).toList
Expand Down Expand Up @@ -253,7 +287,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
procRequiresDirect,
freeEnsures,
freeRequires,
modifies,
modifies.toSet,
body.toList
)
}
Expand All @@ -278,7 +312,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {

def translate(j: Jump): List[BCmd] = j match {
case d: DirectCall =>
val call = List(ProcedureCall(d.target.name, List(), List()))
val call = List(BProcedureCall(d.target.name, List(), List()))
val returnTarget = d.returnTarget match {
case Some(r) => List(GoToCmd(r.label))
case None => List(Comment("no return target"), BAssume(FalseBLiteral))
Expand Down Expand Up @@ -331,7 +365,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
if (lhs == stack) {
List(store)
} else {
val rely = ProcedureCall("rely", List(), List())
val rely = BProcedureCall("rely", List(), List())
val gammaValueCheck = BAssert(BinaryBExpr(BoolIMPLIES, L(lhs, rhs.index), m.rhs.value.toGamma))
val oldAssigns =
guaranteeOldVars.map(g => AssignCmd(g.toOldVar, BMemoryLoad(lhs, g.toAddrVar, Endian.LittleEndian, g.size)))
Expand Down Expand Up @@ -365,7 +399,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
List(assign)
} else {
val memories = loads.map(m => m.memory).toSeq.sorted
List(ProcedureCall("rely", Seq(), Seq()), assign)
List(BProcedureCall("rely", Seq(), Seq()), assign)
}
case a: Assert =>
val body = a.body.toBoogie
Expand Down
8 changes: 4 additions & 4 deletions src/test/correct/arrays_simple/clang/arrays_simple.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
Expand Down Expand Up @@ -74,7 +74,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
{
Expand All @@ -85,10 +85,10 @@ procedure rely_transitive()
procedure rely_reflexive();

procedure guarantee_reflexive();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;

procedure main()
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_mem, Gamma_stack, R0, R31, R8, mem, stack;
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
Expand Down
8 changes: 4 additions & 4 deletions src/test/correct/arrays_simple/clang_O2/arrays_simple.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
}

procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
Expand Down Expand Up @@ -50,7 +50,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
{
Expand All @@ -61,10 +61,10 @@ procedure rely_transitive()
procedure rely_reflexive();

procedure guarantee_reflexive();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;

procedure main()
modifies Gamma_R0, Gamma_mem, R0, mem;
modifies Gamma_R0, R0;
free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
Expand Down
8 changes: 4 additions & 4 deletions src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
Expand Down Expand Up @@ -74,7 +74,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
{
Expand All @@ -85,10 +85,10 @@ procedure rely_transitive()
procedure rely_reflexive();

procedure guarantee_reflexive();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;

procedure main()
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_mem, Gamma_stack, R0, R31, R8, mem, stack;
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
Expand Down
8 changes: 4 additions & 4 deletions src/test/correct/arrays_simple/clang_pic/arrays_simple.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
Expand Down Expand Up @@ -74,7 +74,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
{
Expand All @@ -85,10 +85,10 @@ procedure rely_transitive()
procedure rely_reflexive();

procedure guarantee_reflexive();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;

procedure main()
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_mem, Gamma_stack, R0, R31, R8, mem, stack;
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
Expand Down
8 changes: 4 additions & 4 deletions src/test/correct/arrays_simple/gcc_O2/arrays_simple.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
}

procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 1896bv64) == 1bv8);
Expand Down Expand Up @@ -50,7 +50,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
{
Expand All @@ -61,10 +61,10 @@ procedure rely_transitive()
procedure rely_reflexive();

procedure guarantee_reflexive();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;

procedure main()
modifies Gamma_R0, Gamma_mem, R0, mem;
modifies Gamma_R0, R0;
free requires (memory_load8_le(mem, 69632bv64) == 0bv8);
free requires (memory_load8_le(mem, 69633bv64) == 0bv8);
free requires (memory_load8_le(mem, 69634bv64) == 0bv8);
Expand Down
6 changes: 3 additions & 3 deletions src/test/correct/basic_arrays_read/clang/basic_arrays_read.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
free ensures (memory_load8_le(mem, 1860bv64) == 1bv8);
Expand Down Expand Up @@ -78,7 +78,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
{
call rely();
Expand All @@ -91,7 +91,7 @@ procedure rely_reflexive()
}

procedure guarantee_reflexive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
{
assert true;
}
Expand Down
6 changes: 3 additions & 3 deletions src/test/correct/basic_arrays_read/clang_O2/basic_arrays_read.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
}

procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
free ensures (memory_load8_le(mem, 1848bv64) == 1bv8);
Expand Down Expand Up @@ -69,7 +69,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
{
call rely();
Expand All @@ -82,7 +82,7 @@ procedure rely_reflexive()
}

procedure guarantee_reflexive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
{
assert true;
}
Expand Down
6 changes: 3 additions & 3 deletions src/test/correct/basic_arrays_read/clang_no_plt_no_pic/basic_arrays_read.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
free ensures (memory_load8_le(mem, 1860bv64) == 1bv8);
Expand Down Expand Up @@ -78,7 +78,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
ensures (old(memory_load32_le(mem, bvadd64($arr_addr, 0bv64))) == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
{
call rely();
Expand All @@ -91,7 +91,7 @@ procedure rely_reflexive()
}

procedure guarantee_reflexive()
modifies mem, Gamma_mem;
modifies Gamma_mem, mem;
{
assert true;
}
Expand Down
Loading