Variable sensitivity domain

regression/goto-analyzer-simplify/Makefile

@@ -0,0 +1,31 @@
+
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		rm -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-analyzer-simplify/chain.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+src_dir=../../../src
+
+goto_analyzer=$src_dir/goto-analyzer/goto-analyzer
+
+options=$1
+file_name=${2%.c}
+
+echo options: $options
+echo file name : $file_name
+
+$goto_analyzer $file_name.c $options --simplify $file_name_simp.out
+$goto_analyzer $file_name_simp.out --show-goto-functions

regression/goto-analyzer-simplify/partial-simplify-array/main.c

@@ -0,0 +1,7 @@
+extern int arr[];
+
+void main()
+{
+  int index = 0;
+  int j = arr[index];
+}

regression/goto-analyzer-simplify/partial-simplify-array/test.desc

@@ -0,0 +1,5 @@
+CORE
+main.c
+"--variable-sensitivity --vsd-arrays"
+
+arr\[0l\]

regression/goto-analyzer-simplify/simplify-complex-expression/main.c

@@ -0,0 +1,12 @@
+int nondet_int(void);
+
+int main(void)
+{
+  int r = nondet_int();
+  r = r + 1;
+  if(r == 2)
+  {
+    return 1;
+  }
+  return 0;
+}

regression/goto-analyzer-simplify/simplify-complex-expression/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--variable-sensitivity
+r == 2
+^SIGNAL=0$
+^EXIT=6$
+--
+--
+
+Checks for a bug that occurred while changing the simplifier,
+where a variable would be replaced by the RHS of its last assignment,
+even if the value of that expression had changed since then;
+Most egregiously when the RHS contained the symbol on the LHS (thus leading
+to a recursive definition).

regression/goto-analyzer-simplify/simplify-lhs-array-index/main.c

@@ -0,0 +1,15 @@
+void main()
+{
+  int arr[4] = {1, 2, 3, 4};
+
+  // No simplification
+  arr[0] = 1;
+
+  // Can simplify
+  int constant = 1;
+  arr[constant] = 2;
+
+  // No simplification
+  int nondet;
+  arr[nondet] = 3;
+}

regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--variable-sensitivity --vsd-arrays"
+
+arr\[0l\] =
+arr\[1l\] =
+arr\[\(signed long int\)nondet\] =

regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/main.c

@@ -0,0 +1,33 @@
+void main()
+{
+  int symbol_a;
+  int symbol_b;
+
+  int nondet;
+  int *nondet_pointer;
+  if(nondet > 0)
+  {
+    nondet_pointer = &symbol_a;
+  }
+  else
+  {
+    nondet_pointer = &symbol_b;
+  }
+
+  int *arr[] = {&symbol_a, &symbol_b, nondet_pointer};
+
+  // Simplify the pointer
+  *arr[0] = 1;
+
+  // Simplify index and the pointer
+  int constant1 = 1;
+  *arr[constant1] = 2;
+
+  // Simplify the index but not the pointer
+  int constant2 = 2;
+  *arr[constant2] = 3;
+
+  // No simplification
+  int nondet_index;
+  *arr[nondet_index] = 4;
+}

regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--variable-sensitivity --vsd-arrays --vsd-pointers"
+
+symbol_a = 1
+symbol_b = 2
+\*arr\[2l\] = 3;
+\*arr\[\(signed long int\)nondet_index\] = 4;

regression/goto-analyzer-simplify/simplify-lhs-dereference/main.c

@@ -0,0 +1,22 @@
+void main()
+{
+  int symbol;
+
+  int *pointer = &symbol;
+
+  // Simplify
+  *pointer = 5;
+
+  int nondet;
+  if(nondet > 0)
+  {
+    pointer = &nondet;
+  }
+  else
+  {
+    pointer = &symbol;
+  }
+
+  // No simplification
+  *pointer = 6;
+}

regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+"--variable-sensitivity --vsd-pointers"
+
+symbol = 5
+\*pointer = 6

regression/goto-analyzer-simplify/simplify-lhs-member/main.c

@@ -0,0 +1,42 @@
+struct test_struct
+{
+  int *pointer_component;
+  int array[5];
+};
+
+void main()
+{
+  int symbol;
+
+  struct test_struct value;
+
+  // Simplify a pointer inside a struct
+  int symbol;
+  value.pointer_component = &symbol;
+
+  // Simplify
+  *value.pointer_component = 5;
+
+  int nondet;
+  if(nondet > 0)
+  {
+    value.pointer_component = &nondet;
+  }
+  else
+  {
+    value.pointer_component = &symbol;
+  }
+
+  // No simplification
+  *value.pointer_component = 6;
+
+  // Simplify an array
+
+  // Can simplify
+  int constant = 1;
+  value.array[constant] = 2;
+
+  // No simplification
+  int nondet;
+  value.array[nondet] = 3;
+}

