diff --git a/build.sbt b/build.sbt index 774b42ac..b662c9ee 100644 --- a/build.sbt +++ b/build.sbt @@ -125,7 +125,9 @@ settings( nativeImageOptions ++= Seq( "--no-fallback", "-H:+ReportExceptionStackTraces", - "--allow-incomplete-classpath" + "--allow-incomplete-classpath", + "-H:IncludeResources=tricera/headers/.*", + "-H:IncludeResources=tricera/heap/encodings/.*" ), nativeImageAgentMerge := true diff --git a/cc-parser/cc-parser.jar b/cc-parser/cc-parser.jar index 1e9c7436..eef4d4a5 100644 Binary files a/cc-parser/cc-parser.jar and b/cc-parser/cc-parser.jar differ diff --git a/regression-tests/horn-hcc-heap/inv-compare-zero-bug.c b/regression-tests/horn-hcc-heap/inv-compare-zero-bug.c new file mode 100644 index 00000000..dc7c80e9 --- /dev/null +++ b/regression-tests/horn-hcc-heap/inv-compare-zero-bug.c @@ -0,0 +1,13 @@ +struct Node +{ + struct Node* next; + int data; +}; + +void main() +{ + struct Node* head = calloc(sizeof(struct Node)); + assert(0 == head->next); + // This was failing when evaluating the RHS was adding clauses. + // E.g., when using the invariant encoding. +} \ No newline at end of file diff --git a/src/main/resources/META-INF/native-image/uuverifiers/tricera/reflect-config.json b/src/main/resources/META-INF/native-image/uuverifiers/tricera/reflect-config.json index b1e5dcc7..7de02bac 100644 --- a/src/main/resources/META-INF/native-image/uuverifiers/tricera/reflect-config.json +++ b/src/main/resources/META-INF/native-image/uuverifiers/tricera/reflect-config.json @@ -1,4 +1,49 @@ [ + { + "name": "tricera.concurrency.heap.InvariantEncodingParser$Declaration", + "allDeclaredFields": true, + "allPublicFields": true, + "allDeclaredMethods": true, + "allPublicMethods": true, + "allDeclaredConstructors": true, + "allPublicConstructors": true + }, + { + "name": "tricera.concurrency.heap.InvariantEncodingParser$Argument", + "allDeclaredFields": true, + "allPublicFields": true, + "allDeclaredMethods": true, + "allPublicMethods": true, + "allDeclaredConstructors": true, + "allPublicConstructors": true + }, + { + "name": "tricera.concurrency.heap.InvariantEncodingParser$Predicate", + "allDeclaredFields": true, + "allPublicFields": true, + "allDeclaredMethods": true, + "allPublicMethods": true, + "allDeclaredConstructors": true, + "allPublicConstructors": true + }, + { + "name": "tricera.concurrency.heap.InvariantEncodingParser$FunctionDef", + "allDeclaredFields": true, + "allPublicFields": true, + "allDeclaredMethods": true, + "allPublicMethods": true, + "allDeclaredConstructors": true, + "allPublicConstructors": true + }, + { + "name": "tricera.concurrency.heap.InvariantEncodingParser$ParsedEncoding", + "allDeclaredFields": true, + "allPublicFields": true, + "allDeclaredMethods": true, + "allPublicMethods": true, + "allDeclaredConstructors": true, + "allPublicConstructors": true + }, { "name": "ap.parser.IAtom[]" }, diff --git a/src/main/resources/tricera/headers/macros_ilp32.h b/src/main/resources/tricera/headers/macros_ilp32.h new file mode 100644 index 00000000..782f3776 --- /dev/null +++ b/src/main/resources/tricera/headers/macros_ilp32.h @@ -0,0 +1,42 @@ +#ifndef MACROS_ILP32_H +#define MACROS_ILP32_H + +#define CHAR_BIT 8 + +#define SCHAR_MIN (-128) +#define SCHAR_MAX 127 +#define UCHAR_MAX 255 + +#define SHRT_MIN (-32768) +#define SHRT_MAX 32767 +#define USHRT_MAX 65535 + +#define INT_MIN (-2147483648) +#define INT_MAX 2147483647 +#define UINT_MAX 4294967295U + +#define LONG_MIN (-2147483648L) +#define LONG_MAX 2147483647L +#define ULONG_MAX 4294967295UL + +#define LLONG_MIN (-9223372036854775808LL) +#define LLONG_MAX 9223372036854775807LL +#define ULLONG_MAX 18446744073709551615ULL + +#define SIZE_MAX 4294967295U + +typedef unsigned int size_t; +typedef int ptrdiff_t; + +#define NULL 0 +#define EXIT_SUCCESS 0 +#define EXIT_FAILURE 1 + +#ifndef __bool_true_false_are_defined +#define __bool_true_false_are_defined 1 +#define bool _Bool +#define true 1 +#define false 0 +#endif /* __bool_true_false_are_defined */ + +#endif \ No newline at end of file diff --git a/src/main/resources/tricera/headers/macros_llp64.h b/src/main/resources/tricera/headers/macros_llp64.h new file mode 100644 index 00000000..ae93f0a1 --- /dev/null +++ b/src/main/resources/tricera/headers/macros_llp64.h @@ -0,0 +1,42 @@ +#ifndef MACROS_LLP64_H +#define MACROS_LLP64_H + +#define CHAR_BIT 8 + +#define SCHAR_MIN (-128) +#define SCHAR_MAX 127 +#define UCHAR_MAX 255 + +#define SHRT_MIN (-32768) +#define SHRT_MAX 32767 +#define USHRT_MAX 65535 + +#define INT_MIN (-2147483648) +#define INT_MAX 2147483647 +#define UINT_MAX 4294967295U + +#define LONG_MIN (-2147483648L) +#define LONG_MAX 2147483647L +#define ULONG_MAX 4294967295UL + +#define LLONG_MIN (-9223372036854775808LL) +#define LLONG_MAX 9223372036854775807LL +#define ULLONG_MAX 18446744073709551615ULL + +#define SIZE_MAX 18446744073709551615ULL + +typedef unsigned long long size_t; +typedef long long ptrdiff_t; + +#define NULL 0 +#define EXIT_SUCCESS 0 +#define EXIT_FAILURE 1 + +#ifndef __bool_true_false_are_defined +#define __bool_true_false_are_defined 1 +#define bool _Bool +#define true 1 +#define false 0 +#endif /* __bool_true_false_are_defined */ + +#endif diff --git a/src/main/resources/tricera/headers/macros_lp64.h b/src/main/resources/tricera/headers/macros_lp64.h new file mode 100644 index 00000000..575cf5e0 --- /dev/null +++ b/src/main/resources/tricera/headers/macros_lp64.h @@ -0,0 +1,42 @@ +#ifndef MACROS_LP64_H +#define MACROS_LP64_H + +#define CHAR_BIT 8 + +#define SCHAR_MIN (-128) +#define SCHAR_MAX 127 +#define UCHAR_MAX 255 + +#define SHRT_MIN (-32768) +#define SHRT_MAX 32767 +#define USHRT_MAX 65535 + +#define INT_MIN (-2147483648) +#define INT_MAX 2147483647 +#define UINT_MAX 4294967295U + +#define LONG_MIN (-9223372036854775808L) +#define LONG_MAX 9223372036854775807L +#define ULONG_MAX 18446744073709551615UL + +#define LLONG_MIN (-9223372036854775808LL) +#define LLONG_MAX 9223372036854775807LL +#define ULLONG_MAX 18446744073709551615ULL + +#define SIZE_MAX 18446744073709551615UL + +typedef unsigned long size_t; +typedef long ptrdiff_t; + +#define NULL 0 +#define EXIT_SUCCESS 0 +#define EXIT_FAILURE 1 + +#ifndef __bool_true_false_are_defined +#define __bool_true_false_are_defined 1 +#define bool _Bool +#define true 1 +#define false 0 +#endif /* __bool_true_false_are_defined */ + +#endif diff --git a/src/main/resources/tricera/headers/macros_math.h b/src/main/resources/tricera/headers/macros_math.h new file mode 100644 index 00000000..a3790000 --- /dev/null +++ b/src/main/resources/tricera/headers/macros_math.h @@ -0,0 +1,36 @@ +#ifndef MACROS_MATH_H +#define MACROS_MATH_H + +#define CHAR_BIT 8 + +#define SCHAR_MIN (-128) +#define SCHAR_MAX 127 +#define UCHAR_MAX 255 + +#define SHRT_MIN (-32768) +#define SHRT_MAX 32767 +#define USHRT_MAX 65535 + +#define INT_MIN (-2147483648) +#define INT_MAX 2147483647 +#define UINT_MAX 4294967295U + +#define LLONG_MIN (-9223372036854775808LL) +#define LLONG_MAX 9223372036854775807LL +#define ULLONG_MAX 18446744073709551615ULL + +#define NULL 0 +#define EXIT_SUCCESS 0 +#define EXIT_FAILURE 1 + +typedef unsigned int size_t; +typedef int ptrdiff_t; + +#ifndef __bool_true_false_are_defined +#define __bool_true_false_are_defined 1 +#define bool _Bool +#define true 1 +#define false 0 +#endif /* __bool_true_false_are_defined */ + +#endif diff --git a/src/main/resources/tricera/heap/encodings/R-opt.yml b/src/main/resources/tricera/heap/encodings/R-opt.yml new file mode 100644 index 00000000..518e32fe --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/R-opt.yml @@ -0,0 +1,81 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last", type: "HEAP_TYPE", initial_value: null } + - { name: "$last_addr", type: "unsigned int", initial_value: null } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last", type: "HEAP_TYPE" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "$last = $HEAP_TYPE_DEFAULT();" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + ++$cnt; + if ($last_addr == p) { + result = $last_data; + } else { + if ($p_g == p) { + assert($R($cnt, $last)); + result = $last; + } else { + result = HAVOC_HEAP; + assume($R($cnt, result)); + } + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + $last_addr = p; + $last_data = e; + if ($p_g == p) { $last = e; } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + $last_addr = p; + $last_data = e; + if ($p_g == p) { $last = e; } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/R-tag-opt.yml b/src/main/resources/tricera/heap/encodings/R-tag-opt.yml new file mode 100644 index 00000000..d1d9d0fe --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/R-tag-opt.yml @@ -0,0 +1,93 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last", type: "HEAP_TYPE", initial_value: null } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$last_addr", type: "unsigned int", initial_value: null } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last", type: "HEAP_TYPE" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "$last = $HEAP_TYPE_DEFAULT();" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int l; + ++$cnt; + if ($last_addr == p) { + result = $last_data; + } else { + if ($p_g == p) { + assert($R($cnt, $last, loc, $last_loc)); + result = $last; + } else { + result = HAVOC_HEAP; + l = HAVOC_INT; + assume($R($cnt, result, loc, l)); + } + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last = e; + $last_loc = loc; + } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last = e; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/R-tag.yml b/src/main/resources/tricera/heap/encodings/R-tag.yml new file mode 100644 index 00000000..13d80985 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/R-tag.yml @@ -0,0 +1,81 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last", type: "HEAP_TYPE", initial_value: null } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last", type: "HEAP_TYPE" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "$last = $HEAP_TYPE_DEFAULT();" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int l; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last, loc, $last_loc)); + result = $last; + } else { + result = HAVOC_HEAP; + l = HAVOC_INT; + assume($R($cnt, result, loc, l)); + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + if ($p_g == p) { + $last = e; + $last_loc = loc; + } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + if ($p_g == p) { + $last = e; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/R.yml b/src/main/resources/tricera/heap/encodings/R.yml new file mode 100644 index 00000000..f2d96156 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/R.yml @@ -0,0 +1,69 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last", type: "HEAP_TYPE" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "$last = $HEAP_TYPE_DEFAULT();" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last)); + result = $last; + } else { + result = HAVOC_HEAP; + assume($R($cnt, result)); + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + if ($p_g == p) { $last = e; } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + if ($p_g == p) { $last = e; } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-fun-opt.yml b/src/main/resources/tricera/heap/encodings/RW-fun-opt.yml new file mode 100644 index 00000000..1e7cac72 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-fun-opt.yml @@ -0,0 +1,88 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_addr", type: "unsigned int", initial_value: null } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + #- "assert($W(0, $HEAP_TYPE_DEFAULT()));" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + ++$cnt; + if ($last_addr == p) { + result = $last_data; + } else { + int t; + if ($p_g == p) { + assert($R($cnt, $last_cnt)); + t = $last_cnt; + } else { + t = HAVOC_INT; + assume($R($cnt, t)); + } + result = HAVOC_HEAP; + assume($W(t, result)); + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + $last_addr = p; + $last_data = e; + assert($W($cnt, e)); + if ($p_g == p) { $last_cnt = $cnt; } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + $last_addr = p; + $last_data = e; + assert($W($cnt, e)); + if ($p_g == p) { $last_cnt = $cnt; } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt-p.yml b/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt-p.yml new file mode 100644 index 00000000..b2527e45 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt-p.yml @@ -0,0 +1,103 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$last_addr", type: "unsigned int", initial_value: "0" } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + - { name: "ptr", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + - { name: "write_loc", type: "int" } + - { name: "ptr", type: "int" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int t; + int l; + if ($last_addr == p) { + result = $last_data; + } else { + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt, loc, $last_loc, p)); + t = $last_cnt; + result = HAVOC_HEAP; + assume($W(t, result, $last_loc, p)); + } else { + t = HAVOC_INT; + l = HAVOC_INT; + assume($R($cnt, t, loc, l, p)); + result = HAVOC_HEAP; + assume($W(t, result, l, p)); + } + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + assert($W($cnt, e, loc, p)); + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e, loc, p)); + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt.yml b/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt.yml new file mode 100644 index 00000000..4d2371b2 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt.yml @@ -0,0 +1,101 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$last_addr", type: "unsigned int", initial_value: "0" } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + - { name: "write_loc", type: "int" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int t; + int l; + if ($last_addr == p) { + result = $last_data; + } else { + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt, loc, $last_loc)); + t = $last_cnt; + result = HAVOC_HEAP; + assume($W(t, result, $last_loc)); + } else { + t = HAVOC_INT; + l = HAVOC_INT; + assume($R($cnt, t, loc, l)); + result = HAVOC_HEAP; + assume($W(t, result, l)); + } + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + assert($W($cnt, e, loc)); + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e, loc)); + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt2.yml b/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt2.yml new file mode 100644 index 00000000..17e14306 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-fun-tag-opt2.yml @@ -0,0 +1,130 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$last_addr", type: "unsigned int", initial_value: "0" } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + - { name: "$dirty", type: "int", initial_value: "0" } + - { name: "$last_wt_loc", type: "int", initial_value: "-10" } + - { name: "$last_wt_cnt", type: "int", initial_value: "0" } + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + - { name: "write_loc", type: "int" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int t; + int l; + if ($last_addr == p) { + result = $last_data; + } else { + if($dirty) { // cache is dirty, flush it + assert($W($last_wt_cnt, $last_data, $last_wt_loc)); + if ($p_g == $last_addr) { + $last_cnt = $last_wt_cnt; + $last_loc = $last_wt_loc; + } + $dirty = 0; + } + int t; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt, loc, $last_loc)); + result = HAVOC_HEAP; + assume($W($last_cnt, result, $last_loc)); + } else { + t = HAVOC_INT; + l = HAVOC_INT; + assume($R($cnt, t, loc, l)); + result = HAVOC_HEAP; + assume($W(t, result, l)); + } + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + if (p == $last_addr) { + $last_data = e; + ++$cnt; + $last_wt_loc = loc; + $last_wt_cnt = $cnt; + $dirty = 1; + } else { + if($dirty) { // cache has data, flush it + assert($W($last_wt_cnt, $last_data, $last_wt_loc)); + if ($p_g == $last_addr) { + $last_cnt = $last_wt_cnt; + $last_loc = $last_wt_loc; + } + } + ++$cnt; + $last_addr = p; + $last_data = e; + $last_wt_loc = loc; + $last_wt_cnt = $cnt; + $dirty = 1; + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + if($dirty) { // cache has data, flush it + assert($W($last_wt_cnt, $last_data, $last_wt_loc)); + if ($p_g == $last_addr) { + $last_cnt = $last_wt_cnt; + $last_loc = $last_wt_loc; + } + } + int p = ++$allocCtr; + ++$cnt; + $last_addr = p; + $last_data = e; + $last_wt_loc = loc; + $last_wt_cnt = $cnt; + $dirty = 1; + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-fun-tag.yml b/src/main/resources/tricera/heap/encodings/RW-fun-tag.yml new file mode 100644 index 00000000..bbfd1d28 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-fun-tag.yml @@ -0,0 +1,86 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + - { name: "write_loc", type: "int" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result = HAVOC_HEAP; + int t; + int l; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt, loc, $last_loc)); + assume($W($last_cnt, result, $last_loc)); + } else { + t = HAVOC_INT; + l = HAVOC_INT; + assume($R($cnt, t, loc, l)); + assume($W(t, result, l)); + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + assert($W($cnt, e, loc)); + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e, loc)); + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-fun.yml b/src/main/resources/tricera/heap/encodings/RW-fun.yml new file mode 100644 index 00000000..af61f379 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-fun.yml @@ -0,0 +1,77 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + #- "assert($W(0, $HEAP_TYPE_DEFAULT()));" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int t; + int l; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt)); + t = $last_cnt; + } else { + t = HAVOC_INT; + assume($R($cnt, t)); + } + result = HAVOC_HEAP; + assume($W(t, result)); + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + assert($W($cnt, e)); + if ($p_g == p) { $last_cnt = $cnt; } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e)); + if ($p_g == p) { $last_cnt = $cnt; } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-tag-opt.yml b/src/main/resources/tricera/heap/encodings/RW-tag-opt.yml new file mode 100644 index 00000000..abf52423 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-tag-opt.yml @@ -0,0 +1,104 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$last_addr", type: "unsigned int", initial_value: "0" } + - { name: "$last_data", type: "HEAP_TYPE", initial_value: null } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + - { name: "write_loc", type: "int" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "assert($W(0, $HEAP_TYPE_DEFAULT(), -1));" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int t; + int l; + if ($last_addr == p) { + result = $last_data; + } else { + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt, loc, $last_loc)); + t = $last_cnt; + result = HAVOC_HEAP; + assume($W(t, result, $last_loc)); + } else { + t = HAVOC_INT; + l = HAVOC_INT; + assume($R($cnt, t, loc, l)); + result = HAVOC_HEAP; + assume($W(t, result, l)); + } + $last_addr = p; + $last_data = result; + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + assert($W($cnt, e, loc)); + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e, loc)); + $last_addr = p; + $last_data = e; + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW-tag.yml b/src/main/resources/tricera/heap/encodings/RW-tag.yml new file mode 100644 index 00000000..5bbc5071 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW-tag.yml @@ -0,0 +1,89 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_loc", type: "int", initial_value: "0" } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - { name: "read_loc", type: "int" } + - { name: "write_loc", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + - { name: "write_loc", type: "int" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "assert($W(0, $HEAP_TYPE_DEFAULT(), -1));" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result = HAVOC_HEAP; + int t; + int l; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt, loc, $last_loc)); + assume($W($last_cnt, result, $last_loc)); + } else { + t = HAVOC_INT; + l = HAVOC_INT; + assume($R($cnt, t, loc, l)); + assume($W(t, result, l)); + } + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + assert($W($cnt, e, loc)); + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e, loc)); + if ($p_g == p) { + $last_cnt = $cnt; + $last_loc = loc; + } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/resources/tricera/heap/encodings/RW.yml b/src/main/resources/tricera/heap/encodings/RW.yml new file mode 100644 index 00000000..3a955335 --- /dev/null +++ b/src/main/resources/tricera/heap/encodings/RW.yml @@ -0,0 +1,78 @@ +# Pointer type +ptr_type: "int" + +# Global variables +global_decls: + - { name: "$allocCtr", type: "int", initial_value: "0" } + - { name: "$cnt", type: "unsigned int", initial_value: "0" } + - { name: "$last_cnt", type: "unsigned int", initial_value: "0" } + - { name: "$p_g", type: "int", initial_value: null } # nondet init value + +# Uninterpreted predicates +predicates: + - name: "$R" + args: + - { name: "cnt", type: "int" } + - { name: "last_cnt", type: "int" } + - name: "$W" + args: + - { name: "last_cnt", type: "int" } + - { name: "o", type: "HEAP_TYPE" } + +# Initialisation code injected to the start of entry function +init_code: + - "$p_g = _;" + - "assert($W(0, $HEAP_TYPE_DEFAULT()));" + +# Heap operations +read_fn: + return_type: "HEAP_TYPE" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: | + HEAP_TYPE result; + int t; + ++$cnt; + if ($p_g == p) { + assert($R($cnt, $last_cnt)); + t = $last_cnt; + } else { + t = HAVOC_INT; + assume($R($cnt, t)); + } + result = HAVOC_HEAP; + assume($W(t, result)); + return result; + +write_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + ++$cnt; + if (0 < p && p <= $allocCtr) { + assert($W($cnt, e)); + if ($p_g == p) { $last_cnt = $cnt; } + } + +alloc_fn: + return_type: "PTR_TYPE" + args: + - { name: "e", type: "HEAP_TYPE" } + - { name: "loc", type: "int" } + body: | + int p = ++$allocCtr; + ++$cnt; + assert($W($cnt, e)); + if ($p_g == p) { $last_cnt = $cnt; } + return p; + +free_fn: + return_type: "void" + args: + - { name: "p", type: "PTR_TYPE" } + - { name: "loc", type: "int" } + body: "" diff --git a/src/main/scala/tricera/CPreprocessor.scala b/src/main/scala/tricera/CPreprocessor.scala index 9664dbbf..b8665e69 100644 --- a/src/main/scala/tricera/CPreprocessor.scala +++ b/src/main/scala/tricera/CPreprocessor.scala @@ -49,7 +49,32 @@ object CPreprocessor { try { val errorSuppressingLogger = ProcessLogger(_ => (), _ => ()) if (!includeSystemHeaders) { - ??? + val macroHeaderTempFile: File = { + val resourcePath = arithMode match { + case CCReader.ArithmeticMode.Mathematical => "tricera/headers/macros_math.h" + case CCReader.ArithmeticMode.ILP32 => "tricera/headers/macros_ilp32.h" + case CCReader.ArithmeticMode.LP64 => "tricera/headers/macros_lp64.h" + case CCReader.ArithmeticMode.LLP64 => "tricera/headers/macros_llp64.h" + } + + val inputStream = Option(getClass.getClassLoader.getResourceAsStream(resourcePath)) + .getOrElse { + throw new Main.MainException( + s"Could not find macro header for '$arithMode'. Expected in resources/$resourcePath" + ) + } + + val tmpFile = Files.createTempFile("tricera-macros-", ".h").toFile + tmpFile.deleteOnExit() + Files.copy(inputStream, tmpFile.toPath, StandardCopyOption.REPLACE_EXISTING) + inputStream.close() + tmpFile + } + + cmdLine = Seq("cpp", "-E", "-P", "-CC", "-nostdinc", "-undef") + val pipedInput = s"""#include "${macroHeaderTempFile.getAbsolutePath}"\n#include "$fileName""""" + val inputStream = new java.io.ByteArrayInputStream(pipedInput.getBytes) + (Process(cmdLine) #< inputStream #> preprocessedFile).!(errorSuppressingLogger) } else { cmdLine = Seq("cpp", fileName, "-E", "-P", "-CC") (Process(cmdLine) #> preprocessedFile).!(errorSuppressingLogger) @@ -59,7 +84,7 @@ object CPreprocessor { throw new Main.MainException( "The C preprocessor could not be executed. " + "This might be due to cpp not being installed in the system.\n" + - "Attempted command: " + cmdLine.mkString(" ") + "Attempted command: " + (if (cmdLine != null) cmdLine.mkString(" ") else "N/A") ) } preprocessedFile.getAbsolutePath diff --git a/src/main/scala/tricera/Main.scala b/src/main/scala/tricera/Main.scala index 05ede5a3..0126b802 100644 --- a/src/main/scala/tricera/Main.scala +++ b/src/main/scala/tricera/Main.scala @@ -31,7 +31,7 @@ package tricera import java.io.{FileOutputStream, PrintStream} -import java.nio.file.{Files, Paths} +import java.nio.file.{Files, Paths, StandardCopyOption} import sys.process._ import ap.parser.IExpression.{ConstantTerm, Predicate} import ap.parser.{IAtom, IConstant, IFormula, VariableSubstVisitor} @@ -272,8 +272,8 @@ class Main (args: Array[String]) { // C preprocessor (cpp) val cppFileName = - if(params.cPreprocessor) - CPreprocessor(fileName, includeSystemHeaders = true, params.arithMode) + if(params.cPreprocessor || params.cPreprocessorLight) + CPreprocessor(fileName, includeSystemHeaders = params.cPreprocessor, params.arithMode) else fileName // TriCera preprocessor (tri-pp) @@ -295,7 +295,8 @@ class Main (args: Array[String]) { preprocessedFile.getAbsolutePath, displayWarnings = logPPLevel == 2, quiet = logPPLevel == 0, - entryFunction = TriCeraParameters.get.funcName) + entryFunction = TriCeraParameters.get.funcName, + determinize = TriCeraParameters.get.determinizeInput) if (logPPLevel > 0) Console.withOut(outStream) { println("\n\nEnd of TriCera's preprocessor (tri-pp) warnings and errors") println("=" * 80) diff --git a/src/main/scala/tricera/concurrency/CCReader.scala b/src/main/scala/tricera/concurrency/CCReader.scala index e42de671..86037399 100644 --- a/src/main/scala/tricera/concurrency/CCReader.scala +++ b/src/main/scala/tricera/concurrency/CCReader.scala @@ -76,8 +76,13 @@ object CCReader { propertiesToCheck : Set[properties.Property] = Set( properties.Reachability)) : (CCReader, Boolean, CallSiteTransform.CallSiteTransforms) = { // second ret. arg is true if modelled heap + val programText = new java.util.Scanner(input).useDelimiter("\\A").next() + input.close() // Close the original reader. + val inputVarNames = ParseUtil.parseInputComment(programText) // for the invariant encoding heap model + val programReader = new java.io.StringReader(programText) + def entry(parser : concurrent_c.parser) = parser.pProgram - val prog = parseWithEntry(input, entry _) + val prog = parseWithEntry(programReader, entry _) val atCallTransformedProg = CCAstAtExpressionTransformer.transform(prog) val typeAnnotProg = CCAstTypeAnnotator(atCallTransformedProg) val (transformedCallsProg, callSiteTransforms) = @@ -87,7 +92,7 @@ object CCReader { while (reader == null) try { reader = new CCReader( - transformedCallsProg, entryFunction, propertiesToCheck, scala.Seq()) + transformedCallsProg, entryFunction, propertiesToCheck, inputVarNames) } catch { case NeedsTimeException => { warn("enabling time") @@ -609,8 +614,12 @@ class CCReader private (prog : Program, for(FieldInfo(rawFieldName, fieldType, ptrDepth) <- struct.fieldInfos) yield (CCStruct.rawToFullFieldName(struct.name, rawFieldName), - if (ptrDepth > 0) Heap.AddrSort - else { fieldType match { + if (ptrDepth > 0) { + if (TriCeraParameters.get.invEncoding.nonEmpty) + HeapObj.OtherSort(Sort.Integer) + else + HeapObj.AddrSort + } else { fieldType match { case Left(ind) => HeapObj.ADTSort(ind + 1) case Right(typ) => typ match { @@ -623,20 +632,17 @@ class CCReader private (prog : Program, }).toList // todo: only add types that exist in the program - should also add machine arithmetic types - val predefSignatures = List( - ("O_Int", HeapObj.CtorSignature( - List(("getInt", HeapObj.OtherSort(CCInt.toSort))), ObjSort)), - ("O_UInt", HeapObj.CtorSignature( - List(("getUInt", HeapObj.OtherSort(CCUInt.toSort))), ObjSort)), - ("O_Addr", HeapObj.CtorSignature( - List(("getAddr", HeapObj.AddrSort)), ObjSort)), - ("O_AddrRange", HeapObj.CtorSignature( - List(("getAddrRange", HeapObj.AddrRangeSort)), ObjSort)) - ) - // Make sure that we have one object sort per sort - private val ctorObjSorts = - predefSignatures.flatMap(s => s._2.arguments.map(_._2)) - assert(ctorObjSorts.toSet.size == ctorObjSorts.size) + val predefSignatures = + List(("O_Int", HeapObj.CtorSignature(List(("getInt", HeapObj.OtherSort(CCInt.toSort))), ObjSort)), + ("O_UInt", HeapObj.CtorSignature(List(("getUInt", HeapObj.OtherSort(CCUInt.toSort))), ObjSort))) ++ + (if (TriCeraParameters.get.invEncoding.nonEmpty) Nil else List( + ("O_Addr", HeapObj.CtorSignature(List(("getAddr", HeapObj.AddrSort)), ObjSort)), + ("O_AddrRange", HeapObj.CtorSignature(List(("getAddrRange", HeapObj.AddrRangeSort)), ObjSort)) + )) +// Make sure that we have one object sort per sort +private val ctorObjSorts = + predefSignatures.flatMap(s => s._2.arguments.map(_._2)) +assert(ctorObjSorts.toSet.size == ctorObjSorts.size) val wrapperSignatures : List[(String, HeapObj.CtorSignature)] = @@ -707,7 +713,8 @@ class CCReader private (prog : Program, case _ => typ } } - if(fieldInfos(j).ptrDepth > 0) CCHeapPointer(heap, actualType) + if(fieldInfos(j).ptrDepth > 0) + createHeapPointer(actualType) else actualType})} structDefs += ((ctor.name, CCStruct(ctor, fieldsWithType))) } @@ -729,7 +736,12 @@ class CCReader private (prog : Program, } private val heapModelFactory : HeapModelFactory = - HeapModel.factory(HeapModel.ModelType.TheoryOfHeaps, symexContext, scope, inputVars) + tricera.params.TriCeraParameters.get.invEncoding match { + case Some(_) => + HeapModel.factory(HeapModel.ModelType.Invariants, symexContext, scope, inputVars) + case None => + HeapModel.factory(HeapModel.ModelType.TheoryOfHeaps, symexContext, scope, inputVars) + } for ((name, funcDefAst) <- heapModelFactory.getFunctionsToInject if modelHeap) { if (functionDefs.contains(name)) { @@ -1529,7 +1541,8 @@ class CCReader private (prog : Program, val res = values.eval(actualInitExp)( values.EvalSettings(), evalContext) val (actualLhsVar, actualRes) = lhsVar.typ match { - case _ : CCHeapPointer if res.typ.isInstanceOf[CCArithType] => + case _ : CCHeapPointer if res.typ.isInstanceOf[CCArithType] + && TriCeraParameters.get.invEncoding.isEmpty => if(res.toTerm.asInstanceOf[IIntLit].value.intValue == 0) (lhsVar, CCTerm.fromTerm(heap.nullAddr(), varDec.typ, srcInfo)) else throw new TranslationException("Pointer arithmetic is not " + @@ -1726,9 +1739,9 @@ class CCReader private (prog : Program, private def getPtrType (ptr : Pointer, _typ : CCType) : CCType = { ptr match { - case _ : Point | _ : PointQual => CCHeapPointer(heap, _typ) // todo; support pointer qualifiers? + case _ : Point | _ : PointQual => createHeapPointer(_typ) // todo; support pointer qualifiers? case ptr : PointPoint => - getPtrType(ptr.pointer_, CCHeapPointer(heap, _typ)) + getPtrType(ptr.pointer_, createHeapPointer(_typ)) case _ => throw new TranslationException( "Advanced pointer declarations are not yet supported (line " + getSourceInfo(ptr).line + ")" @@ -2124,7 +2137,7 @@ class CCReader private (prog : Program, getType(listDeclSpecs) case None => CCInt } - if(f.decl.isInstanceOf[BeginPointer]) CCHeapPointer(heap, typ) // SSSOWO Still relevant: todo: can be stack pointer too, this needs to be fixed + if(f.decl.isInstanceOf[BeginPointer]) createHeapPointer(typ) // SSSOWO Still relevant: todo: can be stack pointer too, this needs to be fixed else typ } @@ -2214,20 +2227,23 @@ class CCReader private (prog : Program, scope.LocalVars popFrame } - private def createHeapPointer(decl : BeginPointer, typ : CCType) : - CCHeapPointer = createHeapPointerHelper(decl.pointer_, typ) + private def createHeapPointer(objectType : CCType) : CCType = + CCHeapPointer(heap, objectType) - private def createHeapPointer(decl : PointerStart, typ : CCType) : - CCHeapPointer = createHeapPointerHelper(decl.pointer_, typ) + private def createHeapPointer(decl : BeginPointer, typ : CCType) : CCType = + createHeapPointerHelper(decl.pointer_, typ) - private def createHeapPointerHelper(decl : Pointer, typ : CCType) : - CCHeapPointer = decl match { + private def createHeapPointer(decl : PointerStart, typ : CCType) : CCType = + createHeapPointerHelper(decl.pointer_, typ) + + private def createHeapPointerHelper(decl : Pointer, typ : CCType) : CCType = + decl match { case pp : PointPoint => - CCHeapPointer(heap, createHeapPointerHelper(pp.pointer_, typ)) - case p : Point => - CCHeapPointer(heap, typ) - case _ => throw new TranslationException("Type qualified pointers are " + - "currently not supported: " + decl) + createHeapPointer(createHeapPointerHelper(pp.pointer_, typ)) + case p : Point => + createHeapPointer(typ) + case _ => throw new TranslationException( + s"Type qualified pointers are currently not supported: $decl") } private def getFunctionArgNames(functionDef : Function_def) : scala.Seq[String] = { @@ -2753,7 +2769,10 @@ class CCReader private (prog : Program, output(addRichClause(entryClause, entryPred.srcInfo)) val initStmts : Iterator[Stm] = { - val inputInitCode = scala.Seq() + val inputInitCode = + if(TriCeraParameters.get.determinizeInput) + inputVars.map(v => s"${v.name} = _;") + else scala.Seq() val heapModelInitCode = if (modelHeap) heapModelFactory.getInitCodeToInject else scala.Seq() diff --git a/src/main/scala/tricera/concurrency/ParseUtil.scala b/src/main/scala/tricera/concurrency/ParseUtil.scala index 2f68e385..e3bd56ca 100644 --- a/src/main/scala/tricera/concurrency/ParseUtil.scala +++ b/src/main/scala/tricera/concurrency/ParseUtil.scala @@ -89,4 +89,19 @@ object ParseUtil { CCReader.parseWithEntry(new StringReader(programText), entry) } + /** + * Parses the "/* INPUT: ... */" comment from the raw program text. + * This is produced by tri-pp when using the [[InvariantEncodingModel]] for heap. + * @param programText The full content of the C source file. + * @return A sequence of input variable names found, or an empty sequence if not found. + */ + def parseInputComment(programText : String) : Seq[String] = { + val pattern = """/\*\s*INPUT:\s*([^/\\*]+)\*/""".r + pattern.findFirstMatchIn(programText) match { + case Some(m) => + m.group(1).split(',').map(_.trim).filter(_.nonEmpty).toSeq + case None => + Seq.empty + } + } } diff --git a/src/main/scala/tricera/concurrency/Symex.scala b/src/main/scala/tricera/concurrency/Symex.scala index ede92c50..a26e47d5 100644 --- a/src/main/scala/tricera/concurrency/Symex.scala +++ b/src/main/scala/tricera/concurrency/Symex.scala @@ -339,6 +339,18 @@ class Symex private (context : SymexContext, case _ : CCHeapArrayPointer => true case _ => false } + private def isHeapPointer(exp : Exp, enclosingFunction : String) = + getVar(asLValue(exp), enclosingFunction).typ match { + case _ : CCHeapPointer => true + case _ : CCHeapArrayPointer => true + case _ => false + } + + private def isIndirection(exp : Exp) : Boolean = + exp match { + case exp : Epreop => exp.unary_operator_.isInstanceOf[Indirection] + case _ => false + } private def getPointerType(ind : Int) = { getValue(ind, false).typ match { @@ -530,11 +542,15 @@ class Symex private (context : SymexContext, case CCTerm(_, _: CCStackPointer, srcInfo, _) => throw new UnsupportedCFragmentException( getLineStringShort(srcInfo) + " Only limited support for stack pointers") - case CCTerm(IIntLit(value), _, _, _) if isHeapPointer(lhsVal) => + case CCTerm(t@IIntLit(value), _, _, _) if isHeapPointer(lhsVal) => if (value.intValue != 0) { throw new TranslationException("Pointer assignment only supports 0 (NULL)") - } else CCTerm.fromTerm( - context.heap.nullAddr(), CCHeapPointer(context.heap, lhsVal.typ), newValue.srcInfo) + } else { + val rhsVal : ITerm = if(TriCeraParameters.get.invEncoding.isEmpty) + context.heap.nullAddr() + else t + CCTerm.fromTerm(rhsVal, CCHeapPointer(context.heap, lhsVal.typ), newValue.srcInfo) + } case _ => newValue } @@ -830,6 +846,16 @@ class Symex private (context : SymexContext, Some(callFunction(call.functionName, call.args, call.sourceInfo)) case call : HeapModel.FunctionCallWithGetter => val callResult = callFunction(call.functionName, call.args, call.sourceInfo) + val canAssumeMemorySafety = TriCeraParameters.get.invEncoding match { + case Some(enc) => enc contains "-fun-" + case None => false + } + if(canAssumeMemorySafety || + !context.propertiesToCheck.contains(properties.MemValidDeref)) { + val safetyFormula = context.heap.hasUserHeapCtor( + callResult.toTerm, context.sortCtorIdMap(call.resultType.toSort)) + addGuard(safetyFormula) + } Some(CCTerm.fromTerm(call.getter(callResult.toTerm), call.resultType, call.sourceInfo)) @@ -1359,8 +1385,15 @@ class Symex private (context : SymexContext, case "malloc" | "calloc" => ArrayLocation.Heap case "alloca" | "__builtin_alloca" => ArrayLocation.Stack } + + val canAssumeMemorySafety = TriCeraParameters.get.invEncoding match { + case Some(enc) => enc contains "-fun-" + case None => false + } + val objectTerm = CCTerm.fromTerm(name match { case "calloc" => typ.getZeroInit + case _ if canAssumeMemorySafety => typ.getZeroInit case "malloc" | "alloca" | "__builtin_alloca" => typ.getNonDet }, typ, srcInfo) @@ -1426,9 +1459,14 @@ class Symex private (context : SymexContext, sizeInt match { case Some(1) => // use regular heap model, this is not an array + val canAssumeMemorySafety = TriCeraParameters.get.invEncoding match { + case Some(enc) => enc contains "-fun-" + case None => false + } val objectTerm = CCTerm.fromTerm(name match { case "calloc" => typ.getZeroInit + case _ if canAssumeMemorySafety => typ.getZeroInit case "malloc" | "alloca" | "__builtin_alloca" => typ.getNonDet }, typ, srcInfo) @@ -1790,14 +1828,22 @@ class Symex private (context : SymexContext, if (t2.toTerm != IIntLit(IdealInt(0))) throw new TranslationException("Pointers can only compared with `null` or `0`. " + getLineString(t2.srcInfo)) - else - (t1, CCTerm.fromTerm(context.heap.nullAddr(), t1.typ, t1.srcInfo)) // 0 to nullAddr() + else { + val actualT2 = if(TriCeraParameters.get.invEncoding.isEmpty) + context.heap.nullAddr() + else t2.toTerm + (t1, CCTerm.fromTerm(actualT2, t1.typ, t1.srcInfo)) // 0 to nullAddr() + } case (_: CCArithType, _: CCHeapPointer) => if (t1.toTerm != IIntLit(IdealInt(0))) throw new TranslationException("Pointers can only compared with `null` or `0`. " + getLineString(t2.srcInfo)) - else - (CCTerm.fromTerm(context.heap.nullAddr(), t2.typ, t2.srcInfo), t2) // 0 to nullAddr() + else { + val actualT1 = if(TriCeraParameters.get.invEncoding.isEmpty) + context.heap.nullAddr() + else t1.toTerm + (CCTerm.fromTerm(actualT1, t2.typ, t2.srcInfo), t2) // 0 to nullAddr() + } case _ => (t1, t2) } } diff --git a/src/main/scala/tricera/concurrency/TriCeraPreprocessor.scala b/src/main/scala/tricera/concurrency/TriCeraPreprocessor.scala index 2af1ed81..f6fc2fb7 100644 --- a/src/main/scala/tricera/concurrency/TriCeraPreprocessor.scala +++ b/src/main/scala/tricera/concurrency/TriCeraPreprocessor.scala @@ -31,33 +31,36 @@ package tricera.concurrency import tricera.Main -import sys.process._ +import sys.process.Process import java.nio.file.{Files, Paths} class TriCeraPreprocessor(val inputFilePath : String, val outputFilePath : String, val entryFunction : String, val displayWarnings : Boolean, - val quiet : Boolean) { - val ppPath = sys.env.get("TRI_PP_PATH") match { + val quiet : Boolean, + val determinize : Boolean) { + val ppPath : String = sys.env.get("TRI_PP_PATH") match { case Some(path) => path + "/tri-pp" case _ => val path = Paths.get(System.getProperty("user.dir") + "/tri-pp") - if (Files.exists(path)) path - else - throw new Main.MainException("The preprocessor binary" + + if (Files.exists(path)) path.toString + else throw new Main.MainException("The preprocessor binary" + " (tri-pp) could not be found. Please ensure that the environment " + "variable TRI_PP_PATH is exported and points to the preprocessor's" + " base directory") } - private val cmdLine : scala.Seq[String] = - (scala.Seq(ppPath.toString, inputFilePath,"-o", outputFilePath) ++ - (if(quiet) scala.Seq("-q") else Nil) ++ - scala.Seq("-m", entryFunction, "--", "-xc") ++ - (if(displayWarnings) Nil else scala.Seq("-Wno-everything"))) - private val returnCode = - try { Process(cmdLine) ! } - catch { + + private def runPreprocessor(extraArgs : scala.Seq[String], + errorMsg : String, + input : String, + output : String) : Int = { + val cmdLine : scala.Seq[String] = scala.Seq(ppPath, input, "-o", output) ++ + (if (quiet) scala.Seq("-q") else Nil) ++ extraArgs ++ + scala.Seq("-m", entryFunction, "--", "-xc") ++ + (if (displayWarnings) Nil else scala.Seq("-Wno-everything")) + + try { Process(cmdLine) ! } catch { case _: Throwable => throw new Main.MainException("TriCera preprocessor could not" + " be executed. This might be due to TriCera preprocessor binary " + @@ -66,5 +69,21 @@ class TriCeraPreprocessor(val inputFilePath : String, "Preprocessor command: " + cmdLine ) } - val hasError = returnCode != 0 + } + + private val initialReturnCode = runPreprocessor( + Nil, "TriCera preprocessor could not be executed.", inputFilePath, outputFilePath) + val hasError : Boolean = initialReturnCode != 0 + + if (determinize) { + val determinizeSteps = Seq( + ("--make-calls-unique", "tri-pp failed while trying to make calls unique."), + ("--determinize", "tri-pp failed while trying to make the program deterministic.") + ) + + determinizeSteps.foldLeft(0){ + case (_, (arg, msg)) => + runPreprocessor(Seq(arg), msg, outputFilePath, outputFilePath) + } + } } diff --git a/src/main/scala/tricera/concurrency/ccreader/CCTerm.scala b/src/main/scala/tricera/concurrency/ccreader/CCTerm.scala index d0f236fc..01b99053 100644 --- a/src/main/scala/tricera/concurrency/ccreader/CCTerm.scala +++ b/src/main/scala/tricera/concurrency/ccreader/CCTerm.scala @@ -34,6 +34,7 @@ import tricera.Util.SourceInfo import CCExceptions._ import ap.parser.IExpression._ import tricera.concurrency.CCReader +import tricera.params.TriCeraParameters case class CCTerm(t : ITerm, typ : CCType, @@ -43,7 +44,7 @@ case class CCTerm(t : ITerm, def toFormula : IFormula = originalFormula getOrElse { t match { case IIntLit(value) => !value.isZero - case t if typ.isInstanceOf[CCHeapPointer] => + case t if typ.isInstanceOf[CCHeapPointer] && TriCeraParameters.get.invEncoding.isEmpty => !IExpression.Eq(t, typ.asInstanceOf[CCHeapPointer].heap.nullAddr()) case t if typ == CCBool => t === ap.theories.ADT.BoolADT.True case t => !IExpression.eqZero(t) @@ -52,11 +53,14 @@ case class CCTerm(t : ITerm, def occurringConstants: Seq[IExpression.ConstantTerm] = SymbolCollector constantsSorted t def convertToType(newType: CCType): CCTerm = { + val isInvEncoding = TriCeraParameters.get.invEncoding.nonEmpty (typ, newType) match { case (oldType, newType) if (oldType == newType) => this case (_: CCArithType, newType: CCArithType) => newType cast this + case (_: CCArithType, newType: CCHeapPointer) if isInvEncoding => + newType cast this case (_: CCArithType, CCDuration) => { if (!CCReader.useTime) throw NeedsTimeException @@ -69,6 +73,8 @@ case class CCTerm(t : ITerm, // todo: do not do anything for casts to void? case (oldType: CCArithType, newType: CCHeapPointer) => toTerm match { + case lit: IIntLit if lit.value.intValue == 0 && TriCeraParameters.get.invEncoding.nonEmpty => + CCTerm.fromTerm(IIntLit(0), newType, srcInfo) case lit: IIntLit if lit.value.intValue == 0 => CCTerm.fromTerm(newType.heap.nullAddr(), newType, srcInfo) //newType cast t case _ => diff --git a/src/main/scala/tricera/concurrency/ccreader/CCType.scala b/src/main/scala/tricera/concurrency/ccreader/CCType.scala index 532d9cdf..a8f4b017 100644 --- a/src/main/scala/tricera/concurrency/ccreader/CCType.scala +++ b/src/main/scala/tricera/concurrency/ccreader/CCType.scala @@ -38,6 +38,7 @@ import ap.theories.bitvectors.ModuloArithmetic._ import ap.types.{MonoSortedIFunction, SortedConstantTerm} import CCExceptions._ import tricera.Util.{SourceInfo, getLineString, getLineStringShort} +import tricera.params.TriCeraParameters import scala.collection.mutable.{Stack, HashMap => MHashMap} @@ -56,7 +57,12 @@ abstract sealed class CCType { case CCHeap(heap) => heap.HeapSort case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer + case CCHeapPointer(_ , _) if TriCeraParameters.get.invEncoding.nonEmpty => + Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort + case CCHeapArrayPointer(_, _, _) + if tricera.params.TriCeraParameters.get.invEncoding.nonEmpty + => Sort.Integer case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort case CCArray(_, _, _, s, _) => s.sort case CCStruct(ctor, _) => ctor.resSort @@ -78,8 +84,13 @@ abstract sealed class CCType { case CCHeap(heap) => heap.HeapSort case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer + case CCHeapPointer(_ , _) if TriCeraParameters.get.invEncoding.nonEmpty => + Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort case CCArray(_, _, _, s, _) => s.sort + case CCHeapArrayPointer(_, _, _) + if tricera.params.TriCeraParameters.get.invEncoding.nonEmpty + => Sort.Integer case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort case CCStruct(ctor, _) => ctor.resSort case CCStructField(n, s) => s(n).ctor.resSort @@ -100,7 +111,12 @@ abstract sealed class CCType { case CCHeap(heap) => heap.HeapSort case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer + case CCHeapPointer(_ , _) if TriCeraParameters.get.invEncoding.nonEmpty => + Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort + case CCHeapArrayPointer(_, _, _) + if tricera.params.TriCeraParameters.get.invEncoding.nonEmpty + => Sort.Integer case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort case CCArray(_, _, _, s, _) => s.sort case CCStruct(ctor, _) => ctor.resSort @@ -122,7 +138,12 @@ abstract sealed class CCType { case CCHeap(heap) => heap.HeapSort case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer + case CCHeapPointer(_ , _) if TriCeraParameters.get.invEncoding.nonEmpty => + Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort + case CCHeapArrayPointer(_, _, _) + if tricera.params.TriCeraParameters.get.invEncoding.nonEmpty + => Sort.Integer case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort case CCArray(_, _, _, s, _) => s.sort case CCStruct(ctor, _) => ctor.resSort @@ -237,9 +258,11 @@ abstract sealed class CCType { * possible to do in this class. */ private def castIsAllowed(newType : CCType) : Boolean = { + val isInvariantEncoding = TriCeraParameters.get.invEncoding.nonEmpty this match { - case typ if typ.isArithType && newType.isPointerType - || typ.isPointerType && newType.isArithType => false + case typ if !isInvariantEncoding && + (typ.isArithType && newType.isPointerType + || typ.isPointerType && newType.isArithType) => false case _ => true } } @@ -280,6 +303,8 @@ abstract sealed class CCType { case _ => fieldType.getZeroInit } structType.ctor(const: _*) + case CCHeapPointer(_, _) if TriCeraParameters.get.invEncoding.nonEmpty + => IIntLit(0) case CCHeapPointer(heap, _) => heap.nullAddr() case CCHeapArrayPointer(heap, _, _) => heap.nthAddrRange(0, IIntLit(1)) case CCArray(_, _, _, arrayTheory, _) => arrayTheory.const(0) @@ -503,7 +528,12 @@ case class CCStruct(ctor : MonoSortedIFunction, structs(name).getInitialized(values) case s: CCStruct => s.getInitialized(values) case CCHeapPointer(h, _) => - if (values.isEmpty) h.nullAddr() else values.pop() + val nullAddr = + if (TriCeraParameters.get.invEncoding.nonEmpty) + IIntLit(0) + else + h.nullAddr() + if (values.isEmpty) nullAddr else values.pop() case CCHeapArrayPointer(h, _, _) => throw new TranslationException( "Heap arrays inside structs are" + diff --git a/src/main/scala/tricera/concurrency/heap/HeapModel.scala b/src/main/scala/tricera/concurrency/heap/HeapModel.scala index 44175f14..5c8428ec 100644 --- a/src/main/scala/tricera/concurrency/heap/HeapModel.scala +++ b/src/main/scala/tricera/concurrency/heap/HeapModel.scala @@ -106,7 +106,7 @@ object HeapModel { inputVars : scala.Seq[CCVar]) : HeapModelFactory = mt match { case ModelType.TheoryOfHeaps => new HeapTheoryFactory(context, scope) - case ModelType.Invariants => ??? // new InvariantsHeapFactory(context, scope) + case ModelType.Invariants => new InvariantEncodingsFactory(context, scope, inputVars) } } diff --git a/src/main/scala/tricera/concurrency/heap/InvariantEncodingParser.scala b/src/main/scala/tricera/concurrency/heap/InvariantEncodingParser.scala new file mode 100644 index 00000000..7c37e632 --- /dev/null +++ b/src/main/scala/tricera/concurrency/heap/InvariantEncodingParser.scala @@ -0,0 +1,57 @@ +package tricera.concurrency.heap + +import tricera.concurrency.ccreader.CCExceptions.TranslationException +import net.jcazevedo.moultingyaml._ + +object InvariantEncodingParser { + case class Declaration(name : String, + `type` : String, + initial_value : Option[String]) + case class Argument (name : String, + `type` : String) + case class Predicate (name : String, + args : List[Argument]) + case class FunctionDef(return_type : String, + args : List[Argument], + body : String) + case class ParsedEncoding( + ptr_type : String, + global_decls : Option[List[Declaration]], + predicates : Option[List[Predicate]], + init_code : List[String], + read_fn : FunctionDef, + write_fn : FunctionDef, + alloc_fn : FunctionDef, + free_fn : FunctionDef + ) + + object EncodingYamlProtocol extends DefaultYamlProtocol { + implicit val argumentFormat : YamlFormat[Argument] = yamlFormat2(Argument) + implicit val declarationFormat : YamlFormat[Declaration] = yamlFormat3(Declaration) + implicit val predicateFormat : YamlFormat[Predicate] = yamlFormat2(Predicate) + implicit val functionDefFormat : YamlFormat[FunctionDef] = yamlFormat3(FunctionDef) + implicit val encodingFormat : YamlFormat[ParsedEncoding] = yamlFormat8(ParsedEncoding) + } + + def parse(encodingName : String) : ParsedEncoding = { + val resourcePath = s"tricera/heap/encodings/$encodingName.yml" + val inputStream = Option(getClass.getClassLoader.getResourceAsStream(resourcePath)) + .getOrElse { + throw new TranslationException( + s"Could not find encoding file for '$encodingName'. " + + s"Expected to find it at 'resources/$resourcePath'") + } + val source = scala.io.Source.fromInputStream(inputStream) + try { + import EncodingYamlProtocol._ + val yamlAst = source.mkString.parseYaml + yamlAst.convertTo[ParsedEncoding] + } catch { + case e: Throwable => + throw new TranslationException(s"Failed to parse encoding file for " + + s"'$encodingName': $e") + } finally { + source.close() + } + } +} diff --git a/src/main/scala/tricera/concurrency/heap/InvariantEncodingsModel.scala b/src/main/scala/tricera/concurrency/heap/InvariantEncodingsModel.scala new file mode 100644 index 00000000..ff9fee26 --- /dev/null +++ b/src/main/scala/tricera/concurrency/heap/InvariantEncodingsModel.scala @@ -0,0 +1,291 @@ +/** + * Copyright (c) 2025 Zafer Esen. 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. + */ + +package tricera.concurrency.heap + +import ap.basetypes.IdealInt +import ap.parser.{IExpression, ITerm} +import IExpression.toFunApplier +import tricera.acsl.ACSLTranslator +import tricera.concurrency.ccreader.CCExceptions.TranslationException +import tricera.concurrency.ccreader._ +import tricera.concurrency.concurrent_c.Absyn.{Afunc, Function_def} +import tricera.concurrency.heap.HeapModel._ +import tricera.concurrency.heap.InvariantEncodingParser.ParsedEncoding +import tricera.concurrency.{ParseUtil, SymexContext} +import tricera.params.TriCeraParameters + +import java.io.StringReader +import java.util.regex.{Matcher, Pattern} +import scala.annotation.tailrec +import scala.collection.mutable + +final class InvariantEncodingsFactory( + context : SymexContext, + scope : CCScope, + inputVars : Seq[CCVar]) extends HeapModelFactory { + + private val encodingName = TriCeraParameters.get.invEncoding.getOrElse( + throw new IllegalStateException( + "InvariantEncodingsFactory created without an encoding type specified.") + ) + + private val originalEncoding : ParsedEncoding = + InvariantEncodingParser.parse(encodingName) + + private val (transformedInitCode, transformedFunctions) = { + if (inputVars.isEmpty) { + (originalEncoding.init_code, Map( + "$read" -> originalEncoding.read_fn, + "$write" -> originalEncoding.write_fn, + "$alloc" -> originalEncoding.alloc_fn, + "$free" -> originalEncoding.free_fn + )) + } else { + val predNames = originalEncoding.predicates.getOrElse(Nil).map(_.name).toSet + + def transform(code : String) : String = + transformPredicateCalls(code, predNames, inputVars) + + val newInit = originalEncoding.init_code.map(transform) + val newFuncs = Map( + "$read" -> originalEncoding.read_fn.copy(body = transform(originalEncoding.read_fn.body)), + "$write" -> originalEncoding.write_fn.copy(body = transform(originalEncoding.write_fn.body)), + "$alloc" -> originalEncoding.alloc_fn.copy(body = transform(originalEncoding.alloc_fn.body)), + "$free" -> originalEncoding.free_fn.copy(body = transform(originalEncoding.free_fn.body)) + ) + (newInit, newFuncs) + } + } + + /** + * Uses regex to find and prepend arguments to predicate calls in a C code string. + */ + private def transformPredicateCalls(code : String, + predNames : Set[String], + argsToPrepend : Seq[CCVar]) : String = { + if (argsToPrepend.isEmpty || predNames.isEmpty) return code + + val predPattern = predNames.map(Pattern.quote).mkString("|") + val regex = s"($predPattern)\\s*\\(([^)]*)\\)".r + + regex.replaceAllIn(code, m => { + // m.group(1) is the predicate name, e.g., "$R" + // m.group(2) is the string of existing arguments, e.g., "$cnt, $last_cnt" + val predName = m.group(1) + val existingArgs = m.group(2).trim + + // We must escape the predicate name AND the existing arguments, + // as both are captured from the source and contain literal '$' characters. + val escapedPredName = Matcher.quoteReplacement(predName) + val escapedExistingArgs = Matcher.quoteReplacement(existingArgs) + + val argsToPrependString = argsToPrepend.map(_.name).mkString(", ") + if (existingArgs.isEmpty) { + s"$escapedPredName($argsToPrependString)" + } else { + s"$escapedPredName($argsToPrependString, $escapedExistingArgs)" + } + }) + } + + @tailrec + private def stringToCCType(typeStr : String, + forPointer : Boolean = false) + : CCType = typeStr match { + case "int" => CCInt + case "unsigned int" => CCUInt + case "void" => CCVoid + case "PTR_TYPE" if forPointer => + throw new TranslationException("PTR_TYPE cannot be nested.") + case "PTR_TYPE" => stringToCCType(originalEncoding.ptr_type, forPointer = true) + case "HEAP_TYPE" => CCHeapObject(context.heap) + case _ => throw new TranslationException( + s"Unsupported type in encoding file: $typeStr") + } + + override def requiredVars: Seq[VarSpec] = originalEncoding.global_decls match { + case Some(decls) => decls.map { decl => + val ccType = stringToCCType(decl.`type`) + val initialValue = decl.initial_value match { + case Some(v) => ccType match { + case _: CCArithType => IExpression.i(IdealInt(v)) + case _ => throw new TranslationException(s"Initial value for type ${decl.`type`} not supported.") + } + case None => ccType.getNonDet + } + VarSpec(decl.name, ccType, isGlobal = true, initialValue) + } + case None => Seq() + } + + override def requiredPreds: Seq[PredSpec] = originalEncoding.predicates match { + case Some(preds) => preds.map { + pred => + val originalArgs = pred.args.map (arg => + new CCVar (arg.name, None, stringToCCType (arg.`type`), AutoStorage)) + PredSpec (pred.name, inputVars ++ originalArgs) + } + case None => Seq() + } + + private def preprocess(code: String): String = { + val heapObjectReplacement = Matcher.quoteReplacement("$HeapObject") + code + .replaceAll("\\bPTR_TYPE\\b", originalEncoding.ptr_type) + .replaceAll("\\bHEAP_TYPE\\b", heapObjectReplacement) // <-- CORRECTED + .replaceAll("\\b(HAVOC_INT|HAVOC_HEAP|HEAP_DEFAULT)\\b", "_") + } + + override def getFunctionsToInject: Map[String, Function_def] = { + transformedFunctions.map { case (name, funcDef) => + val args = funcDef.args.map(a => s"${a.`type`} ${a.name}").mkString(", ") + val body = if (funcDef.body.trim.isEmpty) ";" else funcDef.body + val funString = s"${funcDef.return_type} $name($args) { $body }" + + val processedString = preprocess(funString) + val parsedFunc = ParseUtil.parseFunctionDefinition( + new StringReader(processedString)).asInstanceOf[Afunc] + + (name, parsedFunc.function_def_) + } + } + + override def getInitCodeToInject: Seq[String] = { + val originalInitCode = { + val code = transformedInitCode + if (code.size == 1 && code.head.isEmpty) + Seq() + else + code.map { stmtString => + val terminatedStmt = if (stmtString.trim.endsWith(";")) stmtString else stmtString + ";" + preprocess(terminatedStmt) + } + } + originalInitCode + } + + override def apply(resources: Resources): HeapModel = + new InvariantEncodingsModel(context, scope, originalEncoding) +} + +class InvariantEncodingsModel(context : SymexContext, + scope : CCScope, + encoding : ParsedEncoding) extends HeapModel{ + private val readFnName = "$read" + private val writeFnName = "$write" + private val allocFnName = "$alloc" + private val freeFnName = "$free" + + override def read(p : CCTerm, s : Seq[CCTerm], loc : CCTerm) : HeapOperationResult = { + val resultType = p.typ.asInstanceOf[CCHeapPointer].typ + val getter = context.sortGetterMap(resultType.toSort) + FunctionCallWithGetter( + functionName = readFnName, + args = Seq(p, loc), + resultType = resultType, + getter = getter, + sourceInfo = p.srcInfo + ) + } + + override def write(p : CCTerm, o : CCTerm, s : Seq[CCTerm], loc : CCTerm) + : HeapOperationResult = { + FunctionCall( + functionName = writeFnName, + args = Seq(p, o, loc), + resultType = CCVoid, + sourceInfo = p.srcInfo + ) + } + + override def alloc(o : CCTerm, oType : CCType, s : Seq[CCTerm], loc : CCTerm) : HeapOperationResult = { + FunctionCall( + functionName = allocFnName, + args = Seq(o, loc), + resultType = CCHeapPointer(context.heap, oType), + sourceInfo = o.srcInfo + ) + } + + override def free(p : CCTerm, s : Seq[CCTerm], loc : CCTerm) : HeapOperationResult = { + FunctionCall( + functionName = freeFnName, + args = Seq(p, loc), + resultType = CCVoid, + sourceInfo = p.srcInfo + ) + } + + override def getExitAssertions(exitPreds : Seq[CCPredicate]) = Seq() + + // ACSL stuff, these should be refactored to not require a heap term + override def getACSLPreStateHeapTerm( + acslContext : ACSLTranslator.FunctionContext) : ITerm = ??? + override def getACSLPostStateHeapTerm( + acslContext : ACSLTranslator.FunctionContext) : ITerm = ??? + + override def batchAlloc(o : CCTerm, + size : ITerm, + arrayLoc : ArrayLocation.Value, + s : Seq[CCTerm]) : HeapOperationResult = { + ??? + } + + override def arrayRead(arr : CCTerm, + index : CCTerm, + s : Seq[CCTerm], + loc : CCTerm) : HeapOperationResult = { + ??? + } + + override def arrayWrite(arr : CCTerm, + index : CCTerm, + value : CCTerm, + s : Seq[CCTerm], + loc : CCTerm) : HeapOperationResult = { + ??? + } + + override def allocAndInitArray(arrayPtr : CCHeapArrayPointer, + size : ITerm, + initializers : mutable.Stack[ITerm], + s : Seq[CCTerm], + loc : CCTerm) : HeapOperationResult = { + ??? + } + + override def declUninitializedArray(arrayTyp : CCHeapArrayPointer, + size : Option[ITerm], + isGlobalOrStatic : Boolean, + forceNondetInit : Boolean, + s : Seq[CCTerm]) : HeapOperationResult = { + ??? + } +} \ No newline at end of file diff --git a/src/main/scala/tricera/params/TriCeraParameters.scala b/src/main/scala/tricera/params/TriCeraParameters.scala index 6dd15aa7..9f531c91 100644 --- a/src/main/scala/tricera/params/TriCeraParameters.scala +++ b/src/main/scala/tricera/params/TriCeraParameters.scala @@ -58,6 +58,7 @@ class TriCeraParameters extends GlobalParameters { var logPPLevel : Int = 0 // 0: quiet, 1: errors only, 2: errors + warnings var cPreprocessor : Boolean = false + var cPreprocessorLight : Boolean = false var dumpSimplifiedClauses : Boolean = false @@ -107,6 +108,8 @@ class TriCeraParameters extends GlobalParameters { var splitProperties : Boolean = false var useArraysForHeap : Boolean = false + var determinizeInput : Boolean = false + var invEncoding : Option[String] = None var heapModel : TriCeraParameters.HeapModel = TriCeraParameters.NativeHeap @@ -160,6 +163,7 @@ class TriCeraParameters extends GlobalParameters { logPPLevel = (ppLogOption drop 7).toInt; parseArgs(rest) case "-noPP" :: rest => noPP = true; parseArgs(rest) case "-cpp" :: rest => cPreprocessor = true; parseArgs(rest) + case "-cppLight" :: rest => cPreprocessorLight = true; parseArgs(rest) case "-dumpClauses" :: rest => printIntermediateClauseSets = true; parseArgs(rest) case "-dumpSimplified" :: rest => dumpSimplifiedClauses = true; parseArgs(rest) case "-sp" :: rest => smtPrettyPrint = true; parseArgs(rest) @@ -178,6 +182,13 @@ class TriCeraParameters extends GlobalParameters { parseArgs(rest) case "-mathArrays" :: rest => useArraysForHeap = true; parseArgs(rest) + case invEnc :: rest if (invEnc.startsWith("-invEncoding")) => + val parts = invEnc.split(":", 2) + invEncoding = Some(if (parts.length > 1) parts(1) else "RW") + determinizeInput = true + useArraysForHeap = true + parseArgs(rest) + case "-abstract" :: rest => templateBasedInterpolation = true; parseArgs(rest) case "-abstractPO" :: rest => { portfolio = GlobalParameters.Portfolio.Template @@ -344,6 +355,8 @@ class TriCeraParameters extends GlobalParameters { |-h, --help Show this information |-v, --version Print version number |-arithMode:t Integer semantics: math (default), ilp32, lp64, llp64 + |-mathArrays Use mathematical arrays for modeling program arrays (ignores memsafety properties) + |-invEncoding[:t] Use an invariant-based heap encoding, where t is the encoding type (R, RW (default)) |-t:time Set timeout (in seconds) |-cex Show textual counterexamples |-dotCEX Output counterexample in dot format @@ -364,6 +377,8 @@ class TriCeraParameters extends GlobalParameters { | predicate with 'p1' or 'p2' in its name |-m:func Use function func as entry point (default: main) |-cpp Execute the C preprocessor (cpp) on the input file first, this will produce filename.i + |-cppLight Same as -cpp but does not include system header files and builtin macros. + | I.e., -nostdinc -undef |-forceNondetInit Initialize static and global variables to non-deterministic values. |Checked properties: