Merge pull request #141 from diffblue/bugfix/simplify-lhs

Bugfix for LHS simplification

Author: thk123

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 --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 --arrays --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,23 @@
+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 --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 --arrays --pointers --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,21 @@
+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
+  // This will be addressed by diffblue/cbmc-toyota#118
+  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 --arrays --pointers"
+array\[0l\] = 5
+array\[\(signed long int\)nondet\] = 6
+new_array\[1l\] = 7