Made ai_simplify perform a partial simplifcation

thk123 · thk123 · commit de2f979940b3 · 2017-06-15T18:58:39.000+01:00
If the ai_simplify is not able to resolve the expression to a constant,
it tries to simplify recursively any child operations. For example,
given a int i that is know to be 1, and an unknown (top) array a, it
would convert a[i] to a[1].
diff --git a/regression/goto-analyzer-simplify/Makefile b/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
diff --git a/regression/goto-analyzer-simplify/chain.sh b/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
diff --git a/regression/goto-analyzer-simplify/partial-simplify-array/main.c b/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];
+}
diff --git a/regression/goto-analyzer-simplify/partial-simplify-array/test.desc b/regression/goto-analyzer-simplify/partial-simplify-array/test.desc
@@ -0,0 +1,5 @@
+CORE
+main.c
+"--variable --arrays"
+
+arr\[0l\]
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
@@ -275,8 +275,18 @@ bool variable_sensitivity_domaint::ai_simplify(
   sharing_ptrt<abstract_objectt> res=abstract_state.eval(condition, ns);
   exprt c=res->to_constant();
 
-  if(c.id()==ID_nil)  // TODO : simplification within an expression
-    return true;
+  if(c.id()==ID_nil)
+  {
+    bool no_simplification=true;
+
+    // Try to simplify recursively any child operations
+    for(exprt &op : condition.operands())
+    {
+      no_simplification&=ai_simplify(op, ns);
+    }
+
+    return no_simplification;
+  }
   else
   {
     bool condition_changed=(condition!=c);

-Original file line number
+Diff line change
@@ @@ -0,0 +1,5 @@ @@
 +CORE
 +main.c
 +"--variable --arrays"
++
 +arr\[0l\]