diff --git a/regression-tests/runalldirs b/regression-tests/runalldirs index 0e8b91f..605cb18 100755 --- a/regression-tests/runalldirs +++ b/regression-tests/runalldirs @@ -25,6 +25,7 @@ run_test ./rundir math-arrays "" -assert -dev -t:60 run_test ./rundir quantifiers "" -assert -dev -t:60 run_test ./rundir interpreted-predicates "" -assert -dev -t:60 run_test ./rundir properties "" -assert -dev -t:60 +run_test ./rundir toh-contract-translation "" -dev -t:60 #run_test ./rundir ParametricEncoder "" if [ $ERRORS -ne 0 ]; then diff --git a/regression-tests/toh-contract-translation/Answers b/regression-tests/toh-contract-translation/Answers new file mode 100644 index 0000000..f0ade9c --- /dev/null +++ b/regression-tests/toh-contract-translation/Answers @@ -0,0 +1,153 @@ + +get-1.c +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int_ptr" available + +Inferred ACSL annotations +================================================================================ +/* contracts for get */ +/*@ + requires p == n && n_init >= 1; + ensures ((\result == 0 && 0 >= \old(*n)) || \result >= 0) && r1 == \old(r1) && n_init == \old(n_init) && \old(n) == n; +*/ +================================================================================ + +SAFE + +incdec-1.c +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int_ptr" available + +Inferred ACSL annotations +================================================================================ +/* contracts for decrement */ +/*@ + requires \separated(a, b) && \valid(a) && \valid(b); + ensures a_init == \old(a_init) && b_init == \old(b_init) && a == \old(a) && b == \old(b) && \separated(a, b) && \valid(a) && \valid(b); +*/ +/* contracts for increment */ +/*@ + requires val == a && \separated(val, b) && \valid(val) && \valid(b); + ensures \old(val) == a && a_init == \old(a_init) && b_init == \old(b_init) && \old(val) == \old(a) && b == \old(b) && \separated(val, b) && \valid(val) && \valid(b) && *val == 1 + \old(*val); +*/ +================================================================================ + +SAFE + +incdec-2.c +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int_ptr" available + +Inferred ACSL annotations +================================================================================ +/* contracts for decrement */ +/*@ + requires \valid(a); + ensures a_init == \old(a_init) && a == \old(a) && \valid(a); +*/ +/* contracts for increment */ +/*@ + requires val == a && \valid(val); + ensures \old(val) == a && a_init == \old(a_init) && \valid(val) && *val == 1 + \old(*val); +*/ +================================================================================ + +SAFE + +max-1.c +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int" available + +Inferred ACSL annotations +================================================================================ +/* contracts for findMax */ +/*@ + requires x == a && y == b && \separated(x, y) && \valid(x) && \valid(y); + ensures ((a_init == \result && \result >= b_init) || (b_init - a_init >= 1 && b_init == \result)) && r == \old(r) && a_init == \old(a_init) && b_init == \old(b_init) && \old(a) == a && \old(b) == b; +*/ +================================================================================ + +SAFE + +max-2.c +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int" available + +Inferred ACSL annotations +================================================================================ +/* contracts for findMax */ +/*@ + requires max == r && x == a && y == b && \separated(x, y) && \separated(x, max) && \separated(y, max) && \valid(x) && \valid(y) && \valid(max); + ensures (\old(b_init) - \old(a_init) >= 1 || \old(a_init) >= \old(b_init)) && a == \old(x) && b == \old(y) && r == \old(max) && \old(a_init) == a_init && \old(b_init) == b_init; +*/ +================================================================================ + +SAFE + +multadd-1.c +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int_ptr" available +Warning: no definition of function "non_det_int" available +Warning: no definition of function "non_det_int" available +Warning: The following clause has different terms with the same name (term: b:12) +main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post). + +Warning: The following clause has different terms with the same name (term: result:13) +main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post). + +Warning: The following clause has different terms with the same name (term: a:11) +main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post). + +Warning: The following clause has different terms with the same name (term: b:12) +addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13). + +Warning: The following clause has different terms with the same name (term: result:13) +addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13). + +Warning: The following clause has different terms with the same name (term: a:11) +addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13). + + +Inferred ACSL annotations +================================================================================ +/* contracts for addTwoNumbers */ +/*@ + requires \separated(a, b) && \separated(a, result) && \separated(b, result) && \valid(a) && \valid(b) && \valid(result); + ensures a == \old(a) && b == \old(b) && result == \old(result) && a_init == \old(a_init) && b_init == \old(b_init) && \separated(a, b) && \separated(a, result) && \separated(b, result) && \valid(a) && \valid(b) && \valid(result); +*/ +/* contracts for multiplyByTwo */ +/*@ + requires num == a && \separated(num, b) && \separated(num, result) && \separated(b, result) && \valid(num) && \valid(b) && \valid(result); + ensures \old(num) == a && \old(num) == \old(a) && b == \old(b) && result == \old(result) && a_init == \old(a_init) && b_init == \old(b_init) && \separated(num, b) && \separated(num, result) && \separated(b, result) && \valid(num) && \valid(b) && \valid(result) && *num == 2*\old(*num); +*/ +================================================================================ + +SAFE + +truck-2.c + +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +Init: + main21_1(emptyHeap, 0, 0, 0, emptyHeap, 0, 0, 0) +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +Final: + main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +Failed assertion: + +UNSAFE diff --git a/regression-tests/toh-contract-translation/get-1.c b/regression-tests/toh-contract-translation/get-1.c new file mode 100644 index 0000000..dd4595e --- /dev/null +++ b/regression-tests/toh-contract-translation/get-1.c @@ -0,0 +1,34 @@ + +int r1; +int n_init; + +/*@contract@*/ +int get(int* p) { + if (*p <= 0) { + return 0; + } else { + *p = *p - 1; + return 1 + get(p); + } +} + +int* n; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + r1 = non_det_int(); + n_init = non_det_int(); + n = non_det_int_ptr(); + + assume((n_init > 0)); + + n = (int*) malloc(sizeof(*n)); + *n = n_init; + r1 = get(n); + + assert(((r1 >= n_init) && (r1 <= n_init))); +} diff --git a/regression-tests/toh-contract-translation/get-2.c b/regression-tests/toh-contract-translation/get-2.c new file mode 100644 index 0000000..5df848c --- /dev/null +++ b/regression-tests/toh-contract-translation/get-2.c @@ -0,0 +1,42 @@ +// TODO: This test currently results in +// +// java.lang.Exception: Predicate generation failed +// (error "Predicate generation failed") +// Other Error: Predicate generation failed +// +// +int r1; +int n_init; + + +int get(int* p) { + if (*p <= 0) { + return 0; + } else { + *p = *p - 1; + return 1 + get(p); + } +} + +int* n; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + r1 = non_det_int(); + n_init = non_det_int(); + n = non_det_int_ptr(); + + assume((n_init > 0)); + + n = (int*) malloc(sizeof(*n)); + // Commenting out the following line makes the test pass, + // but leads to undefined behavior. + *n = n_init; + r1 = get(n); + + assert(((r1 >= n_init) && (r1 <= (n_init * n_init)))); +} diff --git a/regression-tests/toh-contract-translation/incdec-1.c b/regression-tests/toh-contract-translation/incdec-1.c new file mode 100644 index 0000000..ddb5134 --- /dev/null +++ b/regression-tests/toh-contract-translation/incdec-1.c @@ -0,0 +1,40 @@ +int a_init; +int b_init; + +/*@contract@*/ +void increment(int* val) { + (*val)++; +} + +/*@contract@*/ +void decrement(int* val) { + (*val)--; +} + +int *a; +int *b; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + a_init = non_det_int(); + b_init = non_det_int(); + a = non_det_int_ptr(); + b = non_det_int_ptr(); + + assume(1); + + a = (int*) malloc(sizeof(*a)); + b = (int*) malloc(sizeof(*b)); + + *a = a_init; + *b = b_init; + + increment(a); + decrement(b); + + assert(((*a == (a_init + 1)) && (*b == (b_init - 1)))); +} diff --git a/regression-tests/toh-contract-translation/incdec-2.c b/regression-tests/toh-contract-translation/incdec-2.c new file mode 100644 index 0000000..844532f --- /dev/null +++ b/regression-tests/toh-contract-translation/incdec-2.c @@ -0,0 +1,34 @@ +int a_init; + +/*@contract@*/ +void increment(int* val) { + (*val)++; +} + +/*@contract@*/ +void decrement(int* val) { + (*val)--; +} + +int *a; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + a_init = non_det_int(); + a = non_det_int_ptr(); + + assume(1); + + a = (int*) malloc(sizeof(*a)); + + *a = a_init; + + increment(a); + decrement(a); + + assert((*a == a_init)); +} diff --git a/regression-tests/toh-contract-translation/incdec-3.c b/regression-tests/toh-contract-translation/incdec-3.c new file mode 100644 index 0000000..7edd43e --- /dev/null +++ b/regression-tests/toh-contract-translation/incdec-3.c @@ -0,0 +1,37 @@ +int a_init; +int b_init; + +/*@contract@*/ +void increment(int* val) { + (*val)++; +} + +/*@contract@*/ +void decrement(int* val) { + increment(val); + *val = *val - 2; +} + +int *a; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + a_init = non_det_int(); + b_init = non_det_int(); + a = non_det_int_ptr(); + + assume(1); + + a = (int*) malloc(sizeof(*a)); + + *a = a_init; + + increment(a); + decrement(a); + + assert((*a == a_init)); +} diff --git a/regression-tests/toh-contract-translation/max-1.c b/regression-tests/toh-contract-translation/max-1.c new file mode 100644 index 0000000..8cab084 --- /dev/null +++ b/regression-tests/toh-contract-translation/max-1.c @@ -0,0 +1,40 @@ +int r; + +/*@contract@*/ +int findMax(int* x, int* y) { + if(*x >= *y) + return *x; + else + return *y; +} + +int* a; +int* b; +int a_init; +int b_init; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + r = non_det_int(); + a = non_det_int_ptr(); + b = non_det_int_ptr(); + a_init = non_det_int(); + b_init = non_det_int(); + + assume(1); + + a = (int*) malloc(sizeof(*a)); + b = (int*) malloc(sizeof(*b)); + + *a = a_init; + *b = b_init; + + r = findMax(a, b); + + assert(!((a_init >= b_init) && !(r == a_init))); + assert(!((b_init > a_init) && !(r == b_init))); +} diff --git a/regression-tests/toh-contract-translation/max-2.c b/regression-tests/toh-contract-translation/max-2.c new file mode 100644 index 0000000..9d7a29d --- /dev/null +++ b/regression-tests/toh-contract-translation/max-2.c @@ -0,0 +1,41 @@ +int* r; + +/*@contract@*/ +void findMax(int* x, int* y, int* max) { + if(*x >= *y) + *max = *x; + else + *max = *y; +} + +int* a; +int* b; +int a_init; +int b_init; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + r = non_det_int_ptr(); + a = non_det_int_ptr(); + b = non_det_int_ptr(); + a_init = non_det_int(); + b_init = non_det_int(); + + assume(1); + + a = (int*) malloc(sizeof(*a)); + b = (int*) malloc(sizeof(*b)); + r = (int*) malloc(sizeof(*r)); + + *a = a_init; + *b = b_init; + + findMax(a, b, r); + + assert(!((a_init >= b_init) && !(*r == a_init))); + assert(!((b_init > a_init) && !(*r == b_init))); +} diff --git a/regression-tests/toh-contract-translation/multadd-1.c b/regression-tests/toh-contract-translation/multadd-1.c new file mode 100644 index 0000000..59f1265 --- /dev/null +++ b/regression-tests/toh-contract-translation/multadd-1.c @@ -0,0 +1,43 @@ +/*@contract@*/ +void multiplyByTwo(int* num) { + *num = *num * 2; +} + +/*@contract@*/ +void addTwoNumbers(int* a, int* b, int* result) { + *result = *a + *b; +} + +int* a; +int* b; +int* result; +int a_init; +int b_init; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + a = non_det_int_ptr(); + b = non_det_int_ptr(); + result = non_det_int_ptr(); + a_init = non_det_int(); + b_init = non_det_int(); + + assume(1); + + a = (int*) malloc(sizeof(*a)); + b = (int*) malloc(sizeof(*b)); + result = (int*) malloc(sizeof(*result)); + + *a = a_init; + *b = b_init; + + multiplyByTwo(a); + addTwoNumbers(a, b, result); + + assert((*a == (a_init * 2))); + assert((*result == (*a + b_init))); +} diff --git a/regression-tests/toh-contract-translation/multadd-2.c b/regression-tests/toh-contract-translation/multadd-2.c new file mode 100644 index 0000000..1afffa8 --- /dev/null +++ b/regression-tests/toh-contract-translation/multadd-2.c @@ -0,0 +1,52 @@ + +/*@contract@*/ +void addNumbers(int* x, int* y, int* result) { + *result = *x + *y; +} + +/*@contract@*/ +void multiplyNumbers(int* x, int* y, int* result) { + *result = *x * *y; +} + +int* a; +int* b; +int* c; +int* result1; +int* result2; +int a_init; +int b_init; +int c_init; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + a = non_det_int_ptr(); + b = non_det_int_ptr(); + c = non_det_int_ptr(); + result1 = non_det_int_ptr(); + result2 = non_det_int_ptr(); + a_init = non_det_int(); + b_init = non_det_int(); + c_init = non_det_int(); + + a = (int*) malloc(sizeof(*a)); + b = (int*) malloc(sizeof(*b)); + c = (int*) malloc(sizeof(*c)); + result1 = (int*) malloc(sizeof(*result1)); + result2 = (int*) malloc(sizeof(*result2)); + *a = a_init; + *b = b_init; + *c = c_init; + + addNumbers(a, b, result1); + multiplyNumbers(a, b, result2); + addNumbers(b, c, c); + + assert((*result1 == (a_init + b_init))); + assert((*result2 == (a_init * b_init))); + assert((*c == (b_init + c_init))); +} diff --git a/regression-tests/toh-contract-translation/multadd-3.c b/regression-tests/toh-contract-translation/multadd-3.c new file mode 100644 index 0000000..6c695fa --- /dev/null +++ b/regression-tests/toh-contract-translation/multadd-3.c @@ -0,0 +1,51 @@ + +/*@contract@*/ +void addNumbers(int* x, int* y, int* result) { + *result = *x + *y; +} + +/*@contract@*/ +void multiplyNumbers(int* x, int* y, int* result) { + *result = *x * *y; +} + +int* a; +int* b; +int* c; +int* result1; +int* result2; +int a_init; +int b_init; +int c_init; + +extern int non_det_int(); +extern int* non_det_int_ptr(); + +void main() +{ + //Non-det assignment of global variables + a = non_det_int_ptr(); + b = non_det_int_ptr(); + c = non_det_int_ptr(); + result1 = non_det_int_ptr(); + result2 = non_det_int_ptr(); + a_init = non_det_int(); + b_init = non_det_int(); + c_init = non_det_int(); + + a = (int*) malloc(sizeof(*a)); + b = (int*) malloc(sizeof(*b)); + result1 = (int*) malloc(sizeof(*result1)); + c = result1; + result2 = (int*) malloc(sizeof(*result2)); + *a = a_init; + *b = b_init; + + addNumbers(a, b, result1); + multiplyNumbers(a, b, result2); + addNumbers(b, c, c); + + assert((*result1 == ((a_init + b_init) + b_init))); + assert((*result2 == (a_init * b_init))); + assert((*c == *result1)); +} diff --git a/regression-tests/toh-contract-translation/runtests b/regression-tests/toh-contract-translation/runtests new file mode 100755 index 0000000..a8626a8 --- /dev/null +++ b/regression-tests/toh-contract-translation/runtests @@ -0,0 +1,17 @@ +#!/bin/sh + +LAZABS=../../tri + +TESTS="get-1.c \ + incdec-1.c \ + incdec-2.c \ + max-1.c \ + max-2.c \ + multadd-1.c \ + truck-2.c" + +for name in $TESTS; do + echo + echo $name + $LAZABS -cex -acsl "$@" $name 2>&1 | grep -v 'at ' +done \ No newline at end of file diff --git a/regression-tests/toh-contract-translation/truck-1.c b/regression-tests/toh-contract-translation/truck-1.c new file mode 100644 index 0000000..5adbb4e --- /dev/null +++ b/regression-tests/toh-contract-translation/truck-1.c @@ -0,0 +1,41 @@ + +int driver_distance; +int r_cab_position; + +typedef struct Human { + int distance_driven; +} Human; + +typedef struct Truck { + int x; + struct Human driver; +} *TruckPtr; + +/*@contract@*/ +void tick(TruckPtr t) { + t->x++; + t->driver.distance_driven++; +} + +extern int non_det_int(); + +void main() +{ + //Non-det assignment of global variables + driver_distance = non_det_int(); + r_cab_position = non_det_int(); + + assume(1); + + TruckPtr r_cab = malloc(sizeof(*r_cab)); + r_cab->x = 0; + r_cab->driver.distance_driven = 0; + tick(r_cab); + tick(r_cab); + + driver_distance = r_cab->driver.distance_driven; + r_cab_position = r_cab->x; + + assert((driver_distance == 2)); + assert((r_cab_position == 2)); +} diff --git a/regression-tests/toh-contract-translation/truck-2.c b/regression-tests/toh-contract-translation/truck-2.c new file mode 100644 index 0000000..0eed9cd --- /dev/null +++ b/regression-tests/toh-contract-translation/truck-2.c @@ -0,0 +1,47 @@ + +int driver1_distance; +int driver2_distance; +int r_cab_position; + +typedef struct Human { + int distance_driven; +} *HumanPtr; + +typedef struct Truck { + int x; + struct Human* driver; +} *TruckPtr; + +//No inferred contract found for tick +void tick(TruckPtr t) { + t->x++; + t->driver->distance_driven++; +} + +/*@ + requires \true; + ensures driver1_distance == 2 && driver2_distance == 3; + ensures r_cab_position == driver1_distance + driver2_distance; + assigns driver1_distance, driver2_distance, r_cab_position; +*/ +int main(void) { + TruckPtr r_cab = malloc(sizeof(*r_cab)); + HumanPtr driver1 = malloc(sizeof(*driver1)); + HumanPtr driver2 = malloc(sizeof(*driver2)); + r_cab->x = 0; + driver1->distance_driven = 0; + driver2->distance_driven = 0; + + r_cab->driver = driver1; + tick(r_cab); + tick(r_cab); + + r_cab->driver = driver2; + tick(r_cab); + tick(r_cab); + tick(r_cab); + + driver1_distance = driver1->distance_driven; + driver2_distance = driver2->distance_driven; + r_cab_position = r_cab->x; +} diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index baa5135..2ccd6fb 100644 --- a/src/tricera/Main.scala +++ b/src/tricera/Main.scala @@ -44,7 +44,7 @@ import lazabs.horn.Util.NullStream import lazabs.prover._ import tricera.concurrency.{CCReader, TriCeraPreprocessor} -import tricera.Util.SourceInfo +import tricera.Util.{SourceInfo, printlnDebug} import tricera.benchmarking.Benchmarking._ import tricera.concurrency.CCReader.{CCAssertionClause, CCClause} import tricera.concurrency.ccreader.CCExceptions._ @@ -600,10 +600,119 @@ class Main (args: Array[String]) { if maybeEnc.isEmpty || !maybeEnc.get.prePredsToReplace.contains(ctx.prePred.pred) && !maybeEnc.get.postPredsToReplace.contains(ctx.postPred.pred)) { + + var acslProcessedSolution = processedSolution + + if (modelledHeapRes) { + def applyProcessor(processor: ContractProcessor, + solution: SolutionProcessor.Solution + ): SolutionProcessor.Solution = { + printlnDebug(s"----- Applying $processor to $fun.") + val (newPrecondition, newPostcondition) = + processor(solution, fun, ctx) + printlnDebug("----- Precondition:") + printlnDebug(solution(ctx.prePred.pred).toString) + printlnDebug("----- New Precondition:") + printlnDebug(newPrecondition.toString) + printlnDebug("----- Postcondition:") + printlnDebug(solution(ctx.postPred.pred).toString) + printlnDebug("----- New Postcondition:") + printlnDebug(newPostcondition.toString) + solution + (ctx.prePred.pred -> newPrecondition) + + (ctx.postPred.pred -> newPostcondition) + } + + import ap.parser.IFormula + import ap.parser.IExpression.Predicate + def addClauses(clauses: Option[IFormula], + predicate: Predicate, + solution: SolutionProcessor.Solution) + : SolutionProcessor.Solution = { + clauses match { + case Some(clauseFormula) => + val newContractCondition = + solution(predicate).asInstanceOf[IFormula] & + clauseFormula + solution + (predicate -> newContractCondition) + case None => + solution + } + } + + acslProcessedSolution = + applyProcessor(PostconditionSimplifier, acslProcessedSolution) + + val heapPropProcessors = Seq( + PointerPropProcessor, + AssignmentProcessor + ) + + for (prsor <- heapPropProcessors) { + val contractInfo = ContractInfo(solution, fun, ctx) + val preCCI = + ContractConditionInfo(ctx.prePred.pred, contractInfo) + val postCCI = + ContractConditionInfo(ctx.postPred.pred, contractInfo) + + printlnDebug(s"----- Applying $prsor to precondition of $fun") + printlnDebug("----- Precondition:") + printlnDebug(preCCI.contractCondition.toString) + + val preClauses = + prsor.getClauses(preCCI.contractCondition, preCCI) + + printlnDebug("Result:") + printlnDebug(preClauses.toString) + + acslProcessedSolution = addClauses( + preClauses, ctx.prePred.pred, acslProcessedSolution) + + printlnDebug(s"----- Applying $prsor to postcondition of $fun") + printlnDebug("----- Postcondition:") + printlnDebug(postCCI.contractCondition.toString) + + val postClauses = + prsor.getClauses(postCCI.contractCondition, postCCI) + + printlnDebug("----- Result:") + printlnDebug(postClauses.toString) + + acslProcessedSolution = addClauses( + postClauses,ctx.postPred.pred, acslProcessedSolution) + } + + val printHeapExprProcessors = Seq( + TheoryOfHeapProcessor, + ADTSimplifier, + ADTExploder, + ToVariableForm, + ACSLExpressionProcessor, + ClauseRemover) + + for (processor <- printHeapExprProcessors) { + acslProcessedSolution = applyProcessor(processor, acslProcessedSolution) + } + } + + printlnDebug("----- Applying ACSLLineariser to precondition:") + printlnDebug(acslProcessedSolution(ctx.prePred.pred).toString) + + val fPre = ACSLLineariser asString + acslProcessedSolution(ctx.prePred.pred) + + printlnDebug("----- Result:") + printlnDebug(fPre.toString) + printlnDebug("----- Applying ACSLLineariser to postcondition:") + printlnDebug(acslProcessedSolution(ctx.postPred.pred).toString) + + val fPost = ACSLLineariser asString acslProcessedSolution(ctx.postPred.pred) + printlnDebug("----- Result:") + printlnDebug(fPost) + // todo: implement replaceArgs as a solution processor def funContractToACSLString(fPred : Predicate, argNames : Seq[String]) : String = { - val fPredToSol = fPred -> processedSolution(fPred) + val fPredToSol = fPred -> acslProcessedSolution(fPred) val fPredClause = clausifySolution(fPredToSol, argNames) ACSLLineariser asString fPredClause.constraint } @@ -651,8 +760,7 @@ class Main (args: Array[String]) { } Safe case Right(cex) => { - val clauseToUnmergedRichClauses : Map[Clause, Seq[CCClause]] = - cex._2.iterator.map{ + val clauseToUnmergedRichClauses : Map[Clause, Seq[CCClause]] = cex._2.iterator.map { case (_, clause) => val richClauses : Seq[CCClause] = mergedToOriginal get clause match { diff --git a/src/tricera/Util.scala b/src/tricera/Util.scala index d237e5f..7a1dad1 100644 --- a/src/tricera/Util.scala +++ b/src/tricera/Util.scala @@ -46,6 +46,11 @@ object Util { def warn(msg : String) : Unit = Console.err.println("Warning: " + msg) + def printlnDebug(msg : String) : Unit = { + if (params.TriCeraParameters.get.printDebugMessages) + println(msg) + } + case class SourceInfo (line : Int, col : Int) private def getIntegerField(obj: Any, fieldName: String): Int = { diff --git a/src/tricera/acsl/ACSLTranslator.scala b/src/tricera/acsl/ACSLTranslator.scala index 97b91f4..80de672 100644 --- a/src/tricera/acsl/ACSLTranslator.scala +++ b/src/tricera/acsl/ACSLTranslator.scala @@ -50,12 +50,15 @@ object ACSLTranslator { def getGlobals : Seq[CCVar] def sortWrapper(s: Sort): Option[IFunction] def sortGetter(s: Sort): Option[IFunction] + def wrapperSort(wrapper: IFunction): Option[Sort] + def getterSort(getter: IFunction): Option[Sort] def getCtor(s: Sort): Int def getTypOfPointer(t: CCType): CCType def isHeapEnabled: Boolean def getHeap: Heap def getHeapTerm: ITerm def getOldHeapTerm : ITerm + val getStructMap: Map[IFunction, CCStruct] val annotationBeginSourceInfo : SourceInfo val annotationNumLines : Int } diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala index c6bd711..6e4fce8 100644 --- a/src/tricera/concurrency/CCReader.scala +++ b/src/tricera/concurrency/CCReader.scala @@ -738,6 +738,10 @@ class CCReader private (prog : Program, objectSorts.zip(objectGetters).toMap val sortWrapperMap : Map[Sort, MonoSortedIFunction] = objectSorts.zip(objectWrappers).toMap + val getterSortMap : Map[MonoSortedIFunction, Sort] = + sortGetterMap.map(_.swap) + val wrapperSortMap : Map[MonoSortedIFunction, Sort] = + sortWrapperMap.map(_.swap) val sortCtorIdMap : Map[Sort, Int] = objectSorts.zip(0 until structCount+structCtorsOffset).toMap @@ -967,7 +971,19 @@ class CCReader private (prog : Program, def sortGetter(s: Sort): Option[MonoSortedIFunction] = sortGetterMap.get(s) + + def wrapperSort(wrapper: IFunction): Option[Sort] = wrapper match { + case w: MonoSortedIFunction => + wrapperSortMap.get(w) + case _ => None + } + def getterSort(getter: IFunction): Option[Sort] = getter match { + case g: MonoSortedIFunction => + getterSortMap.get(g) + case _ => None + } + def getTypOfPointer(t: CCType): CCType = t match { case p: CCHeapPointer => p.typ case t => t @@ -975,6 +991,9 @@ class CCReader private (prog : Program, def getCtor(s: Sort): Int = sortCtorIdMap(s) + override val getStructMap: Map[IFunction, CCStruct] = + structDefs.values.toSet.map((struct: CCStruct) => (struct.ctor, struct)).toMap + override val annotationBeginSourceInfo : SourceInfo = getSourceInfo(fun) override val annotationNumLines : Int = // todo: this is currently incorrect - to be fixed! @@ -4333,6 +4352,19 @@ private def collectVarDecls(dec : Dec, sortWrapperMap get s override def sortGetter(s: Sort): Option[IFunction] = sortGetterMap get s + override def wrapperSort(wrapper: IFunction): Option[Sort] = + wrapper match { + case w: MonoSortedIFunction => + wrapperSortMap.get(w) + case _ => None + } + override def getterSort(getter: IFunction): Option[Sort] = + getter match { + case g: MonoSortedIFunction => + getterSortMap.get(g) + case _ => None + } + override def getCtor(s: Sort): Int = sortCtorIdMap(s) override def getTypOfPointer(t: CCType): CCType = t match { @@ -4341,13 +4373,19 @@ private def collectVarDecls(dec : Dec, } override def isHeapEnabled: Boolean = modelHeap override def getHeap: HeapObj = - if (modelHeap) heap else throw NeedsHeapModelException + if (modelHeap) heap + else throw new TranslationException("getHeap called with no heap!") override def getHeapTerm: ITerm = if (modelHeap) stmSymex.getValues(GlobalVars.lastIndexWhere(heapVar)).toTerm - else throw NeedsHeapModelException - override def getOldHeapTerm: ITerm = - getHeapTerm // todo: heap term for exit predicate? + else throw new TranslationException("getHeapTerm called with no heap!") + override def getOldHeapTerm: ITerm = { + if (modelHeap) getHeapTerm + else throw new TranslationException("getOldHeapTerm called with no heap!") + } // todo: heap term for exit predicate? + + override val getStructMap: Map[IFunction, CCStruct] = + structDefs.values.toSet.map((struct: CCStruct) => (struct.ctor, struct)).toMap override val annotationBeginSourceInfo : SourceInfo = getSourceInfo(stm) @@ -4400,6 +4438,18 @@ private def collectVarDecls(dec : Dec, sortWrapperMap get s override def sortGetter(s : Sort) : Option[IFunction] = sortGetterMap get s + override def wrapperSort(wrapper: IFunction): Option[Sort] = + wrapper match { + case w: MonoSortedIFunction => + wrapperSortMap.get(w) + case _ => None + } + override def getterSort(getter: IFunction): Option[Sort] = + getter match { + case g: MonoSortedIFunction => + getterSortMap.get(g) + case _ => None + } override def getCtor(s : Sort) : Int = sortCtorIdMap(s) override def getTypOfPointer(t : CCType) : CCType = t match { @@ -4415,6 +4465,9 @@ private def collectVarDecls(dec : Dec, else throw NeedsHeapModelException override def getOldHeapTerm : ITerm = getHeapTerm // todo: heap term for exit predicate? + + override val getStructMap: Map[IFunction, CCStruct] = + structDefs.values.toSet.map((struct: CCStruct) => (struct.ctor, struct)).toMap override val annotationBeginSourceInfo : SourceInfo = getSourceInfo(loop_annot) diff --git a/src/tricera/params/TriCeraParameters.scala b/src/tricera/params/TriCeraParameters.scala index d9cdcd1..16082ac 100644 --- a/src/tricera/params/TriCeraParameters.scala +++ b/src/tricera/params/TriCeraParameters.scala @@ -96,6 +96,7 @@ class TriCeraParameters extends GlobalParameters { var useArraysForHeap : Boolean = false var devMode : Boolean = false + var printDebugMessages : Boolean = false var displayACSL = false var inferLoopInvariants = false @@ -125,7 +126,7 @@ class TriCeraParameters extends GlobalParameters { private val greeting = "TriCera v" + version + ".\n(C) Copyright " + "2012-2024 Zafer Esen and Philipp Ruemmer\n" + - "Contributors: Pontus Ernstedt, Hossein Hojjat" + "Contributors: Pontus Ernstedt, Hossein Hojjat, Oskar Soederberg" private def parseArgs(args: List[String], shouldExecute : Boolean = true): Boolean = args match { @@ -265,6 +266,7 @@ class TriCeraParameters extends GlobalParameters { case "-assert" :: rest => TriCeraParameters.get.assertions = true; parseArgs(rest) case "-assertNoVerify" :: rest => TriCeraParameters.get.assertions = true; TriCeraParameters.get.fullSolutionOnAssert = false; parseArgs(rest) case "-dev" :: rest => devMode = true; showVarLineNumbersInTerms = true; parseArgs(rest) + case "-debug" :: rest => printDebugMessages = true; parseArgs(rest) case "-varLines" :: rest => showVarLineNumbersInTerms = true; parseArgs(rest) case "-sym" :: rest => symexEngine = GlobalParameters.SymexEngine.BreadthFirstForward diff --git a/src/tricera/postprocessor/ACSLExpressionProcessor.scala b/src/tricera/postprocessor/ACSLExpressionProcessor.scala new file mode 100644 index 0000000..5e438c0 --- /dev/null +++ b/src/tricera/postprocessor/ACSLExpressionProcessor.scala @@ -0,0 +1,241 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + /* ACSLExpressionProcessor.scala + * + * See ACSLProcessor in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this contract processor, theory of heap expressions are translated to ACSL + * expressions. + * + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import ap.theories.Heap.HeapFunExtractor +import ap.theories.ADT +import ap.theories.Heap +import ap.theories.Theory +import ContractConditionType._ +import ap.types.MonoSortedIFunction +import tricera.acsl.ACSLTranslator.{FunctionContext => ACSLFunctionContext} + +object ACSLExpressionProcessor + extends ContractProcessor { + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + val visitor = + new ACSLExpressionVisitor(cci) + visitor(cci.contractCondition) + } + + class ACSLExpressionVisitor( + cci: ContractConditionInfo + ) extends CollectingVisitor[Int, IExpression] { + + def apply(contractCondition: IFormula): IFormula = { + visit(contractCondition, 0).asInstanceOf[IFormula] + } + + override def preVisit( + t: IExpression, + quantifierDepth: Int + ): PreVisitResult = t match { + case v: IVariableBinder => UniSubArgs(quantifierDepth + 1) + case _ => KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[IExpression] + ): IExpression = { + + t match { + case IFunApp( + selector: MonoSortedIFunction, + Seq( + IFunApp( + getFun, + Seq( + TheoryOfHeapFunApp( + readFun, + Seq(Var(h), Var(p)) + ) + ) + ) + ) + ) + if (cci.isGetter(getFun) && + cci.isReadFun(readFun) && + cci.isSelector(selector) && + (cci.isCurrentHeap(h, quantifierDepth) || + cci.isOldHeap(h, quantifierDepth))) => + cci.contractConditionType match { + case Precondition => + ACSLExpression.arrowFunApp( + ACSLExpression.arrow, + p, + selector, + quantifierDepth, + cci + ) + case Postcondition => + ( + cci.isOldHeap(h, quantifierDepth), + cci.isOldVar(p, quantifierDepth), + cci.isParam(p, quantifierDepth) + ) match { + case (false, false, false) => + // read(@h, p), p not param => p->a + ACSLExpression.arrowFunApp( + ACSLExpression.arrow, + p, + selector, + quantifierDepth, + cci + ) + case (false, true, true) => + // read(@h, p_0), p is param => p->a + ACSLExpression.arrowFunApp( + ACSLExpression.arrow, + p, + selector, + quantifierDepth, + cci + ) + case (false, true, false) => + // read(@h, p_0), p not param => \old(p)->a + ACSLExpression.arrowFunApp( + ACSLExpression.arrowOldPointer, + p, + selector, + quantifierDepth, + cci + ) + case (true, true, true) => + // read(@h_0, p_0), p is param => \old(p->a) + ACSLExpression.arrowFunApp( + ACSLExpression.oldArrow, + p, + selector, + quantifierDepth, + cci + ) + case (true, true, false) => + // read(@h_0, p_0), p not param => \old(p->a) + ACSLExpression.arrowFunApp( + ACSLExpression.oldArrow, + p, + selector, + quantifierDepth, + cci + ) + case _ => t update subres + } + } + + // read(h,p).get_ ~> *p + case IFunApp( + getFun, + Seq( + TheoryOfHeapFunApp( + readFun, + Seq(Var(h), Var(p)) + ) + ) + ) + if (cci.isGetter(getFun) && + cci.isReadFun(readFun) && + (cci.isCurrentHeap(h, quantifierDepth) || + cci.isOldHeap(h, quantifierDepth))) => { + cci.contractConditionType match { + case Precondition => + ACSLExpression.derefFunApp( + ACSLExpression.deref, + p, + quantifierDepth, + cci + ) + case Postcondition => + ( + cci.isOldHeap(h, quantifierDepth), + cci.isOldVar(p, quantifierDepth), + cci.isParam(p, quantifierDepth) + ) match { + case (false, false, false) => // read(@h, p), p not param + ACSLExpression.derefFunApp( + ACSLExpression.deref, + p, + quantifierDepth, + cci + ) + case (false, true, true) => // read(@h, p_0), p is param + ACSLExpression.derefFunApp( + ACSLExpression.deref, + p, + quantifierDepth, + cci + ) + case (false, true, false) => // read(@h, p_0), p not param + ACSLExpression.derefFunApp( + ACSLExpression.derefOldPointer, + p, + quantifierDepth, + cci + ) + case (true, true, true) => // read(@h_0, p_0), p is param + ACSLExpression.derefFunApp( + ACSLExpression.oldDeref, + p, + quantifierDepth, + cci + ) + case (true, true, false) => // read(@h_0, p_0), p not param + ACSLExpression.derefFunApp( + ACSLExpression.oldDeref, + p, + quantifierDepth, + cci + ) + case _ => t update subres + } + } + } + + case _ => t update subres + } + } + } +} diff --git a/src/tricera/postprocessor/ACSLFunctions.scala b/src/tricera/postprocessor/ACSLFunctions.scala new file mode 100644 index 0000000..e7af4d5 --- /dev/null +++ b/src/tricera/postprocessor/ACSLFunctions.scala @@ -0,0 +1,146 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* ACSLExpression.scala + * + * Defines IFunctiions and Predicates corresponding to ACSL expressions. + */ + +package tricera.postprocessor + +import ap.parser._ +import ap.terfor.ConstantTerm +import IExpression._ +import ap.types.MonoSortedIFunction + +object ACSLExpression { + val valid = new Predicate("\\valid", 1) + val deref = new IFunction("deref", 1, false, false) // *p + val oldDeref = new IFunction("oldDeref", 1, false, false) // \old(*p) + val derefOldPointer = + new IFunction("derefOldPointer", 1, false, false) // *\old(p) + val arrow = new IFunction("arrow", 2, false, false) // p->a + val arrowOldPointer = + new IFunction("arrowOldPointer", 2, false, false) // \old(p)->a + val oldArrow = new IFunction("oldArrow", 2, false, false) // \old(p)->a + val separated = new Predicate("\\separated", 2) // \separated(p1, p2) + + val functions = Set(deref, oldDeref, derefOldPointer, arrow, arrowOldPointer, oldArrow) + val predicates = Set(valid, separated) + + // Here a ConstantTerm is introduced as a container for the variable name + def derefFunApp( + derefFunction: IFunction, + pointer: ISortedVariable, + quantifierDepth: Int, + cci: ContractConditionInfo + ) = { + val name = cci.stripOld(cci.getVarName(pointer, quantifierDepth).get) + IFunApp(derefFunction, Seq(IConstant(new ConstantTerm(name)))) + } + + def arrowFunApp( + arrowFunction: IFunction, + pointer: ISortedVariable, + selector: MonoSortedIFunction, + quantifierDepth: Int, + cci: ContractConditionInfo + ) = { + val pointerName = cci.stripOld( + cci.getVarName(pointer, quantifierDepth).get + ) + val selectorName = selector.name + IFunApp( + arrowFunction, + Seq( + IConstant(new ConstantTerm(pointerName)), + IConstant(new ConstantTerm(selectorName)) + ) + ) + } + + def separatedPointers( + pointers: Set[ISortedVariable], + quantifierDepth: Int, + cci: ContractConditionInfo + ): IFormula = { + + def separatedAtom(p1: String, p2: String): IFormula = { + IAtom( + separated, + Seq(IConstant(new ConstantTerm(p1)), IConstant(new ConstantTerm(p2))) + ).asInstanceOf[IFormula] + } + + val pointerNames = variableSetToRawNameSeq(pointers, quantifierDepth, cci) + if (pointerNames.size >= 2) { + pointerNames + .combinations(2) + .map({ case Seq(p1, p2) => + separatedAtom(p1, p2) + }) + .reduceLeft(_ & _) + } else { + IBoolLit(true) + } + } + + def validPointers( + pointers: Set[ISortedVariable], + quantifierDepth: Int, + cci: ContractConditionInfo + ): IFormula = { + def validAtom(p: String) = { + IAtom(valid, Seq(IConstant(new ConstantTerm(p)))).asInstanceOf[IFormula] + } + + val pointerNames = variableSetToRawNameSeq(pointers, quantifierDepth, cci) + pointerNames.size match { + case s if s >= 2 => + pointerNames + .map((p) => validAtom(p)) + .reduceLeft(_ & _) + case s if s == 1 => + validAtom(pointerNames.head) + case _ => IBoolLit(true) + } + } + + def variableSetToRawNameSeq( + variableSet: Set[ISortedVariable], + quantifierDepth: Int, + cci: ContractConditionInfo + ): Seq[String] = { + variableSet + .map(pointer => + cci.stripOld(cci.getVarName(pointer, quantifierDepth).get) + ) + .toSeq + } +} diff --git a/src/tricera/postprocessor/ACSLLineariser.scala b/src/tricera/postprocessor/ACSLLineariser.scala index 15e3fcf..c9534e2 100644 --- a/src/tricera/postprocessor/ACSLLineariser.scala +++ b/src/tricera/postprocessor/ACSLLineariser.scala @@ -316,6 +316,30 @@ object ACSLLineariser { Seq(IIntLit(upper), IIntLit(lower), t)) => TryAgain(t, ctxt.addOpPrec("[" + upper + ":" + lower + "]", 10)) + // constant is a temporary container of the variable name + case IFunApp(ACSLExpression.deref, Seq(_: IConstant)) => + print("*") + noParentOp(ctxt) + + case IFunApp(ACSLExpression.derefOldPointer, Seq(_: IConstant)) => + print("*\\old(") + SubArgs(List(ctxt setParentOp ")")) + + case IFunApp(ACSLExpression.oldDeref, Seq(_: IConstant)) => + print("\\old(*") + SubArgs(List(ctxt setParentOp ")")) + + case IFunApp(ACSLExpression.arrow, Seq(_: IConstant, _: IConstant)) => + allButLast(ctxt setPrecLevel 0, "->", "", 2) + + case IFunApp(ACSLExpression.arrowOldPointer, Seq(_: IConstant, _: IConstant)) => + print("\\old(") + allButLast(ctxt setPrecLevel 0, ")->", "", 2) + + case IFunApp(ACSLExpression.oldArrow, Seq(_: IConstant, _: IConstant)) => + print("\\old(") + allButLast(ctxt setPrecLevel 0, "->", ")", 2) + case IFunApp(fun, _) => { if (fun.arity == 1) { allButLast(ctxt setPrecLevel 0, ".", "." + fun2Identifier(fun), 1) diff --git a/src/tricera/postprocessor/ADTExploder.scala b/src/tricera/postprocessor/ADTExploder.scala index db7a9cd..6bc4fa6 100644 --- a/src/tricera/postprocessor/ADTExploder.scala +++ b/src/tricera/postprocessor/ADTExploder.scala @@ -34,10 +34,17 @@ import ap.theories.ADT.ADTProxySort import ap.theories.{ADT, TheoryRegistry} import ap.types.{MonoSortedIFunction, SortedConstantTerm} -object ADTExploder extends SolutionProcessor { +object ADTExploder extends SolutionProcessor + with ContractProcessor { def apply(expr : IFormula) : IFormula = Rewriter.rewrite(expr, explodeADTs).asInstanceOf[IFormula] + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + apply(cci.contractCondition) + } + case class ADTTerm(t : ITerm, adtSort : ADTProxySort) object adtTermExploder extends CollectingVisitor[Object, IExpression] { def getADTTerm(t : IExpression) : Option[ADTTerm] = { @@ -57,6 +64,23 @@ object ADTExploder extends SolutionProcessor { subres: Seq[IExpression]) : IExpression = { import IExpression._ + def checkExplodable(originalEq : IEquation, ctorFun : IFunction, + lhsIsCtor : Boolean) : Boolean = { + val newEq = originalEq update subres + val (newFunApp, selectorTerms, newRootTerm) = + if (lhsIsCtor) { + val Eq(newFunApp@IFunApp(_, selectorTerms), newRootTerm) = newEq + (newFunApp, selectorTerms, newRootTerm) + } else { + val Eq(newRootTerm, newFunApp@IFunApp(_, selectorTerms)) = newEq + (newFunApp, selectorTerms, newRootTerm) + } + val adtTerm = getADTTerm(newFunApp).get + val adt = adtTerm.adtSort.adtTheory + val ctorIndex = adt.constructors.indexOf(ctorFun) + ctorIndex != -1 + } + def explodeADTSelectors (originalEq : IEquation, ctorFun : IFunction, lhsIsCtor : Boolean) = { val newEq = originalEq update subres @@ -74,14 +98,16 @@ object ADTExploder extends SolutionProcessor { val selectors = adt.selectors(ctorIndex) (for ((fieldTerm, selectorInd) <- selectorTerms zipWithIndex) yield selectors(selectorInd)(newRootTerm) === - fieldTerm.asInstanceOf[ITerm]).reduce(_ &&& _) + fieldTerm).reduce(_ &&& _) } t match { - case e@Eq(funApp@IFunApp(fun, _), _) if getADTTerm(funApp).nonEmpty => - explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = true) - case e@Eq(_, funApp@IFunApp(fun, _)) if getADTTerm(funApp).nonEmpty => - explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = false) + case e@Eq(funApp@IFunApp(fun, _), _) if getADTTerm(funApp).nonEmpty && + checkExplodable(e.asInstanceOf[IEquation], fun, lhsIsCtor = true) => + explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = true) + case e@Eq(_, funApp@IFunApp(fun, _)) if getADTTerm(funApp).nonEmpty && + checkExplodable(e.asInstanceOf[IEquation], fun, lhsIsCtor = false) => + explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = false) case t@IFunApp(f,_) => val newApp = t update subres (for (theory <- TheoryRegistry lookupSymbol f; diff --git a/src/tricera/postprocessor/ADTSimplifier.scala b/src/tricera/postprocessor/ADTSimplifier.scala new file mode 100644 index 0000000..266b46e --- /dev/null +++ b/src/tricera/postprocessor/ADTSimplifier.scala @@ -0,0 +1,120 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + /* ADTSimplifier.scala + * + * See ADTProcessor in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this step, struct expressions are reduced to a simpler form containing + * fewer subexpressions, which can be handled by the ACSLExpressionProcessor + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import tricera.concurrency.ccreader.CCStruct +import ap.theories.ADT.ADTProxySort +import ap.theories.{ADT, TheoryRegistry} +import ap.types.{MonoSortedIFunction, SortedConstantTerm} +import tricera.acsl.ACSLTranslator.{FunctionContext => ACSLFunctionContext} + +object ADTSimplifier extends ContractProcessor { + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + apply(cci) + } + + def apply( + cci: ContractConditionInfo + ): IFormula = { + val adtTermSimplifier = new ADTTermSimplifier(cci) + adtTermSimplifier.visit(cci.contractCondition, null).asInstanceOf[IFormula] + } + + class ADTTermSimplifier(cci: ContractConditionInfo) + extends CollectingVisitor[Object, IExpression] { + + override def postVisit( + t: IExpression, + none: Object, + subres: Seq[IExpression] + ): IExpression = { + + import IExpression._ + + def getField( + selector: MonoSortedIFunction, + constructor: MonoSortedIFunction, + fields: Seq[ITerm] + ): Option[ITerm] = { + cci.acslContext.getStructMap.get(constructor) match { + case Some(struct) => + val index = struct.sels.map(_._1).indexOf(selector) + fields.lift(index) + case _ => None + } + } + + def structHasField( + constructor: MonoSortedIFunction, + selector: MonoSortedIFunction, + acslContext: ACSLFunctionContext + ) = { + acslContext.getStructMap.get(constructor) match { + case Some(struct) => + struct.sels.map(_._1).contains(selector) + case _ => false + } + } + + t match { + // S(x,y).a -> x + case f @ IFunApp( + selFun: MonoSortedIFunction, + Seq( + structCtorFunApp @ IFunApp( + structCtor: MonoSortedIFunction, + fields + ) + ) + ) + if cci.isStructCtor(structCtor) + && structHasField(structCtor, selFun, cci.acslContext) => + getField(selFun, structCtor, fields).get + + case _ => + t update subres + } + } + } +} diff --git a/src/tricera/postprocessor/AssignmentProcessor.scala b/src/tricera/postprocessor/AssignmentProcessor.scala new file mode 100644 index 0000000..5639e58 --- /dev/null +++ b/src/tricera/postprocessor/AssignmentProcessor.scala @@ -0,0 +1,216 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* AssignmentProcessor.scala + * + * See AssignmentExtractor in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this contract processor, postcondition equalities between dereferenced + * pointers and their values are extracted. This information is extracted from + * assignments to the heap and can only be done whenever the post heap state is + * expressed. The precondition is left unchanged. + */ + +package tricera.postprocessor + +import tricera.postprocessor.ContractConditionType._ +import ap.parser._ + +object AssignmentProcessor extends ContractProcessor with ClauseCreator { + def apply( + expr: IExpression, + valueSet: ValSet, + separatedSet: Set[ISortedVariable], + cci: ContractConditionInfo + ): Option[IFormula] = { + (new AssignmentProcessor(valueSet, separatedSet, cci)).visit(expr, 0) + } + + def processContractCondition(cci: ContractConditionInfo) = { + getClauses(cci.contractCondition, cci) match { + case Some(clauses) => + cci.contractCondition + .&(clauses) + case _ => + cci.contractCondition + } + } + + def getClauses( + expr: IExpression, + cci: ContractConditionInfo + ): Option[IFormula] = { + cci.contractConditionType match { + case Precondition => + None + case Postcondition => + val valueSet = ValSetReader.deBrujin(cci.contractCondition) + val separatedSet = + PointerPropProcessor.getSafePointers(cci.contractCondition, cci) + AssignmentProcessor(expr, valueSet, separatedSet, cci) + } + } +} + +class AssignmentProcessor( + valueSet: ValSet, + separatedSet: Set[ISortedVariable], + cci: ContractConditionInfo +) extends CollectingVisitor[Int, Option[IFormula]] { + + private def getReverseAssignments(t: IExpression): Seq[(ITerm, ITerm)] = { + t match { + case IFunApp( + writeFun, + Seq(heap, pointer, value) + ) if (cci.isWriteFun(writeFun)) => + val assignment = + (pointer.asInstanceOf[ITerm], value.asInstanceOf[ITerm]) + assignment +: getReverseAssignments(heap) + case _ => Seq() + } + } + + def assignmentToEquality( + pointer: ITerm, + value: ITerm, + heapVar: ISortedVariable + ): Option[IFormula] = { + cci.getGetter(value) match { + case Some(selector) => + Some( + IEquation( + IFunApp( + selector, + Seq(IFunApp(cci.heapTheory.read, Seq(heapVar, pointer))) + ), + IFunApp(selector, Seq(value)) + ).asInstanceOf[IFormula] + ) + case _ => None + } + } + + def extractEqualitiesFromWriteChain( + funApp: IExpression, + heapVar: ISortedVariable + ): Option[IFormula] = { + def takeWhileSeparated(assignments: Seq[(ITerm, ITerm)]) = { + if (separatedSet.isEmpty) { + Seq(assignments.head) + } else { + assignments.takeWhile { case (pointer, value) => + separatedSet.exists(valueSet.areEqual(pointer, _)) + } + } + } + + def takeFirstAddressWrites(assignments: Seq[(ITerm, ITerm)]) = { + assignments + .foldLeft((Set[ITerm](), Seq[(ITerm, ITerm)]())) { + case ((seen, acc), (pointer, value)) => + if (seen.contains(pointer)) { + (seen, acc) + } else { + (seen + pointer, acc :+ (pointer, value)) + } + } + ._2 + } + + val assignments = getReverseAssignments(funApp) + val separatedAssignments = takeWhileSeparated(assignments) + val currentAssignments = takeFirstAddressWrites(separatedAssignments) + .map { case (pointer, value) => + assignmentToEquality(pointer, value, heapVar).get + } + currentAssignments.size match { + case s if s >= 2 => + Some(currentAssignments.reduce(_ & _)) + case 1 => + Some(currentAssignments.head) + case _ => None + } + } + + def shiftFormula( + formula: Option[IFormula], + quantifierDepth: Int + ): Option[IFormula] = { + formula match { + case Some(f) => + if (ContainsQuantifiedVisitor(f, quantifierDepth)) { + None + } else { + Some(VariableShiftVisitor(f, quantifierDepth, -quantifierDepth)) + } + case None => None + } + } + + override def preVisit( + t: IExpression, + quantifierDepth: Int + ): PreVisitResult = t match { + case v: IVariableBinder => UniSubArgs(quantifierDepth + 1) + case _ => KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[Option[IFormula]] + ): Option[IFormula] = { + t match { + // write(write(...write(@h, ptr1, val1)...)) -> read(@h, ptr1) == val1 && read(@h, ptr2) == val2 && ... + // addresses must be separated and pointers valid + case IEquation( + heapFunApp @ IFunApp(function, _), + Var(h) + ) if cci.isCurrentHeap(h, quantifierDepth) => + shiftFormula( + extractEqualitiesFromWriteChain(heapFunApp, h), + quantifierDepth + ) + + // other order.. + case IEquation( + Var(h), + heapFunApp @ IFunApp(function, _) + ) if cci.isCurrentHeap(h, quantifierDepth) => + shiftFormula( + extractEqualitiesFromWriteChain(heapFunApp, h), + quantifierDepth + ) + + case _ => subres.collectFirst { case Some(h) => h } + } + } +} diff --git a/src/tricera/postprocessor/ClauseRemover.scala b/src/tricera/postprocessor/ClauseRemover.scala new file mode 100644 index 0000000..1acd4f7 --- /dev/null +++ b/src/tricera/postprocessor/ClauseRemover.scala @@ -0,0 +1,269 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* ClauseRemover.scala + * + * See ClauseRemover in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this contract processor, clauses that are not expressible in ACSL + * are removed. + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import ContractConditionType._ + +object ClauseRemover extends ContractProcessor { + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + apply(cci.contractCondition, cci).asInstanceOf[IFormula] + } + + // TODO: Use IFormula instead of IExpression? + def apply(expr: IExpression, cci: ContractConditionInfo): IExpression = { + val noTOHExpr = CleanupVisitor(TheoryOfHeapRemoverVisitor(expr, cci)) + val noTOHOrExplPtrExpr = CleanupVisitor(ExplicitPointerRemover(noTOHExpr, cci)) + val noTrivialEqExpr = CleanupVisitor(TrivialEqualityRemover(noTOHOrExplPtrExpr, cci)) + val newContractCondition = CleanupVisitor(HeapEqualityRemover(noTrivialEqExpr, cci)) + newContractCondition + } +} + +object TheoryOfHeapRemoverVisitor { + def apply(expr: IExpression, cci: ContractConditionInfo): IExpression = { + (new TheoryOfHeapRemoverVisitor(cci)).visit(expr, 0) + } +} + +class TheoryOfHeapRemoverVisitor(cci: ContractConditionInfo) + extends CollectingVisitor[Int, IExpression] { + + override def preVisit(t: IExpression, quantifierDepth: Int): PreVisitResult = + t match { + case default => + KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[IExpression] + ): IExpression = t match { + case IBinFormula(IBinJunctor.And, _, _) => + val f1 = subres(0) + val f2 = subres(1) + (ContainsTOHVisitor(f1, cci), ContainsTOHVisitor(f2, cci)) match { + case (false, false) => + t update subres + case (true, false) => + f2 + case (false, true) => + f1 + case (true, true) => + IBoolLit(true) + } + case q @ ISortedQuantified(_, _, formula) => + q update subres + case default => t update subres + } +} + +object ContainsTOHVisitor { + def apply(expr: IExpression, cci: ContractConditionInfo): Boolean = { + (new ContainsTOHVisitor(cci))(expr) + } +} + +class ContainsTOHVisitor(cci: ContractConditionInfo) + extends CollectingVisitor[Unit, Boolean] { + + def apply(expr: IExpression): Boolean = { + visit(expr, ()) + } + + override def preVisit(t: IExpression, arg: Unit): PreVisitResult = t match { + case TheoryOfHeapFunApp(_, _) => + ShortCutResult(true) + case IFunApp(fun, args) if (cci.isGetter(fun) || cci.isWrapper(fun)) => + ShortCutResult(true) + case _ => + KeepArg + } + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[Boolean] + ): Boolean = + if (subres.isEmpty) false else subres.reduce(_ || _) +} + +object ExplicitPointerRemover extends ContractProcessor { + def processContractCondition(cci: ContractConditionInfo): IFormula = { + (new ExplicitPointerRemoverVisitor(cci)).visit(cci.contractCondition, 0).asInstanceOf[IFormula] + } + + def apply(expr: IExpression, cci: ContractConditionInfo): IExpression = { + val newExpr = (new ExplicitPointerRemoverVisitor(cci)).visit(expr, 0) + CleanupVisitor(newExpr) + } +} + +class ExplicitPointerRemoverVisitor(cci: ContractConditionInfo) + extends CollectingVisitor[Int, IExpression] { + + override def preVisit(t: IExpression, quantifierDepth: Int): PreVisitResult = + t match { + case vb: IVariableBinder => + UniSubArgs(quantifierDepth + 1) + case _ => + KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[IExpression] + ): IExpression = { + t update subres match { + case f: IFormula if ContainsExplicitPointerVisitor(f, quantifierDepth, cci) => + IBoolLit(true) + case _ => + t update subres + } + } +} + +object ContainsExplicitPointerVisitor { + def apply(expr: IExpression, quantifierDepth: Int, cci: ContractConditionInfo): Boolean = { + (new ContainsExplicitPointerVisitor(cci))(expr, quantifierDepth) + } +} + +class ContainsExplicitPointerVisitor(cci: ContractConditionInfo) + extends CollectingVisitor[Int, Boolean] { + def apply(expr: IExpression, quantifierDepth: Int): Boolean = { + visit(expr, quantifierDepth) + } + + override def preVisit( + t: IExpression, + quantifierDepth: Int + ): PreVisitResult = { + t match { + case vb: IVariableBinder => + UniSubArgs(quantifierDepth + 1) + + case IEquation(v1: ISortedVariable, v2: ISortedVariable) + if cci.isPointer(v1, quantifierDepth) && cci.isPointer( + v2, + quantifierDepth + ) => + ShortCutResult(false) + case TheoryOfHeapFunApp(_, _) => + ShortCutResult(false) + case IFunApp(fun, _) if cci.isACSLFunction(fun) => + ShortCutResult(false) + case IAtom(pred, _) if cci.isACSLPredicate(pred) => + ShortCutResult(false) + case IBinFormula(IBinJunctor.And, _, _) => + ShortCutResult(false) + case _ => + KeepArg + } + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[Boolean] + ): Boolean = t match { + case v: ISortedVariable if cci.isPointer(v, quantifierDepth) => + true + case _ => + if (subres.isEmpty) false else subres.reduce(_ || _) + } +} + +object TrivialEqualityRemover { + def apply(expr: IExpression, cci: ContractConditionInfo): IExpression = { + (new TrivialEqualityRemover(cci)).visit(expr, ()) + } +} + +class TrivialEqualityRemover(cci: ContractConditionInfo) + extends CollectingVisitor[Unit, IExpression] { + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[IExpression] + ): IExpression = t match { + case IEquation(left, right) if left == right => + IBoolLit(true) + case _ => + t update subres + } +} + +object HeapEqualityRemover { + def apply(expr: IExpression, cci: ContractConditionInfo): IExpression = { + (new HeapEqualityRemover(cci)).visit(expr, 0) + } +} + +class HeapEqualityRemover(cci: ContractConditionInfo) + extends CollectingVisitor[Int, IExpression] { + + override def preVisit(t: IExpression, quantifierDepth: Int): PreVisitResult = + t match { + case vb: IVariableBinder => + UniSubArgs(quantifierDepth + 1) + case _ => + KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[IExpression] + ): IExpression = t match { + case IEquation(left: ISortedVariable, _) if cci.isCurrentHeap(left, quantifierDepth) => + IBoolLit(true) + case IEquation(_, right: ISortedVariable) if cci.isCurrentHeap(right, quantifierDepth) => + IBoolLit(true) + case _ => + t update subres + } +} diff --git a/src/tricera/postprocessor/ContractConditionTools.scala b/src/tricera/postprocessor/ContractConditionTools.scala new file mode 100644 index 0000000..3f3dd6d --- /dev/null +++ b/src/tricera/postprocessor/ContractConditionTools.scala @@ -0,0 +1,227 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + /* ContractConditionTools.scala + * + * Various tools used for processing contract conditions. + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import ap.theories.Heap +import ap.theories.Heap.HeapFunExtractor +import ap.theories.ADT +import tricera.postprocessor.ContractConditionType._ + +trait ExpressionUtils { + def iterateUntilFixedPoint( + expr: IExpression, + apply: IExpression => IExpression + ): IExpression = { + val expressions: Stream[IExpression] = Stream.iterate(expr)(apply) + expressions + .zip(expressions.tail) + .collectFirst { case (a, b) if a == b => a } + .getOrElse(expr) + } +} + +trait IdGenerator { + def generateId: String = java.util.UUID.randomUUID.toString +} + +// Indicates whether an IExpression contains a quantifier +object ContainsQuantifiedVisitor extends CollectingVisitor[Int, Boolean] { + def apply(expr: IExpression, quantifierDepth: Int): Boolean = { + ContainsQuantifiedVisitor.visit(expr, quantifierDepth) + } + + override def preVisit(t: IExpression, quantifierDepth: Int): PreVisitResult = + t match { + case v: ISortedQuantified => UniSubArgs(quantifierDepth + 1) + case ISortedVariable(index, _) => + if (index < quantifierDepth) + ShortCutResult(true) + else + ShortCutResult(false) + case _ => KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[Boolean] + ): Boolean = + if (subres.isEmpty) false else subres.reduce(_ || _) +} + +// Returns the number of free variables minus 1 +object MaxIndexVisitor extends CollectingVisitor[Unit, Int] { + def apply(expr: IExpression): Int = { + MaxIndexVisitor.visit(expr, ()) + } + + override def preVisit(t: IExpression, arg: Unit): PreVisitResult = t match { + case v: IVariable => ShortCutResult(v.index) + case _ => KeepArg + } + + override def postVisit(t: IExpression, arg: Unit, subres: Seq[Int]): Int = + if (subres.isEmpty) 0 else subres.max +} + +// Returns an IExpression where simplifications related to the literals +// true and false have been made +object CleanupVisitor extends CollectingVisitor[Unit, IExpression] { + def apply(expr: IExpression): IExpression = { + Rewriter.rewrite(expr, (t) => CleanupVisitor.visit(t, ())) + } + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[IExpression] + ): IExpression = t match { + case IBinFormula(IBinJunctor.And, f1, f2) if (f1 == IBoolLit(true)) => f2 + case IBinFormula(IBinJunctor.And, f1, f2) if (f2 == IBoolLit(true)) => f1 + case IBinFormula(IBinJunctor.And, f1, f2) + if (f1 == IBoolLit(false) || f2 == IBoolLit(false)) => + false + case IBinFormula(IBinJunctor.Or, f1, f2) if (f1 == IBoolLit(true)) => f1 + case IBinFormula(IBinJunctor.Or, f1, f2) if (f2 == IBoolLit(true)) => f2 + case IBinFormula(IBinJunctor.Or, f1, f2) if (f1 == IBoolLit(false)) => f2 + case IBinFormula(IBinJunctor.Or, f1, f2) if (f2 == IBoolLit(false)) => f1 + case ISortedQuantified(_, _, f) if (f == IBoolLit(true)) => IBoolLit(true) + case ISortedQuantified(_, _, f) if (f == IBoolLit(false)) => IBoolLit(false) + case INot(f) if (f == IBoolLit(true)) => IBoolLit(false) + case INot(f) if (f == IBoolLit(false)) => IBoolLit(true) + case _ => t + } +} + +// Returns a tuple (newExpression, replacedExpression) where n:th IFormula +// in depth-first left-first order is replaced by newFormula in +// newExpression, and replacedExpression is the expression that was +// substituted +object ReplaceNthIFormulaVisitor { + def apply( + expr: IExpression, + n: Int, + replaceByFormula: IFormula + ): (IExpression, Option[IExpression]) = { + val replaceFormulaVisitor: ReplaceNthIFormulaVisitor = + new ReplaceNthIFormulaVisitor(n, replaceByFormula) + val newFormula = replaceFormulaVisitor.visit(expr, ()) + (newFormula, replaceFormulaVisitor.getReplacedFormula) + } + + class ReplaceNthIFormulaVisitor(n: Int, replaceByFormula: IFormula) + extends CollectingVisitor[Unit, IExpression] { + private var formulaCount = 0 + private var formula: Option[IExpression] = None + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[IExpression] + ): IExpression = t match { + case f: IFormula if formulaCount == n => + formula = Some(f) + formulaCount += 1 + replaceByFormula + case f: IFormula => + formulaCount += 1 + t.update(subres) + case _ => + t.update(subres) + } + + def getReplacedFormula: Option[IExpression] = formula + } +} + +// Returns the number of IFormulas in an IExpression +object IFormulaCounterVisitor extends CollectingVisitor[Unit, Int] { + def apply(expr: IExpression): Int = { + IFormulaCounterVisitor.visit(expr, ()) + } + + override def postVisit(t: IExpression, arg: Unit, subres: Seq[Int]): Int = + t match { + case f: IFormula => subres.sum + 1 + case _ => subres.sum + } +} + +// Match types + +object Is_O_Sort { + def unapply( + expr: IExpression + ): Option[IExpression] = expr match { + case IExpression.EqLit( + IFunApp( + ADT.CtorId(_, _), + Seq(arg) + ), + _ + ) => + Some(arg) + + case _ => None + } +} + +object TheoryOfHeapFunApp { + def unapply( + expr: IExpression + ): Option[(IFunction, Seq[IExpression])] = expr match { + case IFunApp( + function @ Heap.HeapFunExtractor(_), + args + ) => + Some((function, args)) + + case _ => None + } +} + +object Var { + def unapply( + expr: IExpression + ): Option[ISortedVariable] = expr match { + case variable @ ISortedVariable(index, _) => + Some(variable) + + case _ => None + } +} diff --git a/src/tricera/postprocessor/ContractConditionType.scala b/src/tricera/postprocessor/ContractConditionType.scala new file mode 100644 index 0000000..8c4dbd3 --- /dev/null +++ b/src/tricera/postprocessor/ContractConditionType.scala @@ -0,0 +1,43 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* ContractConditionType.scala + * + * Definition of the contract condition types (precondition, postcondition and a + * union of the two). + */ + +package tricera.postprocessor + +object ContractConditionType extends Enumeration { + type ContractConditionType = Value + val Precondition, Postcondition = Value +} + +import ContractConditionType._ \ No newline at end of file diff --git a/src/tricera/postprocessor/ContractProcessorUtils.scala b/src/tricera/postprocessor/ContractProcessorUtils.scala new file mode 100644 index 0000000..a78437f --- /dev/null +++ b/src/tricera/postprocessor/ContractProcessorUtils.scala @@ -0,0 +1,283 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + /* ContractProcessorUtils.scala + * + * Defines classes for easily accessing all information regarding a contract + * condition and it's terms. Also defines traits for contract processors. + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import tricera.postprocessor.ContractConditionType._ +import ap.types.MonoSortedIFunction +import _root_.tricera.concurrency.ccreader.CCHeapPointer +import _root_.tricera.concurrency.ccreader.CCStackPointer +import _root_.tricera.concurrency.ccreader.CCHeapArrayPointer +import tricera.concurrency.ccreader.CCExceptions.TranslationException + +case class ContractInfo( + solution: SolutionProcessor.Solution, + function: String, + context: FunctionContext +) { + val prePredicate = context.prePred.pred + val postPredicate = context.postPred.pred + val precondition = solution(prePredicate) + val postcondition = solution(postPredicate) + val acslContext = context.acslContext + val prePredACSLArgNames = context.prePredACSLArgNames + val postPredACSLArgNames = context.postPredACSLArgNames + val paramNames = acslContext.getParams.map(x => x.name) + val heapTheory = if (!acslContext.isHeapEnabled) { + throw new TranslationException( + "Heap solution processor called with no heap.") + } else acslContext.getHeap + val selectors = acslContext.getStructMap.values + .map((struct) => struct.sels.map(_._1)) + .toSet + .flatten + + def getContractConditionType( + predicate: Predicate + ): ContractConditionType = predicate match { + case context.prePred.pred => + ContractConditionType.Precondition + case context.postPred.pred => + ContractConditionType.Postcondition + } + + def toContractConditionInfo(predicate: Predicate): ContractConditionInfo = { + ContractConditionInfo(predicate, this) + } +} + +case class ContractConditionInfo(predicate: Predicate, ci: ContractInfo) { + val prePredicate = ci.prePredicate + val postPredicate = ci.postPredicate + val precondition = ci.precondition + val postcondition = ci.postcondition + val acslContext = ci.acslContext + val prePredACSLArgNames = ci.prePredACSLArgNames + val postPredACSLArgNames = ci.postPredACSLArgNames + val paramNames = ci.paramNames + val heapTheory = ci.heapTheory + val selectors = ci.selectors + + val contractConditionType = ci.getContractConditionType(predicate) + val contractCondition: IFormula = contractConditionType match { + case ContractConditionType.Precondition => + ci.precondition + case ContractConditionType.Postcondition => + ci.postcondition + } + val acslArgNames = contractConditionType match { + case Precondition => + ci.prePredACSLArgNames + case Postcondition => + ci.postPredACSLArgNames + } + + def getVarName( + variable: ISortedVariable, + quantifierDepth: Int + ): Option[String] = { + acslArgNames.lift(variable.index - quantifierDepth) + } + + def isSelector( + function: IFunction + ): Boolean = { + function match { + case monoFun: MonoSortedIFunction => + selectors.contains(monoFun) + case _: IFunction => false + } + } + + def isWriteFun(function: IFunction): Boolean = function == heapTheory.write + + def isReadFun(function: IFunction): Boolean = function == heapTheory.read + + def isAllocFun(function: IFunction): Boolean = function == heapTheory.alloc + + def isNewHeapFun(function: IFunction): Boolean = + function == heapTheory.newHeap + + def isNewAddrFun(function: IFunction): Boolean = + function == heapTheory.newAddr + + def isGetter(function: IFunction): Boolean = + acslContext.getterSort(function).isDefined + + def isWrapper(function: IFunction): Boolean = + acslContext.wrapperSort(function).isDefined + + def isStructCtor(fun: MonoSortedIFunction): Boolean = { + acslContext.getStructMap.get(fun).isDefined + } + + def isACSLFunction(fun: IFunction): Boolean = { + ACSLExpression.functions.contains(fun) + } + def isACSLPredicate(pred: Predicate): Boolean = { + ACSLExpression.predicates.contains(pred) + } + + def isPrecondition: Boolean = { + contractConditionType == Precondition + } + + def isPostcondition: Boolean = { + contractConditionType == Postcondition + } + + def isParam( + variable: ISortedVariable, + quantifierDepth: Int + ): Boolean = { + getVarName(variable, quantifierDepth).exists(varName => + paramNames.contains(stripOld(varName)) + ) + } + + def isOldVar( + variable: ISortedVariable, + quantifierDepth: Int + ): Boolean = { + getVarName(variable, quantifierDepth).exists(varName => + varName.startsWith("\\old") + ) + } + + def isOldHeap( + variable: ISortedVariable, + quantifierDepth: Int + ): Boolean = { + getVarName(variable, quantifierDepth).exists(_ == "\\old(@h)") + } + + def isCurrentHeap( + variable: ISortedVariable, + quantifierDepth: Int + ): Boolean = { + getVarName(variable, quantifierDepth).exists(_ == "@h") + } + + def isPointer(variable: ISortedVariable, quantifierDepth: Int): Boolean = { + getPureVarName(variable, quantifierDepth) match { + case Some(varName) => + val ccVar = acslContext.getParams + .find(_.name == varName) + .orElse(acslContext.getGlobals.find(_.name == varName)) + + ccVar.flatMap(ccVariable => Some(ccVariable.typ)) match { + case Some(_: CCHeapPointer) => true + case Some(_: CCStackPointer) => true + case Some(_: CCHeapArrayPointer) => true + case _ => false + } + case None => false + } + } + + def getPureVarName( + variable: ISortedVariable, + quantifierDepth: Int + ): Option[String] = { + getVarName(variable, quantifierDepth) match { + case Some(varName) => Some(stripOld(varName)) + case None => None + } + } + + def stripOld(input: String): String = { + val prefix = "\\old(" + val suffix = ")" + + if (input.startsWith(prefix) && input.endsWith(suffix)) { + input.substring(prefix.length, input.length - suffix.length) + } else { + input + } + } + + def getGetter(heapTerm: ITerm): Option[IFunction] = { + heapTerm match { + case IFunApp(wrapper, _) => + acslContext.wrapperSort(wrapper).flatMap(acslContext.sortGetter) + case _ => None + } + } +} + +trait ClauseCreator { + def getClauses(expr: IExpression, cci: ContractConditionInfo): Option[IFormula] +} + +trait ContractProcessor { + def apply( + solution: SolutionProcessor.Solution, + function: String, + context: FunctionContext + ): (IFormula, IFormula) = { + val contractInfo = ContractInfo(solution, function, context) + val preconditionInfo = + contractInfo.toContractConditionInfo(context.prePred.pred) + val postconditionInfo = + contractInfo.toContractConditionInfo(context.postPred.pred) + ( + processContractCondition(preconditionInfo), + processContractCondition(postconditionInfo) + ): ( + IFormula, + IFormula + ) + } + + /** This is the function that should be implemented in new + * ContractConditionProcessors + * @param solution + * : All predicates in solution + * @param predicate + * : Predicate to process + * @param function + * : function name + * @param context + * : function context + * @return + * : processed IExpression + */ + def processContractCondition( + contractConditionInfo: ContractConditionInfo + ): IFormula +} diff --git a/src/tricera/postprocessor/EqualitySwapper.scala b/src/tricera/postprocessor/EqualitySwapper.scala new file mode 100644 index 0000000..7ac190e --- /dev/null +++ b/src/tricera/postprocessor/EqualitySwapper.scala @@ -0,0 +1,149 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + /* EqualitySwapper.scala + * + * Defines objects and classes for converting expressions to equivalent + * representations. The ToVariableForm processor is defined here. + * + * See ToVariableForm in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import tricera.postprocessor.ContractConditionType._ + +object ToVariableForm extends ContractProcessor { + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + val valueSet = cci.contractConditionType match { + case Precondition => + ValSetReader.deBrujin(cci.precondition) + case Postcondition => + ValSet.merge( + ValSetReader.deBrujin(cci.precondition), + ValSetReader.deBrujin(cci.postcondition) + ) + } + EqualitySwapper.deBrujin(cci.contractCondition, valueSet.toVariableFormMap, cci).asInstanceOf[IFormula] + } +} + +object ToExplicitForm { + def deBrujin(expr: IExpression, valueSet: ValSet, cci: ContractConditionInfo) = { + EqualitySwapper.deBrujin(expr, valueSet.toExplicitFormMap, cci) + } + + def invariant(expr: IExpression, valueSet: ValSet, cci: ContractConditionInfo) = { + EqualitySwapper.invariant(expr, valueSet.toExplicitFormMap, cci) + } +} + +object EqualitySwapper { + def deBrujin(expr: IExpression, swapMap: Map[IExpression, ITerm], cci: ContractConditionInfo) = { + (new EqualitySwapper(swapMap, cci))(expr) + } + + def invariant(expr: IExpression, swapMap: Map[IExpression, ITerm], cci: ContractConditionInfo) = { + (new InvariantEqualitySwapper(swapMap, cci))(expr) + } +} + +class EqualitySwapper(swapMap: Map[IExpression, ITerm], cci: ContractConditionInfo) + extends CollectingVisitor[Int, IExpression] + with ExpressionUtils { + + // swaps every expression except equalities but including the @h expression + def apply(contractCondition: IExpression): IExpression = { + def rewriter(expr: IExpression): IExpression = { + visit(expr, 0) + } + iterateUntilFixedPoint(contractCondition, rewriter) + } + + override def preVisit( + t: IExpression, + quantifierDepth: Int + ): PreVisitResult = t match { + case IEquation(v: ISortedVariable, term) if !cci.isCurrentHeap(v, quantifierDepth) => + ShortCutResult(t) + case IEquation(term, v: ISortedVariable) if !cci.isCurrentHeap(v, quantifierDepth) => + ShortCutResult(t) + case IIntFormula(IIntRelation.EqZero, term) => + ShortCutResult(t) + case vb: IVariableBinder => + UniSubArgs(quantifierDepth + 1) + case _ => + KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[IExpression] + ): IExpression = t match { + case h: ISortedVariable if cci.isCurrentHeap(h, quantifierDepth) => + t update subres + case term: ITerm => + val res = t update subres + val shiftedTerm = + VariableShiftVisitor(term, quantifierDepth, -quantifierDepth) + swapMap.get(shiftedTerm) match { + case Some(variable) => + val newVariable = + VariableShiftVisitor(variable, 0, quantifierDepth) + newVariable + case None => + res + } + case default => t update subres + } +} + +class InvariantEqualitySwapper(swapMap: Map[IExpression, ITerm], cci: ContractConditionInfo) extends EqualitySwapper(swapMap, cci) { + + override def preVisit( + t: IExpression, + quantifierDepth: Int + ): PreVisitResult = t match { + case IEquation(v: ISortedVariable, term) if !cci.isCurrentHeap(v, quantifierDepth) => + ShortCutResult(t) + case IEquation(term, v: ISortedVariable) if !cci.isCurrentHeap(v, quantifierDepth) => + ShortCutResult(t) + case IIntFormula(IIntRelation.EqZero, term) => + ShortCutResult(t) + case _ => + KeepArg + } +} diff --git a/src/tricera/postprocessor/HeapRepresentation.scala b/src/tricera/postprocessor/HeapRepresentation.scala new file mode 100644 index 0000000..6f9aca3 --- /dev/null +++ b/src/tricera/postprocessor/HeapRepresentation.scala @@ -0,0 +1,112 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + /* HeapRepresentation.scala + * + * Definitions related to a "heap simulator" which can translate theory + * of heap expressions to a map containing relevant information. This is + * used by PointerPropProcessor. + */ + +package tricera.postprocessor + +import ap.parser._ + +case class Address(addressSpaceId: String, counter: Int) extends ITerm { + override def toString = { + "Addr" + List("ID" + addressSpaceId.take(4), counter).mkString("(", ",", ")") + } +} + +object HeapState { + def emptyStorage = Map.empty[Address, ITerm] + + def empty = HeapState("empty", -1, emptyStorage) + + def heapById(id: String) = HeapState(id, -1, Map.empty[Address, ITerm]) + +} + +case class AllocRes(newHeap: HeapState, newAddr: Address) extends ITerm + +case class HeapState( + addressSpaceId: String, + counter: Int, + storage: Map[Address, ITerm] +) extends ITerm { + // addresses <= counter are allocated + + def alloc(obj: ITerm): AllocRes = { + val allocationAddress = Address(addressSpaceId, counter + 1) + AllocRes( + HeapState(addressSpaceId, counter + 1, storage + (allocationAddress -> obj)), + allocationAddress + ) + } + + def write( + addr: Address, + obj: ITerm + ): HeapState = { + if (addressSpaceId == addr.addressSpaceId) { + writeToAddressSpace(addr, obj) + } else { + HeapState(addressSpaceId, counter, HeapState.emptyStorage) + } + } + + private def writeToAddressSpace(addr: Address, obj: ITerm): HeapState = { + if (addr.counter <= counter) { + val newStorage = this.havocPossibleUnknownAliases(addr).storage + (addr -> obj) + HeapState(addressSpaceId, counter, newStorage) + } else { + this + } + } + + def read( + addr: Address + ): ITerm = { + storage.get(addr) match { + case Some(x) => x + case None => this + } + } + + private def havocPossibleUnknownAliases(addr: Address): HeapState = { + val keysToHavoc = storage.keys.filterNot(_.addressSpaceId == addr.addressSpaceId) + val newStorage = storage -- (keysToHavoc) + HeapState(addressSpaceId, counter, newStorage) + } + + override def toString = { + "Heap" + List("ID" + addressSpaceId.take(4), counter, storage) + .mkString("(", ",", ")") + } +} \ No newline at end of file diff --git a/src/tricera/postprocessor/PointerPropProcessor.scala b/src/tricera/postprocessor/PointerPropProcessor.scala new file mode 100644 index 0000000..7e1045b --- /dev/null +++ b/src/tricera/postprocessor/PointerPropProcessor.scala @@ -0,0 +1,205 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* PointerPropProcessor.scala + * + * See PointerPropExtractor in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this contract processor, any separation and validity clauses that can be + * deduced are extracted. This can only be done whenever the heap state is + * expressed. + */ + +package tricera.postprocessor + +import ap.parser._ +import scala.collection.immutable.Stack + +object PointerPropProcessor extends ContractProcessor with ClauseCreator { + def processContractCondition(cci: ContractConditionInfo) = { + getSafePointers(cci.contractCondition, cci) match { + case safePointers if safePointers.size >= 2 => + cci.contractCondition + .&(ACSLExpression.separatedPointers(safePointers, 0, cci)) + .&(ACSLExpression.validPointers(safePointers, 0, cci)) + case _ => + cci.contractCondition + } + } + + def getClauses(expr: IExpression, cci: ContractConditionInfo): Option[IFormula] = { + getSafePointers(expr, cci) match { + case safePointers if safePointers.size >= 2 => + Some(ACSLExpression.separatedPointers(safePointers, 0, cci) + .&(ACSLExpression.validPointers(safePointers, 0, cci))) + case safePointers if safePointers.size == 1 => + Some(ACSLExpression.validPointers(safePointers, 0, cci)) + case _ => + None + } + } + + def getSafePointers(expr: IExpression, cci: ContractConditionInfo): Set[ISortedVariable] = { + val invForm = ToInvariantFormVisitor(expr) + val valueSet = ValSetReader.invariant(invForm) + val explForm = ToExplicitForm.invariant(invForm, valueSet, cci) + val redForm = HeapReducer(explForm, cci) + HeapExtractor(redForm, cci) match { + case Some(heap) => + val redValueSet = ValSetReader.invariant(redForm) + readSafeVariables(heap, redValueSet) + case _ => Set.empty[ISortedVariable] + } + } + + def readSafeVariables( + heap: HeapState, + valueSetWithAddresses: ValSet + ): Set[ISortedVariable] = { + heap.storage.keys + .flatMap(valueSetWithAddresses.getVariableForm(_)) + .asInstanceOf[Set[ISortedVariable]] + } +} + +object HeapExtractor { + def apply( + expr: IExpression, + cci: ContractConditionInfo + ): Option[HeapState] = { + (new InvariantHeapExtractor(cci)).visit(expr, ()) + } +} + +class InvariantHeapExtractor(cci: ContractConditionInfo) + extends CollectingVisitor[Unit, Option[HeapState]] { + override def preVisit(t: IExpression, arg: Unit): PreVisitResult = t match { + case IEquation(h: ISortedVariable, heap: HeapState) if cci.isCurrentHeap(h, 0) => + ShortCutResult(Some(heap)) + case _ => + KeepArg + } + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[Option[HeapState]] + ): Option[HeapState] = t match { + case h: HeapState => Some(h) + case _ => subres.collectFirst { case Some(h) => h } + } +} + +object HeapReducer { + def apply( + invariantExpression: IExpression, + cci: ContractConditionInfo + ): IExpression = { + (new HeapReducer(cci)).visit(invariantExpression, Stack[String]()) + } +} + +class HeapReducer(cci: ContractConditionInfo) + extends CollectingVisitor[Stack[String], IExpression] { + + override def postVisit( + t: IExpression, + quantifierIds: Stack[String], + subres: Seq[IExpression] + ): IExpression = { + t update subres match { + case IFunApp(fun, args) if (fun.name == "emptyHeap" && args.isEmpty) => + HeapState.empty + case QuantifiedVarWithId(ISortedVariable(_, sort), id) + if sort.name == "Heap" => + HeapState.heapById(id) + case TheoryOfHeapFunApp( + writeFun, + Seq(heap: HeapState, addr: Address, obj) + ) if cci.isWriteFun(writeFun) => + heap.write(addr, obj.asInstanceOf[ITerm]) + case TheoryOfHeapFunApp( + readFun, + Seq(heap: HeapState, addr: Address) + ) if cci.isReadFun(readFun) => + heap.read(addr) + case TheoryOfHeapFunApp( + allocFun, + Seq(heap: HeapState, obj) + ) if cci.isAllocFun(allocFun) => + heap.alloc(obj.asInstanceOf[ITerm]) + case TheoryOfHeapFunApp(newHeapFun, Seq(allocRes: AllocRes)) + if cci.isNewHeapFun(newHeapFun) => + allocRes.newHeap + case TheoryOfHeapFunApp(newAddrFun, Seq(allocRes: AllocRes)) + if cci.isNewAddrFun(newAddrFun) => + allocRes.newAddr + case _ => t update subres + } + } +} + +case class QuantifiedVarWithId(variable: ISortedVariable, id: String) + extends ITerm { + override def toString = { + variable.toString + "(Q" + id.take(4) + ")" + } +} + +object ToInvariantFormVisitor + extends CollectingVisitor[Stack[String], IExpression] + with IdGenerator { + + def apply(contractCondition: IExpression): IExpression = { + visit(contractCondition, Stack[String]()) + } + + override def preVisit( + t: IExpression, + quantifierIds: Stack[String] + ): PreVisitResult = t match { + case v: IVariableBinder => UniSubArgs(quantifierIds.push(generateId)) + case _ => KeepArg + } + + override def postVisit( + t: IExpression, + quantifierIds: Stack[String], + subres: Seq[IExpression] + ): IExpression = t match { + case v @ ISortedVariable(index, sort) => + if (index < quantifierIds.size) { // quantified variable + QuantifiedVarWithId(v, quantifierIds(index)) + } else { + ISortedVariable(index - quantifierIds.size, sort) + } + case _ => t update (subres) + } +} diff --git a/src/tricera/postprocessor/PostconditionSimplifier.scala b/src/tricera/postprocessor/PostconditionSimplifier.scala new file mode 100644 index 0000000..a3793b4 --- /dev/null +++ b/src/tricera/postprocessor/PostconditionSimplifier.scala @@ -0,0 +1,145 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* PostconditionSimplifier.scala + * + * See PostconditionSimplifier in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this contract processor, attempts are made to simplify the postcondition by + * using the information in the precondition. This is done as the simplified + * postcondition may contain more clauses that are directly expressible in ACSL. + * The precondition is left unchanged. + */ + +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import ap.SimpleAPI.ProverStatus +import ap.SimpleAPI.TimeoutException +import ap.theories._ +import ap.SimpleAPI + +object PostconditionSimplifier extends ContractProcessor { + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + cci.contractConditionType match { + case ContractConditionType.Precondition => + cci.contractCondition + case ContractConditionType.Postcondition => + apply(cci.precondition, cci.postcondition) + } + } + + def apply(precondition: IFormula, postcond: IFormula): IFormula = { + var postcondition = postcond + + def attemptReplacingIFormulasBy(replaceByFormula: IFormula) = { + var i = 0 + var cont = true + while (cont) { + ReplaceNthIFormulaVisitor(postcondition, i, replaceByFormula) match { + case (newPostcondition, Some(replacedFormula)) => + isEquivalentPostcondition( + precondition, + postcondition, + newPostcondition.asInstanceOf[IFormula] + ) match { + case true => + postcondition = newPostcondition.asInstanceOf[IFormula] + val removedIFormulas = + IFormulaCounterVisitor(replacedFormula) - 1 + i = i + 1 - removedIFormulas + case false => + i = i + 1 + } + case (_, None) => + cont = false + } + } + // Note: Cleanup rules for false literals are not yet implemented in CleanupVisitor + postcondition = CleanupVisitor(postcondition).asInstanceOf[IFormula] + } + attemptReplacingIFormulasBy(IBoolLit(true)) + attemptReplacingIFormulasBy(IBoolLit(false)) + postcondition + } + + def replaceVarsWithConstants(p: SimpleAPI, formula: IFormula): IFormula = { + val maxIndex = MaxIndexVisitor(formula) + val constants = p.createConstants("c", 0 to maxIndex).toList + VariableSubstVisitor(formula.asInstanceOf[IFormula], (constants, 0)) + } + + def collectAndAddTheories(p: SimpleAPI, formula: IFormula) = { + val theories: Seq[Theory] = { + val coll = new TheoryCollector + coll(formula) + coll.theories + } + p.addTheories(theories) + } + + def isEquivalentPostcondition( + precondition: IFormula, + postcondition: IFormula, + simplifiedPostcondition: IFormula + ): Boolean = { + SimpleAPI.withProver { p => + val formula = + precondition + .==>(postcondition.<=>(simplifiedPostcondition)) + .asInstanceOf[IFormula] + val constFormula = replaceVarsWithConstants(p, formula) + collectAndAddTheories(p, formula) + + p.??(constFormula) + + val result = + try + p.withTimeout(100) { + p.??? + } + catch { + case x: SimpleAPI.SimpleAPIException if x == TimeoutException => + None + } + + result match { + case ProverStatus.Valid => + true + case _ => + false + } + } + } +} diff --git a/src/tricera/postprocessor/TheoryOfHeapProcessor.scala b/src/tricera/postprocessor/TheoryOfHeapProcessor.scala new file mode 100644 index 0000000..43355e7 --- /dev/null +++ b/src/tricera/postprocessor/TheoryOfHeapProcessor.scala @@ -0,0 +1,106 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* TheoryOfHeapProcessor.scala + * + * See TOHProcessor in "Automated Inference of ACSL Contracts for + * Programs with Heaps" by Oskar Söderberg + * + * In this contract processor, theory of heap expressions are reduced to a simpler form + * containing fewer subexpressions, which can be handled by the ADTSimplifier, + * ADTExploder and ACSLExpressionProcessor. + */ + +package tricera.postprocessor + +import ap.parser._ +import ap.theories.ADT +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import ap.theories.Heap +import ap.theories.Heap.HeapFunExtractor +import ContractConditionType._ +import tricera.acsl.ACSLTranslator.{FunctionContext => ACSLFunctionContext} +import ap.types.Sort + +object TheoryOfHeapProcessor + extends ContractProcessor { + def processContractCondition( + cci: ContractConditionInfo + ): IFormula = { + TheoryOfHeapRewriter(cci).asInstanceOf[IFormula] + } + + object TheoryOfHeapRewriter extends ExpressionUtils { + def apply(cci: ContractConditionInfo): IExpression = { + val theoryOfHeapRewriter = new TheoryOfHeapRewriter(cci) + iterateUntilFixedPoint(cci.contractCondition, theoryOfHeapRewriter.apply) + } + } + + class TheoryOfHeapRewriter( + cci: ContractConditionInfo + ) extends CollectingVisitor[Unit, IExpression] { + + def apply(contractCondition: IExpression): IExpression = { + visit(contractCondition, ()) + } + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[IExpression] + ): IExpression = t match { + + // o.get.O_ -> o + case IFunApp(wrapper, Seq(IFunApp(getter, Seq(obj)))) + if (cci.isWrapper(wrapper) + && cci.isGetter(getter)) => + obj + + // o.O_.get -> o + case IFunApp(getter, Seq(IFunApp(wrapper, Seq(obj)))) + if (cci.isWrapper(wrapper) + && cci.isGetter(getter)) => + obj + + // read(write(h,p,o),p) -> o + case TheoryOfHeapFunApp( + readFun, + Seq(TheoryOfHeapFunApp(writeFun, Seq(Var(h), p2, o)), p1) + ) + if (cci.isReadFun(readFun) + && cci.isWriteFun(writeFun) + && p1 == p2) => + o + + case _ => t update subres + } + } +} diff --git a/src/tricera/postprocessor/ValSet.scala b/src/tricera/postprocessor/ValSet.scala new file mode 100644 index 0000000..de9afb7 --- /dev/null +++ b/src/tricera/postprocessor/ValSet.scala @@ -0,0 +1,317 @@ +/** + * Copyright (c) 2023 Oskar Soederberg. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* ValSet.scala + * + * Defines objects and classes for treating equivalences. A Val represents a + * Set[ITerm] where the ITerms are equivalent. A ValSet is a Set[Vals], allowing to + * add new equivalences. ValSet keeps the number of Vals as low as possible, merging + * any two Vals whenever they turn out to be equal. + */ +package tricera.postprocessor + +import ap.parser._ +import IExpression.Predicate +import tricera.concurrency.CCReader.FunctionContext +import ap.theories.ADT + +object Val { + def apply(term1: ITerm, term2: ITerm): Val = { + Val(Set(term1, term2)) + } + + def merge(vals: Set[Val]): Val = { + vals.reduce((val1, val2) => (val1 | val2)) + } +} +case class Val(variants: Set[ITerm]) { + def getExplicitForm: Option[ITerm] = variants find { + case a: Address => false + case v: ISortedVariable => false + case _ => true + } + + def getAddrForm: Option[ITerm] = variants find { + case a: Address => true + case _ => false + } + + def getVariableForm: Option[ITerm] = variants find { + case v: ISortedVariable => true + case _ => false + } + + def +(term: ITerm): Val = { + Val(variants + term) + } + + def +(v: Val): Val = { + Val.merge(Set(this, v)) + } + + def &(v: Val): Val = { + Val(variants & v.variants) + } + + def |(v: Val): Val = { + Val(variants | v.variants) + } + + def nonEmpty: Boolean = { + variants.nonEmpty + } + + def equalsTerm(term: ITerm): Boolean = { + variants.contains(term) + } + + def equalsOneOf(terms: Set[ITerm]): Boolean = { + (variants & terms).nonEmpty + } +} + +object ValSet { + + def apply(term1: ITerm, term2: ITerm): ValSet = { + ValSet(Set(Val(term1, term2))) + } + + def empty(): ValSet = { + ValSet(Set.empty[Val]) + } + + def merge(vs1: ValSet, vs2: ValSet): ValSet = { + (vs1.isEmpty, vs2.isEmpty) match { + case (true, _) => vs2 + case (_, true) => vs1 + case _ => + (vs1.vals ++ vs2.vals).foldLeft( + ValSet.empty + )((vs, v) => { + val (equalVals, rest) = vs.vals.partition(_ & v nonEmpty) + val newVal: Val = if (equalVals.nonEmpty) { + Val.merge(equalVals + v) + } else { + v + } + ValSet(rest + (newVal)) + }) + } + } +} + +case class ValSet(vals: Set[Val]) { + + def addEquality(term1: ITerm, term2: ITerm): ValSet = { + val maybeVal1 = getVal(term1) + val maybeVal2 = getVal(term2) + (maybeVal1, maybeVal2) match { + case (Some(val1), Some(val2)) => + ValSet(vals.-(val1).-(val2).+(val1 + val2)) + case (Some(v), None) => + ValSet(vals.-(v).+(v.+(term2))) + case (None, Some(v)) => + ValSet(vals.-(v).+(v.+(term1))) + case (None, None) => + ValSet(vals.+(Val(term1, term2))) + } + } + + def isEmpty = vals.isEmpty + + def areEqual(term1: ITerm, term2: ITerm): Boolean = { + getVal(term1) match { + case Some(v) => v.equalsTerm(term2) + case None => term1 == term2 + } + } + + def getVal(term: ITerm): Option[Val] = { + vals.find { + case v: Val if v.variants.contains(term) => true + case _ => false + } + } + + def getExplicitForm(term: ITerm): Option[ITerm] = { + getVal(term) match { + case Some(v) => v.getExplicitForm + case None => None + } + } + + def getVariableForm(term: ITerm): Option[ITerm] = { + getVal(term) match { + case Some(v) => v.getVariableForm + case None => None + } + } + + def toVariableFormMap: Map[IExpression, ISortedVariable] = { + vals + .collect { + case value if value.getVariableForm.isDefined => + val variable = value.getVariableForm.get.asInstanceOf[ISortedVariable] + value.variants + .filterNot(_ == variable) + .map(_ -> variable) + } + .flatten + .toMap + } + + def toExplicitFormMap: Map[IExpression, ITerm] = { + vals + .collect { + case value if value.getExplicitForm.isDefined => + val variable = value.getExplicitForm.get + value.variants + .filterNot(_ == variable) + .map(_ -> variable) + } + .flatten + .toMap + } + + def merge(eqs: ValSet): ValSet = { + ValSet.merge(this, eqs) + } + + override def toString = { + val setsStrings = vals.map { v => + v.variants.mkString("{", " :: ", "}") + } + setsStrings.mkString("", ", \n", "") + } +} + +object ValSetReader { + // NOTE: expressions must be invariant and unique (not de Bruijn indexed) + def invariant(contractCondition: IExpression): ValSet = { + InvariantReader.visit(contractCondition, ()) + } + + def deBrujin(contractCondition: IExpression): ValSet = { + DeBrujinReader.visit(contractCondition, 0) + } + + object InvariantReader + extends CollectingVisitor[Unit, ValSet] + with ExpressionUtils { + + override def postVisit( + t: IExpression, + arg: Unit, + subres: Seq[ValSet] + ): ValSet = { + def returnDefault = subres.size match { + case 0 => ValSet.empty + case _ => subres.reduce(ValSet.merge(_, _)) + } + + t match { + // skip is_O_ + case IExpression.EqLit(IFunApp(ADT.CtorId(_, _), Seq(_)), _) => + returnDefault + + case e @ IEquation(term1, term2) => + (subres :+ ValSet(term1, term2)).reduce( + ValSet.merge(_, _) + ) + + case e @ IIntFormula(IIntRelation.EqZero, term) => + (subres :+ ValSet(0, term)).reduce( + ValSet.merge(_, _) + ) + + case default => + returnDefault + } + } + } + + // skips all quantified variables (as they don't 'exist' outside formula) + object DeBrujinReader + extends CollectingVisitor[Int, ValSet] + with ExpressionUtils { + + override def preVisit( + t: IExpression, + quantifierDepth: Int + ): PreVisitResult = t match { + case IBinFormula(IBinJunctor.Or, _, _) => + ShortCutResult(ValSet.empty()) + case vb: IVariableBinder => + UniSubArgs(quantifierDepth + 1) + case _ => + KeepArg + } + + override def postVisit( + t: IExpression, + quantifierDepth: Int, + subres: Seq[ValSet] + ): ValSet = { + def returnDefault = subres.size match { + case 0 => ValSet.empty + case _ => subres.reduce(ValSet.merge(_, _)) + } + + def shiftTerm(term: ITerm, quantifierDepth: Int): ITerm = { + VariableShiftVisitor(term, quantifierDepth, -quantifierDepth) + } + + t match { + // skip is_O_ + case IExpression.EqLit(IFunApp(ADT.CtorId(_, _), Seq(_)), _) => + returnDefault + + case e @ IEquation(term1, term2) + if !ContainsQuantifiedVisitor(term1, quantifierDepth) + && !ContainsQuantifiedVisitor(term2, quantifierDepth) => + val shiftedTerm1 = shiftTerm(term1, quantifierDepth) + val shiftedTerm2 = shiftTerm(term2, quantifierDepth) + (subres :+ ValSet(shiftedTerm1, shiftedTerm2)).reduce( + ValSet.merge(_, _) + ) + + case e @ IIntFormula(IIntRelation.EqZero, term) + if !ContainsQuantifiedVisitor(term, quantifierDepth) => + val shiftedTerm = shiftTerm(term, quantifierDepth) + (subres :+ ValSet(0, shiftedTerm)).reduce( + ValSet.merge(_, _) + ) + + case default => + returnDefault + } + } + + } +}