Skip to content

Commit

Permalink
Merge pull request #102 from UQ-PAC/stackidentificationissue
Browse files Browse the repository at this point in the history 
Stack Identification Bug Fix
  • Loading branch information
@ailrst
ailrst authored Oct 13, 2023
2 parents ada2dd4 + adc916c commit 96b6d13
Show file tree
Hide file tree
Showing 93 changed files with 635 additions and 947 deletions.
8 changes: 6 additions & 2 deletions src/main/scala/ir/Program.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,10 @@ class Procedure(
}

// update stack references
val rhsStackRefs = l.rhs.variables.intersect(stackRefs)
val variableVisitor = VariablesWithoutStoresLoads()
variableVisitor.visitExpr(l.rhs)

val rhsStackRefs = variableVisitor.variables.toSet.intersect(stackRefs)
if (rhsStackRefs.nonEmpty) {
stackRefs.add(l.lhs)
} else if (stackRefs.contains(l.lhs) && l.lhs != stackPointer) {
Expand All @@ -144,7 +147,8 @@ class Procedure(
for (j <- b.jumps) {
j match {
case g: GoTo => visitBlock(g.target)
case _ =>
case d: DirectCall => d.returnTarget.foreach(visitBlock)
case i: IndirectCall => i.returnTarget.foreach(visitBlock)
}
}
}
Expand Down
24 changes: 24 additions & 0 deletions src/main/scala/ir/Visitor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -314,3 +314,27 @@ class ExternalRemover(external: Set[String]) extends Visitor {
super.visitProcedure(node)
}
}

