Invariant-based heap model

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

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.
+}

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[]"
   },

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

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

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

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

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: ""