Merge pull request #8091 from thomasspriggs/tas/fix_goto_decls

Add support for variables entering scope via a goto

regression/cbmc/declaration-goto/issue7997.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+extern void __VERIFIER_assume(int cond);
+extern int __VERIFIER_nondet_int(void);
+
+int main(void)
+{
+  if(__VERIFIER_nondet_int())
+    goto switch_2_1;
+  int tmp_ndt_4 = __VERIFIER_nondet_int();
+  __VERIFIER_assume(__VERIFIER_nondet_int());
+  __VERIFIER_assume(tmp_ndt_4 == 1);
+switch_2_1:
+  assert(tmp_ndt_4 > 0);
+  return 0;
+}

regression/cbmc/declaration-goto/issue7997.desc

@@ -0,0 +1,12 @@
+CORE
+issue7997.c
+--trace
+\[main\.assertion\.1\] line \d+ assertion tmp_ndt_4 \> 0\: FAILURE
+return_value___VERIFIER_nondet_int=\-?[1-9]\d*
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+The assertion should be falsifiable when `goto switch_2_1` introduces
+`tmp_ndt_4` to the scope without initialising it.

regression/cbmc/declaration-goto/multiple_goto_single_label.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+extern void __VERIFIER_assume(int cond);
+
+int main(void)
+{
+  int l = 2;
+  int if_condition1;
+  if(if_condition1)
+  {
+    unsigned int j = 42;
+    l = 3;
+    goto merge_point;
+  }
+  int if_condition2;
+  if(if_condition2)
+  {
+    l = 4;
+    unsigned int k = 24;
+    goto merge_point;
+  }
+  int i = 3;
+  int m = 9;
+
+merge_point:
+  assert(i == 3 || m == 9 || l == 3);
+  assert(i == 3 || m == 9 || l == 4);
+  return 0;
+}

regression/cbmc/declaration-goto/multiple_goto_single_label.desc

@@ -0,0 +1,12 @@
+CORE
+multiple_goto_single_label.c
+
+\[main\.assertion\.1\] line \d+ assertion i \=\= 3 \|\| m \=\= 9 \|\| l \=\= 3\: FAILURE
+\[main\.assertion\.2\] line \d+ assertion i \=\= 3 \|\| m \=\= 9 \|\| l \=\= 4\: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Test for the case where there are multiple gotos which target the same label
+and both introduce variables into the scope.

regression/cbmc/declaration-goto/re-enter_scope.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+extern void __VERIFIER_assume(int cond);
+
+int main(void)
+{
+  int if_condition;
+  if(if_condition)
+  {
+    unsigned int i = 42;
+    goto j_scope;
+  i_scope:
+    assert(i == 42);
+    return 0;
+  }
+  int j = 3;
+  assert(j == 3);
+
+j_scope:
+  assert(j == 3);
+  if(if_condition)
+    goto i_scope;
+  return 0;
+}

regression/cbmc/declaration-goto/re-enter_scope.desc

@@ -0,0 +1,13 @@
+CORE
+re-enter_scope.c
+
+\[main\.assertion\.1\] line 13 assertion i \=\= 42\: FAILURE
+\[main\.assertion\.2\] line 17 assertion j \=\= 3\: SUCCESS
+\[main\.assertion\.3\] line 20 assertion j \=\= 3\: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Test that if execution re-enters a scope via a goto the pre-existing variable
+becomes non-det.

regression/cbmc/destructors/compound_literal.desc

@@ -2,21 +2,21 @@ CORE
 main.c
 --unwind 10 --show-goto-functions --no-standard-checks
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*8: END_FUNCTION
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-       // 49 file main.c line 44 function main
-       DEAD main::1::newAlloc0
-       // 50 file main.c line 44 function main
-       DEAD main::1::pc
-       // 51 file main.c line 44 function main
-       DEAD main::$tmp::literal
-       // 52 file main.c line 45 function main
-    8: END_FUNCTION
+        // 57 file main.c line 44 function main
+        DEAD main::1::newAlloc0
+        // 58 file main.c line 44 function main
+        DEAD main::1::pc
+        // 59 file main.c line 44 function main
+        DEAD main::$tmp::literal
+        // 60 file main.c line 45 function main
+     9: END_FUNCTION
 
 This asserts that when you've created a compound literal that both temp and real
 variable gets killed.