/** Gives variables that are not contained within a MemoryStore or MemoryLoad
* */
class VariablesWithoutStoresLoads extends ReadOnlyVisitor {
val variables: mutable.Set[Variable] = mutable.Set()

override def visitRegister(node: Register): Register = {
variables.add(node)
node
}
override def visitLocalVar(node: LocalVar): LocalVar = {
variables.add(node)
node
}

override def visitMemoryStore(node: MemoryStore): MemoryStore = {
node
}

override def visitMemoryLoad(node: MemoryLoad): MemoryLoad = {
node
}

}
6 changes: 3 additions & 3 deletions src/test/correct/basic_function_call_caller/clang/basic_function_call_caller.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ procedure main()
assert ((bvadd64(R8, 52bv64) == $x_addr) ==> (L(mem, $y_addr) ==> Gamma_y_old));
assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R8, Gamma_R8 := zero_extend32_32(memory_load32_le(mem, bvadd64(R29, 18446744073709551612bv64))), (gamma_load32(Gamma_mem, bvadd64(R29, 18446744073709551612bv64)) || L(mem, bvadd64(R29, 18446744073709551612bv64)));
R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R29, 18446744073709551612bv64))), gamma_load32(Gamma_stack, bvadd64(R29, 18446744073709551612bv64));
R9, Gamma_R9 := 69632bv64, true;
call rely();
assert (L(mem, bvadd64(R9, 56bv64)) ==> Gamma_R8);
Expand All @@ -202,8 +202,8 @@ procedure main()
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R0, Gamma_R0 := 0bv64, true;
#5, Gamma_#5 := bvadd64(R31, 16bv64), Gamma_R31;
R29, Gamma_R29 := memory_load64_le(mem, #5), (gamma_load64(Gamma_mem, #5) || L(mem, #5));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(#5, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(#5, 8bv64)) || L(mem, bvadd64(#5, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, #5), gamma_load64(Gamma_stack, #5);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(#5, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#5, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
6 changes: 3 additions & 3 deletions ...orrect/basic_function_call_caller/clang_no_plt_no_pic/basic_function_call_caller.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ procedure main()
assert ((bvadd64(R8, 52bv64) == $x_addr) ==> (L(mem, $y_addr) ==> Gamma_y_old));
assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R8, Gamma_R8 := zero_extend32_32(memory_load32_le(mem, bvadd64(R29, 18446744073709551612bv64))), (gamma_load32(Gamma_mem, bvadd64(R29, 18446744073709551612bv64)) || L(mem, bvadd64(R29, 18446744073709551612bv64)));
R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R29, 18446744073709551612bv64))), gamma_load32(Gamma_stack, bvadd64(R29, 18446744073709551612bv64));
R9, Gamma_R9 := 69632bv64, true;
call rely();
assert (L(mem, bvadd64(R9, 56bv64)) ==> Gamma_R8);
Expand All @@ -202,8 +202,8 @@ procedure main()
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R0, Gamma_R0 := 0bv64, true;
#5, Gamma_#5 := bvadd64(R31, 16bv64), Gamma_R31;
R29, Gamma_R29 := memory_load64_le(mem, #5), (gamma_load64(Gamma_mem, #5) || L(mem, #5));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(#5, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(#5, 8bv64)) || L(mem, bvadd64(#5, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, #5), gamma_load64(Gamma_stack, #5);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(#5, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#5, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
6 changes: 3 additions & 3 deletions src/test/correct/basic_function_call_caller/gcc/basic_function_call_caller.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ procedure main()
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R0, Gamma_R0 := 69632bv64, true;
R0, Gamma_R0 := bvadd64(R0, 24bv64), Gamma_R0;
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(mem, bvadd64(R31, 28bv64))), (gamma_load32(Gamma_mem, bvadd64(R31, 28bv64)) || L(mem, bvadd64(R31, 28bv64)));
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 28bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 28bv64));
call rely();
assert (L(mem, R0) ==> Gamma_R1);
x_old := memory_load32_le(mem, $x_addr);
Expand All @@ -256,8 +256,8 @@ procedure main()
assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R0, Gamma_R0 := 0bv64, true;
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
6 changes: 3 additions & 3 deletions .../correct/basic_function_call_caller/gcc_no_plt_no_pic/basic_function_call_caller.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ procedure main()
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R0, Gamma_R0 := 69632bv64, true;
R0, Gamma_R0 := bvadd64(R0, 24bv64), Gamma_R0;
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(mem, bvadd64(R31, 28bv64))), (gamma_load32(Gamma_mem, bvadd64(R31, 28bv64)) || L(mem, bvadd64(R31, 28bv64)));
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 28bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 28bv64));
call rely();
assert (L(mem, R0) ==> Gamma_R1);
x_old := memory_load32_le(mem, $x_addr);
Expand All @@ -256,8 +256,8 @@ procedure main()
assert ((x_old == 0bv32) ==> (memory_load32_le(mem, $x_addr) == 0bv32));
assert (Gamma_y_old ==> ((memory_load32_le(mem, $x_addr) == 0bv32) || gamma_load32(Gamma_mem, $y_addr)));
R0, Gamma_R0 := 0bv64, true;
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
12 changes: 5 additions & 7 deletions src/test/correct/basicfree/clang/basicfree.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,22 +161,20 @@ procedure main()
call malloc();
goto l0000030d;
l0000030d:
call rely();
assert (L(mem, bvadd64(R31, 8bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store64_le(mem, bvadd64(R31, 8bv64), R0), gamma_store64(Gamma_mem, bvadd64(R31, 8bv64), Gamma_R0);
R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 8bv64), R0), gamma_store64(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R0);
R9, Gamma_R9 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R8, Gamma_R8 := 1bv64, true;
call rely();
assert (L(mem, R9) ==> Gamma_R8);
mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R30, Gamma_R30 := 2048bv64, true;
call #free();
goto l00000338;
l00000338:
#5, Gamma_#5 := bvadd64(R31, 16bv64), Gamma_R31;
R29, Gamma_R29 := memory_load64_le(mem, #5), (gamma_load64(Gamma_mem, #5) || L(mem, #5));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(#5, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(#5, 8bv64)) || L(mem, bvadd64(#5, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, #5), gamma_load64(Gamma_stack, #5);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(#5, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#5, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
12 changes: 5 additions & 7 deletions src/test/correct/basicfree/clang_no_plt_no_pic/basicfree.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,22 +161,20 @@ procedure main()
call malloc();
goto l000008ed;
l000008ed:
call rely();
assert (L(mem, bvadd64(R31, 8bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store64_le(mem, bvadd64(R31, 8bv64), R0), gamma_store64(Gamma_mem, bvadd64(R31, 8bv64), Gamma_R0);
R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 8bv64), R0), gamma_store64(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R0);
R9, Gamma_R9 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R8, Gamma_R8 := 1bv64, true;
call rely();
assert (L(mem, R9) ==> Gamma_R8);
mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R30, Gamma_R30 := 2048bv64, true;
call #free();
goto l00000918;
l00000918:
#5, Gamma_#5 := bvadd64(R31, 16bv64), Gamma_R31;
R29, Gamma_R29 := memory_load64_le(mem, #5), (gamma_load64(Gamma_mem, #5) || L(mem, #5));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(#5, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(#5, 8bv64)) || L(mem, bvadd64(#5, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, #5), gamma_load64(Gamma_stack, #5);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(#5, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#5, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
12 changes: 5 additions & 7 deletions src/test/correct/basicfree/clang_pic/basicfree.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,22 +161,20 @@ procedure main()
call malloc();
goto l000008ed;
l000008ed:
call rely();
assert (L(mem, bvadd64(R31, 8bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store64_le(mem, bvadd64(R31, 8bv64), R0), gamma_store64(Gamma_mem, bvadd64(R31, 8bv64), Gamma_R0);
R9, Gamma_R9 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 8bv64), R0), gamma_store64(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R0);
R9, Gamma_R9 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R8, Gamma_R8 := 1bv64, true;
call rely();
assert (L(mem, R9) ==> Gamma_R8);
mem, Gamma_mem := memory_store32_le(mem, R9, R8[32:0]), gamma_store32(Gamma_mem, R9, Gamma_R8);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R30, Gamma_R30 := 2048bv64, true;
call #free();
goto l00000918;
l00000918:
#5, Gamma_#5 := bvadd64(R31, 16bv64), Gamma_R31;
R29, Gamma_R29 := memory_load64_le(mem, #5), (gamma_load64(Gamma_mem, #5) || L(mem, #5));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(#5, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(#5, 8bv64)) || L(mem, bvadd64(#5, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, #5), gamma_load64(Gamma_stack, #5);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(#5, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#5, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
12 changes: 5 additions & 7 deletions src/test/correct/basicfree/gcc/basicfree.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,21 +229,19 @@ procedure main()
call malloc();
goto l00000307;
l00000307:
call rely();
assert (L(mem, bvadd64(R31, 24bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store64_le(mem, bvadd64(R31, 24bv64), R0), gamma_store64(Gamma_mem, bvadd64(R31, 24bv64), Gamma_R0);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 24bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 24bv64)) || L(mem, bvadd64(R31, 24bv64)));
stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 24bv64), R0), gamma_store64(Gamma_stack, bvadd64(R31, 24bv64), Gamma_R0);
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64));
R1, Gamma_R1 := 1bv64, true;
call rely();
assert (L(mem, R0) ==> Gamma_R1);
mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 24bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 24bv64)) || L(mem, bvadd64(R31, 24bv64)));
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64));
R30, Gamma_R30 := 2044bv64, true;
call #free();
goto l00000332;
l00000332:
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
12 changes: 5 additions & 7 deletions src/test/correct/basicfree/gcc_no_plt_no_pic/basicfree.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,21 +229,19 @@ procedure main()
call malloc();
goto l000008dc;
l000008dc:
call rely();
assert (L(mem, bvadd64(R31, 24bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store64_le(mem, bvadd64(R31, 24bv64), R0), gamma_store64(Gamma_mem, bvadd64(R31, 24bv64), Gamma_R0);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 24bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 24bv64)) || L(mem, bvadd64(R31, 24bv64)));
stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 24bv64), R0), gamma_store64(Gamma_stack, bvadd64(R31, 24bv64), Gamma_R0);
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64));
R1, Gamma_R1 := 1bv64, true;
call rely();
assert (L(mem, R0) ==> Gamma_R1);
mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 24bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 24bv64)) || L(mem, bvadd64(R31, 24bv64)));
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64));
R30, Gamma_R30 := 2044bv64, true;
call #free();
goto l00000907;
l00000907:
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
12 changes: 5 additions & 7 deletions src/test/correct/basicfree/gcc_pic/basicfree.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,21 +229,19 @@ procedure main()
call malloc();
goto l000008dc;
l000008dc:
call rely();
assert (L(mem, bvadd64(R31, 24bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store64_le(mem, bvadd64(R31, 24bv64), R0), gamma_store64(Gamma_mem, bvadd64(R31, 24bv64), Gamma_R0);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 24bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 24bv64)) || L(mem, bvadd64(R31, 24bv64)));
stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 24bv64), R0), gamma_store64(Gamma_stack, bvadd64(R31, 24bv64), Gamma_R0);
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64));
R1, Gamma_R1 := 1bv64, true;
call rely();
assert (L(mem, R0) ==> Gamma_R1);
mem, Gamma_mem := memory_store32_le(mem, R0, R1[32:0]), gamma_store32(Gamma_mem, R0, Gamma_R1);
R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R31, 24bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 24bv64)) || L(mem, bvadd64(R31, 24bv64)));
R0, Gamma_R0 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64));
R30, Gamma_R30 := 2044bv64, true;
call #free();
goto l00000907;
l00000907:
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
return;
}
Expand Down
4 changes: 2 additions & 2 deletions src/test/correct/function/clang/function.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,8 @@ procedure main()
assert (L(mem, bvadd64(R8, 56bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 56bv64), R0[32:0]), gamma_store32(Gamma_mem, bvadd64(R8, 56bv64), Gamma_R0);
R0, Gamma_R0 := 0bv64, true;
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
return;
}
4 changes: 2 additions & 2 deletions src/test/correct/function/clang_no_plt_no_pic/function.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,8 @@ procedure main()
assert (L(mem, bvadd64(R8, 56bv64)) ==> Gamma_R0);
mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 56bv64), R0[32:0]), gamma_store32(Gamma_mem, bvadd64(R8, 56bv64), Gamma_R0);
R0, Gamma_R0 := 0bv64, true;
R29, Gamma_R29 := memory_load64_le(mem, R31), (gamma_load64(Gamma_mem, R31) || L(mem, R31));
R30, Gamma_R30 := memory_load64_le(mem, bvadd64(R31, 8bv64)), (gamma_load64(Gamma_mem, bvadd64(R31, 8bv64)) || L(mem, bvadd64(R31, 8bv64)));
R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
return;
}
Loading

0 comments on commit 96b6d13

Please sign in to comment.