regression/goto-analyzer-simplify/simplify-lhs-member/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--variable-sensitivity --vsd-arrays --vsd-pointers --vsd-structs"
+
+symbol = 5
+\*value\.pointer_component = 6
+value\.array\[1l\] = 2
+value\.array\[\(signed long int\)nondet\] = 3

regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/main.c

@@ -0,0 +1,20 @@
+void main()
+{
+  int array[] = {1, 2, 3, 4, 5};
+
+  int *pointer = array;
+
+  // Simplify -> array[0] = 5
+  *pointer = 5;
+
+  int nondet;
+  pointer[nondet] = 6;
+
+  // TODO: Currently writing to an offset pointer sets the domain to top
+  // so recreate the variables to reign the domain back in
+  int new_array[] = {1, 2, 3, 4, 5};
+  int *new_pointer = new_array;
+
+  int constant = 1;
+  new_pointer[constant] = 7;
+}

regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+"--variable-sensitivity --vsd-arrays --vsd-pointers"
+array\[0l\] = 5
+array\[\(signed long int\)nondet\] = 6
+new_array\[1l\] = 7

regression/goto-analyzer-simplify/simplify-multiply-by-zero/main.c

@@ -0,0 +1,8 @@
+int nondet_int(void);
+
+int main(void)
+{
+  int K = nondet_int();
+  int x = 0;
+  return K * x;
+}

regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+"--variable-sensitivity"
+^SIGNAL=0$
+^EXIT=6$
+main#return_value = 0;
+--
+--
+Tests that a multiplication
+of variable*variable can be simplified
+if one of the variables can be evaluated to 0.

regression/goto-analyzer/constant_assertions_01/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int nondet_int(void);
+
+int main(int argc, char **argv)
+{
+  int x = nondet_int();
+  int y = nondet_int();
+
+  __CPROVER_assert(0, "0");
+  __CPROVER_assert(0 && 1, "0 && 1");
+  __CPROVER_assert(0 || 0, "0 || 0");
+  __CPROVER_assert(0 && x, "0 && x");
+  __CPROVER_assert(y && 0, "y && 0");
+
+  return 0;
+}

regression/goto-analyzer/constant_assertions_01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --variable-sensitivity
+^\[main.assertion.1\] line 10 0: FAILURE \(if reachable\)$
+^\[main.assertion.2\] line 11 0 && 1: FAILURE \(if reachable\)$
+^\[main.assertion.3\] line 12 0 || 0: FAILURE \(if reachable\)$
+^\[main.assertion.4\] line 13 0 && x: FAILURE \(if reachable\)$
+^\[main.assertion.5\] line 14 y && 0: FAILURE \(if reachable\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_assertions_02/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int nondet_int(void);
+
+int main(int argc, char **argv)
+{
+  int x = nondet_int();
+  int y = nondet_int();
+
+  __CPROVER_assert(1, "1");
+  __CPROVER_assert(0 || 1, "0 || 1");
+  __CPROVER_assert(1 && 1, "1 && 1");
+  __CPROVER_assert(1 || x, "1 || x");
+  __CPROVER_assert(y || 1, "y || 1");
+
+  return 0;
+}

regression/goto-analyzer/constant_assertions_02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --variable-sensitivity
+^\[main\.assertion\.1\] line 10 1: SUCCESS
+^\[main\.assertion\.2\] line 11 0 || 1: SUCCESS
+^\[main\.assertion\.3\] line 12 1 && 1: SUCCESS
+^\[main\.assertion\.4\] line 13 1 || x: SUCCESS
+^\[main\.assertion\.5\] line 14 y || 1: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_01/main.c

@@ -1,13 +1,13 @@
+#include <assert.h>
 
 int main()
 {
   int i, j=20;
-  
+
   if (j==20)
   {
     int x=1,y=2,z;
     z=x+y;
-    assert(z==3);
+    __CPROVER_assert(z == 3, "z==3");
   }
-
 }

regression/goto-analyzer/constant_propagation_01/test-vsd.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --simplify out.gb
+^EXIT=0$
+^SIGNAL=0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_02/main.c

@@ -3,10 +3,10 @@ int main()
 {
   int i=0, j=2;
 
-  if (i==0) 
+  if(i == 0)
   {
     i++;
     j++;
   }
-  assert(j!=3);
+  __CPROVER_assert(j != 3, "j!=3");
 }

regression/goto-analyzer/constant_propagation_02/test-vsd.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --simplify out.gb
+^EXIT=0$
+^SIGNAL=0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+--
+^warning: ignoring