Better property handling (#10)

* Start properties refactor.
The goal is to refactor assertions so that each one corresponds
to a property. Properties can be toggled - this allowed finer
grained control over which properties TriCera checks. After the
refactor is complete, it should also be clear which property an
input program does not satisfy.
- Added properties package.
- Refactored Main to collect properties from YAML files in a more
  structured way.
- Started refactoring of existing memsafety properties.

* More work on memvalid-free.
Non-heap allocated pointers now throw an error as soon as they
are tried to be freed. They are no longer automatically freed -
this was done for memvalid-track, but that will now be implemented
in another way, so freeing non-heap pointers is no longer
necessary.
Also added regression tests for memvalid-free.

* Adds valid-deref tests.

* Properties - naming and documentation

* Adds support for memcleanup property.

* Adds memcleanup regression tests.

* More property related improvements.
- Adds CLI options for specifying properties.
- Fixes valid-deref properties always being added.
- Formatting of CLI help text.

* Bug fixes in properties and solution printing, updates regression tests.
- Fixes the regression tests based on properties, removing
  redundant ones.
- Fixes a bug where valid-cleanup ghost variable was initialized
  twice.
- Fixes a bug in printing contracts for void functions.
- Makes printing of solutions more robust by replacing
  string replacement with term rewriting.

* Refactor YAML parser to its own class.

* Warning message when parsing fails.

* Adds support for splitting properties, and many other changes.
- Fixes how certain properties are checked.
- It is now possible to check each property separately.
- Updates regression tests.
- Many other changes related to properties.

* Add missing regression test.

* Minor change in error output, regression tests

regression-tests/acsl-contracts/Answers

@@ -30,15 +30,12 @@ contract10.hcc
 SAFE
 
 contract11.hcc
-Warning: enabling heap model
 SAFE
 
 contract12.hcc
-Warning: enabling heap model
 SAFE
 
 contract13.hcc
-Warning: enabling heap model
 UNSAFE
 
 contract14.hcc
@@ -48,7 +45,6 @@ contract15.hcc
 SAFE
 
 contract16.hcc
-Warning: enabling heap model
 SAFE
 
 contract17.hcc
@@ -58,11 +54,9 @@ contract18.hcc
 UNSAFE
 
 contract19.hcc
-Warning: enabling heap model
 SAFE
 
 contract20.hcc
-Warning: enabling heap model
 UNSAFE
 
 contract21.hcc
@@ -72,23 +66,18 @@ contract22.hcc
 UNSAFE
 
 contract23.hcc
-Warning: enabling heap model
 UNSAFE
 
 contract24.hcc
-Warning: enabling heap model
 UNSAFE
 
 contract25.hcc
-Warning: enabling heap model
 SAFE
 
 contract26.hcc
-Warning: enabling heap model
 SAFE
 
 contract27.hcc
-Warning: enabling heap model
 SAFE
 
 struct-field-access-1-true.hcc

regression-tests/horn-hcc-heap/memtrack-04.yml → regression-tests/acsl-standalone/getptr_safe.yml

@@ -1,11 +1,10 @@
 format_version: '2.0'
 
-input_files: 'memtrack-04.c'
+input_files: 'getptr_safe.c'
 
 properties:
   - property_file: ../properties/valid-memsafety.prp
     expected_verdict: true
-    subproperty: valid-memtrack
 
 options:
   language: C

regression-tests/horn-hcc-heap/memtrack-05.yml → regression-tests/acsl-standalone/getptr_unsafe.yml

@@ -1,11 +1,11 @@
 format_version: '2.0'
 
-input_files: 'memtrack-05.c'
+input_files: 'getptr_unsafe.c'
 
 properties:
   - property_file: ../properties/valid-memsafety.prp
     expected_verdict: false
-    subproperty: valid-memtrack
+    subproperty: valid-deref
 
 options:
   language: C

regression-tests/acsl-standalone/runtests

@@ -24,6 +24,6 @@ TESTS="inc_safe.c \
 for name in $TESTS; do
     echo
     echo $name
-    $LAZABS "$@" $name 2>&1 | grep -v 'at '
+    $LAZABS "$@" $name -memsafety -reachsafety
 done
 

regression-tests/horn-bv/Answers

@@ -1,7 +1,6 @@
 
 nonlinear2.hcc
 Warning: no definition of function "nondet" available
-UNSAFE
 
 -----------------------------------------------------------------
 Init:
@@ -66,8 +65,9 @@ Final:
   main((-447365120).\as[signed bv[32]], 11.\as[signed bv[32]])   
 -----------------------------------------------------------------
 Failed assertion:
-false :- main(f:5, i:6), f:5 < 1 | i:6 < 1. (line:13 col:3)
+false :- main(f:5, i:6), f:5 < 1 | i:6 < 1. (line:13 col:3) (property: user-assertion)
 
+UNSAFE
 
 ../horn-hcc/loop1.hcc
 Warning: entry function "main" not found

regression-tests/horn-contracts/Answers

@@ -1,6 +1,5 @@
 
 contract1.hcc
-SAFE
 
 Inferred ACSL annotations
 ================================================================================
@@ -11,9 +10,9 @@ Inferred ACSL annotations
 */
 ================================================================================
 
+SAFE
 
 contract2.hcc
-SAFE
 
 Inferred ACSL annotations
 ================================================================================
@@ -24,9 +23,9 @@ Inferred ACSL annotations
 */
 ================================================================================
 
+SAFE
 
 contract2b.hcc
-UNSAFE
 
 ------------------
 Init:
@@ -51,11 +50,11 @@ Final:
   main_2(-4, 5)   
 ------------------
 Failed assertion:
-false :- main_2(g:2, y:14), g:2 < 0. (line:18 col:3)
+false :- main_2(g:2, y:14), g:2 < 0. (line:18 col:3) (property: user-assertion)
 
+UNSAFE
 
 contract3.hcc
-SAFE
 
 Inferred ACSL annotations
 ================================================================================
@@ -66,9 +65,9 @@ Inferred ACSL annotations
 */
 ================================================================================
 
+SAFE
 
 takeuchi.hcc
-SAFE
 
 Inferred ACSL annotations
 ================================================================================
@@ -79,9 +78,9 @@ Inferred ACSL annotations
 */
 ================================================================================
 
+SAFE
 
 assert.hcc
-SAFE
 
 Inferred ACSL annotations
 ================================================================================
@@ -92,9 +91,9 @@ Inferred ACSL annotations
 */
 ================================================================================
 
+SAFE
 
 fib.hcc
-UNSAFE
 
 ---------------
 Init:
@@ -109,8 +108,11 @@ Final:
  main12_3_1(8) 
 ---------------
 Failed assertion:
-false :- main12_3_1(x:12), x:12 != 0. (line:14 col:3)
+false :- main12_3_1(x:12), x:12 != 0. (line:14 col:3) (property: user-assertion)
 
+UNSAFE
 
 stackptr.hcc
-Warning: enabling heap model
+tricera.concurrency.ccreader.CCExceptions$TranslationException: Function contracts are currently not supported together with stack pointers (10:5)
+(error "Function contracts are currently not supported together with stack pointers (10:5)")
+Other Error: Function contracts are currently not supported together with stack pointers (10:5)

regression-tests/horn-hcc-2/Answers

@@ -38,7 +38,6 @@ Warning: entry function "main" not found
 SAFE
 
 lazy-and-or-bug.hcc
-UNSAFE
 
 ------------------------------------
 Init:
@@ -62,6 +61,7 @@ Init:
 Final:
      A10_7(1)         main(1, 1)    
 ------------------------------------
+UNSAFE
 
 channels.hcc
 Warning: entry function "main" not found
@@ -73,7 +73,6 @@ SAFE
 
 channels-2b.hcc
 Warning: entry function "main" not found
-UNSAFE
 
 ------------------------
 Init:
@@ -88,6 +87,7 @@ Init:
 Final:
  A7_10(42)   B(42, -10) 
 ------------------------
+UNSAFE
 
 channels-3.hcc
 tricera.concurrency.ccreader.CCExceptions$TranslationException: Cannot execute Receive(d) and Send(c) in one step
@@ -100,7 +100,6 @@ SAFE
 
 duration2.hcc
 Warning: enabling time
-UNSAFE
 
 ------------------------------------------------------
 Init:
@@ -130,14 +129,14 @@ Init:
 Final:
    A_2(0, 1, 0, 0, 0, 0)    main_1(0, 1, 0, 0, 0, 0)  
 ------------------------------------------------------
+UNSAFE
 
 duration3.hcc
 Warning: enabling time
 SAFE
 
 duration3b.hcc
 Warning: enabling time
-UNSAFE
 
 ------------------------------------------------
 Init:
@@ -167,14 +166,14 @@ Init:
 Final:
    B_2(0, 1, 0, 0, 0)    main9_15_0(0, 1, 0, 0) 
 ------------------------------------------------
+UNSAFE
 
 duration3c.hcc
 Warning: enabling time
 SAFE
 
 duration3d.hcc
 Warning: enabling time
-UNSAFE
 
 ----------------------------------------------
 Init:
@@ -206,14 +205,14 @@ Delay: 1.0
 Final:
    B_2(0, 1, 0, -1)      main9_15_0(0, 1, 0)  
 ----------------------------------------------
+UNSAFE
 
 nonlinear1.hcc
 Warning: no definition of function "nondet" available
 SAFE
 
 nonlinear2.hcc
 Warning: no definition of function "nondet" available
-UNSAFE
 
 ----------------
 Init:
@@ -228,14 +227,14 @@ Final:
  main12_7(2, 4) 
 ----------------
 Failed assertion:
-false :- main12_7(x:7, y:10). (line:13 col:5)
+false :- main12_7(x:7, y:10). (line:13 col:5) (property: user-assertion)
 
+UNSAFE
 
 typedef1.hcc
 SAFE
 
 switch1.hcc
-UNSAFE
 
 ----------------
 Init:
@@ -250,8 +249,9 @@ Final:
    main(0, 0)   
 ----------------
 Failed assertion:
-false :- main(x:4, y:5), y:5 < 1. (line:19 col:3)
+false :- main(x:4, y:5), y:5 < 1. (line:19 col:3) (property: user-assertion)
 
+UNSAFE
 
 switch2.hcc
 Warning: no definition of function "nondet" available