Merge pull request #5472 from martin-cs/refactor/VSD-with-history-2

Variable sensitivity domain

Author: NlightNFotis

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;