Skip to content

Commit

Permalink
fix: invertibility condition for SLTU (when t != 0)
Browse files Browse the repository at this point in the history 
This fixes the bogus assumption that `t != BitVector(1)` implies that
`t == BitVector(0)`, which does not hold in our engine since the target
value `t` can be any arbitrary 64-bit vector. Determining whether such
target values make sense in general is outside the scope of this change.
  • Loading branch information
@mstarzinger
mstarzinger committed Apr 26, 2021
1 parent c24270a commit 6947f52
Show file tree
Hide file tree
Showing 3 changed files with 64 additions and 36 deletions.
21 changes: 21 additions & 0 deletions examples/test-sltu-2.c
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
uint64_t main() {
uint64_t a;
uint64_t* x;

x = malloc(8);

*x = 0;

read(0, x, 1);

a = *x - 42;

if (a < 0)
return 0;
if (a > 18446744073709551615)
return 0;
if (a == 18446744073709551615)
return 1;

return 0;
}
75 changes: 40 additions & 35 deletions src/solver/monster.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,21 +66,22 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) ->
}
}
},
BVOperator::Sltu => {
// (x<s) = t
if d == OperandSide::Lhs {
if t == BitVector(1) {
BVOperator::Sltu => match d {
OperandSide::Lhs => {
if t != BitVector(0) {
!(s == BitVector(0))
} else {
true
}
// (s<x) = t
} else if t == BitVector(1) {
!(s == BitVector::ones())
} else {
true
}
}
OperandSide::Rhs => {
if t != BitVector(0) {
!(s == BitVector::ones())
} else {
true
}
}
},
BVOperator::Remu => match d {
OperandSide::Lhs => !(s <= t),
OperandSide::Rhs => {
Expand All @@ -93,7 +94,7 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) ->
}
}

// initialize bit vectors with a consistent intial assignment to the formula
// initialize bit vectors with a consistent initial assignment to the formula
// inputs are initialized with random values
fn initialize_ab<F: Formula>(formula: &F) -> Vec<BitVector> {
// Initialize values for all input/const nodes
Expand Down Expand Up @@ -197,27 +198,28 @@ fn compute_inverse_value(op: BVOperator, s: BitVector, t: BitVector, d: OperandS

result | arbitrary_bits
}
BVOperator::Sltu => {
if d == OperandSide::Lhs {
BVOperator::Sltu => match d {
OperandSide::Lhs => {
if t == BitVector(0) {
// x<s == false
// therefore we need a random x>=s
// x<s == false; therefore we need a random x>=s
BitVector(thread_rng().sample(Uniform::new_inclusive(s.0, BitVector::ones().0)))
} else {
// x<s == true
// therefore we need a random x<s
// x<s == true; therefore we need a random x<s
BitVector(thread_rng().sample(Uniform::new(0, s.0)))
}
} else if t == BitVector(0) {
// s<x == false
// therefore we need a random x<=s
BitVector(thread_rng().sample(Uniform::new_inclusive(0, s.0)))
} else {
// s<x == true
// therefore we need a random x>s
BitVector(thread_rng().sample(Uniform::new_inclusive(s.0 + 1, BitVector::ones().0)))
}
}
OperandSide::Rhs => {
if t == BitVector(0) {
// s<x == false; therefore we need a random x<=s
BitVector(thread_rng().sample(Uniform::new_inclusive(0, s.0)))
} else {
// s<x == true; therefore we need a random x>s
BitVector(
thread_rng().sample(Uniform::new_inclusive(s.0 + 1, BitVector::ones().0)),
)
}
}
},
BVOperator::Divu => match d {
OperandSide::Lhs => {
if (t == BitVector::ones()) && (s == BitVector(1)) {
Expand Down Expand Up @@ -346,23 +348,26 @@ fn compute_consistent_value(op: BVOperator, t: BitVector, d: OperandSide) -> Bit
}
}
},
BVOperator::Sltu => {
if d == OperandSide::Lhs {
BVOperator::Sltu => match d {
OperandSide::Lhs => {
if t == BitVector(0) {
// x<s == false
BitVector(thread_rng().sample(Uniform::new_inclusive(0, BitVector::ones().0)))
} else {
// x<s == true
BitVector(thread_rng().sample(Uniform::new(0, BitVector::ones().0)))
}
} else if t == BitVector(0) {
// s<x == false
BitVector(thread_rng().sample(Uniform::new_inclusive(0, BitVector::ones().0)))
} else {
// s<x == true
BitVector(thread_rng().sample(Uniform::new(1, BitVector::ones().0)))
}
}
OperandSide::Rhs => {
if t == BitVector(0) {
// s<x == false
BitVector(thread_rng().sample(Uniform::new_inclusive(0, BitVector::ones().0)))
} else {
// s<x == true
BitVector(thread_rng().sample(Uniform::new(1, BitVector::ones().0)))
}
}
},
BVOperator::Remu => match d {
OperandSide::Lhs => {
if t == BitVector::ones() {
Expand Down
4 changes: 3 additions & 1 deletion tests/engine.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use std::{
};
use utils::{compile_riscu, init, with_temp_dir};

const TEST_FILES: [&str; 20] = [
const TEST_FILES: [&str; 21] = [
"arithmetic.c",
"echo-line.c",
"if-else.c", // needs timeout
Expand All @@ -22,6 +22,7 @@ const TEST_FILES: [&str; 20] = [
"simple-assignment-1-35.c",
"test-remu.c",
"test-sltu.c",
"test-sltu-2.c",
//"memory-access-1-35.c",
"memory-invalid-read.c",
"memory-invalid-write.c",
Expand Down Expand Up @@ -184,6 +185,7 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
("simple-assignment-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("test-remu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("test-sltu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("test-sltu-2.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
//("memory-access-1-35.c", Bug::
("memory-invalid-read.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) |
("memory-invalid-write.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) |
Expand Down

0 comments on commit 6947f52

Please sign in to comment.