local_bitvector_analysist: track whether an object may be alive

A local variable is alive if it has been declared and not yet been
marked dead.

Co-authored-by: Remi Delmas <[email protected]>

Author: tautschnig

regression/goto-instrument/show-local-bitvector-analysis1/main.c

@@ -0,0 +1,18 @@
+int foo(int i)
+{
+  int x;
+  if(x > 0)
+  {
+    int i;
+  }
+  else
+  {
+    int j;
+  }
+  return i;
+}
+
+int main()
+{
+  foo(42);
+}

regression/goto-instrument/show-local-bitvector-analysis1/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-local-bitvector-analysis
+activate-multi-line-match
+\*\*\*\* file main.c line 7 function foo\n(\n|.)*\s+foo::i: \+unknown\n(\n|.)*\n\s+// \d+ file main.c line 7 function foo\n\s+DEAD foo::1::1::i
+\*\*\*\* file main.c line 7 function foo\n(\n|.)*\s+foo::1::2::j: \+unknown\n(\n|.)*\n\s+// \d+ file main.c line 7 function foo\n\s+DEAD foo::1::1::i
+\*\*\*\* file main.c line 7 function foo\n(\n|.)*\s+foo::1::x: \+uninitialized\+maybe_alive\n(\n|.)*\n\s+// \d+ file main.c line 7 function foo\n\s+DEAD foo::1::1::i
+\*\*\*\* file main.c line 7 function foo\n(\n|.)*\s+foo::1::1::i: \+uninitialized\+maybe_alive\n(\n|.)*\n\s+// \d+ file main.c line 7 function foo\n\s+DEAD foo::1::1::i
+\*\*\*\* file main.c line 11 function foo\n(\n|.)*\s+foo::i: \+unknown\n(\n|.)*\n\s+// \d+ file main.c line 11 function foo\n\s+DEAD foo::1::2::j
+\*\*\*\* file main.c line 11 function foo\n(\n|.)*\s+foo::1::2::j: \+uninitialized\+maybe_alive\n(\n|.)*\n\s+// \d+ file main.c line 11 function foo\n\s+DEAD foo::1::2::j
+\*\*\*\* file main.c line 11 function foo\n(\n|.)*\s+foo::1::x: \+uninitialized\+maybe_alive\n(\n|.)*\n\s+// \d+ file main.c line 11 function foo\n\s+DEAD foo::1::2::j
+\*\*\*\* file main.c line 11 function foo\n(\n|.)*\s+foo::1::1::i: \+unknown\n(\n|.)*\n\s+// \d+ file main.c line 11 function foo\n\s+DEAD foo::1::2::j
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+\*\*\*\* file main.c line 13 function foo\n.*maybe_alive(\n|.)*END_FUNCTION

src/analyses/local_bitvector_analysis.cpp

@@ -35,6 +35,8 @@ void local_bitvector_analysist::flagst::print(std::ostream &out) const
     out << "+static_lifetime";
   if(is_integer_address())
     out << "+integer_address";
+  if(is_maybe_alive())
+    out << "+maybe_alive";
 }
 
 bool local_bitvector_analysist::merge(points_tot &a, points_tot &b)
@@ -229,6 +231,14 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
     else
       return flagst::mk_unknown();
   }
+  else if(rhs.id() == ID_decl)
+  {
+    return flagst::mk_uninitialized() | flagst::mk_maybe_alive();
+  }
+  else if(rhs.id() == ID_dead)
+  {
+    return flagst::mk_uninitialized();
+  }
   else
     return flagst::mk_unknown();
 }
@@ -274,18 +284,12 @@ void local_bitvector_analysist::build()
 
     case DECL:
       assign_lhs(
-        instruction.decl_symbol(),
-        exprt(ID_uninitialized),
-        loc_info_src,
-        loc_info_dest);
+        instruction.decl_symbol(), exprt(ID_decl), loc_info_src, loc_info_dest);
       break;
 
     case DEAD:
       assign_lhs(
-        instruction.dead_symbol(),
-        exprt(ID_uninitialized),
-        loc_info_src,
-        loc_info_dest);
+        instruction.dead_symbol(), exprt(ID_dead), loc_info_src, loc_info_dest);
       break;
 
     case FUNCTION_CALL:

src/analyses/local_bitvector_analysis.h

@@ -59,14 +59,15 @@ class local_bitvector_analysist
     // the bits for the "bitvector analysis"
     enum bitst
     {
-      B_unknown=1<<0,
-      B_uninitialized=1<<1,
-      B_uses_offset=1<<2,
-      B_dynamic_local=1<<3,
-      B_dynamic_heap=1<<4,
-      B_null=1<<5,
-      B_static_lifetime=1<<6,
-      B_integer_address=1<<7
+      B_unknown = 1 << 0,
+      B_uninitialized = 1 << 1,
+      B_uses_offset = 1 << 2,
+      B_dynamic_local = 1 << 3,
+      B_dynamic_heap = 1 << 4,
+      B_null = 1 << 5,
+      B_static_lifetime = 1 << 6,
+      B_integer_address = 1 << 7,
+      B_maybe_alive = 1 << 8
     };
 
     explicit flagst(const bitst _bits):bits(_bits)
@@ -162,6 +163,16 @@ class local_bitvector_analysist
       return (bits&B_integer_address)!=0;
     }
 
+    static flagst mk_maybe_alive()
+    {
+      return flagst(B_maybe_alive);
+    }
+
+    bool is_maybe_alive() const
+    {
+      return (bits & B_maybe_alive) != 0;
+    }
+
     void print(std::ostream &) const;
 
     flagst operator|(const flagst other) const