regression/cbmc/destructors/enter_lexical_block.desc

@@ -2,32 +2,34 @@ CORE
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*GOTO 3
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*ASSIGN going_to::nested_if := true[\s]*(?P>comment_block)[\s]*.*GOTO 3
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-       // 37 file main.c line 36 function main
-    5: DECL main::1::2::2::newAlloc4 : struct tag-test
-       // 38 file main.c line 36 function main
+       // 41 file main.c line 36 function main
+    6: DECL main::1::2::2::newAlloc4 : struct tag-test
+       // 42 file main.c line 36 function main
        ASSIGN main::1::2::2::newAlloc4 := { 4 }
-       // 39 file main.c line 37 function main
+       // 43 file main.c line 37 function main
        DECL main::1::2::2::newAlloc6 : struct tag-test
-       // 40 file main.c line 37 function main
+       // 44 file main.c line 37 function main
        ASSIGN main::1::2::2::newAlloc6 := { 6 }
-       // 41 file main.c line 38 function main
+       // 45 file main.c line 38 function main
        DECL main::1::2::2::newAlloc7 : struct tag-test
-       // 42 file main.c line 38 function main
+       // 46 file main.c line 38 function main
        ASSIGN main::1::2::2::newAlloc7 := { 7 }
-       // 43 file main.c line 39 function main
+       // 47 file main.c line 39 function main
        DEAD main::1::2::2::newAlloc7
-       // 44 file main.c line 39 function main
+       // 48 file main.c line 39 function main
        DEAD main::1::2::2::newAlloc6
-       // 45 file main.c line 39 function main
+       // 49 file main.c line 39 function main
        DEAD main::1::2::2::newAlloc4
-       // 46 file main.c line 39 function main
+       // 50 file main.c line 39 function main
+       ASSIGN going_to::nested_if := true
+       // 51 file main.c line 39 function main
        GOTO 3
 
 This asserts that when the GOTO is going into a lexical block that destructors

regression/cbmc/symex_should_filter_value_sets/test.desc

@@ -9,8 +9,8 @@ main::1::c3!0@1#. = 1
 main::1::c4!0@1#. = 1
 main::1::c5!0@1#. = 1
 main::1::c6!0@1#. = 1
-main::1::c7!0@1#. = 1
-main::1::c8!0@1#. = 1
+main::1::c7!0@2#. = 1
+main::1::c8!0@2#. = 1
 main::1::c9!0@1#. = 1
 main::1::c10!0@1#. = 1
 main::1::c11!0@1#. = 1

src/goto-programs/Makefile

@@ -5,7 +5,6 @@ SRC = allocate_objects.cpp \
       class_identifier.cpp \
       compute_called_functions.cpp \
       destructor.cpp \
-      destructor_tree.cpp \
       elf_reader.cpp \
       ensure_one_backedge_per_target.cpp \
       format_strings.cpp \
@@ -60,6 +59,7 @@ SRC = allocate_objects.cpp \
       rewrite_union.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \
+      scope_tree.cpp \
       set_properties.cpp \
       show_goto_functions.cpp \
       show_goto_functions_json.cpp \

src/goto-programs/goto_clean_expr.cpp

@@ -53,7 +53,7 @@ symbol_exprt goto_convertt::make_compound_literal(
   if(!new_symbol.is_static_lifetime)
   {
     code_deadt code_dead(result);
-    targets.destructor_stack.add(std::move(code_dead));
+    targets.scope_stack.add(std::move(code_dead), {});
   }
 
   return result;