Treat local dirty variables as shared ones

regression/cbmc-concurrency/dirty_local1/main.c

@@ -0,0 +1,15 @@
+int * global_ptr;
+
+void f()
+{
+  *global_ptr=42;
+}
+
+int main()
+{
+  int a=0;
+  global_ptr=&a;
+  __CPROVER_ASYNC_1: f();
+  assert(a==0);
+}
+

regression/cbmc-concurrency/dirty_local1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-concurrency/dirty_local2/main.c

@@ -0,0 +1,98 @@
+typedef unsigned bool;
+
+#define true 1
+#define false 0
+
+typedef char Register;
+
+enum RegisterId
+{
+  SIGNAL_REG_ID = 0,
+  DATA_A_REG_ID = 1,
+
+  REG_NR = 2
+};
+
+typedef enum RegisterId RegisterId;
+
+struct Firmware;
+typedef void (*InterruptHandler)(struct Firmware *fw, RegisterId reg_id);
+
+struct Hardware
+{
+  struct Firmware* fw;
+
+  Register regs[REG_NR];
+  bool is_on;
+
+  InterruptHandler interrupt_handler;
+};
+
+Register read_data_register(struct Hardware *hw, RegisterId reg_id)
+{
+  if (!hw->is_on)
+    return '\0';
+
+  Register reg = hw->regs[reg_id];
+  hw->regs[SIGNAL_REG_ID] &= ~reg_id;
+
+  return reg;
+}
+
+void write_data_register(struct Hardware *hw, RegisterId reg_id, Register data)
+{
+  check_data_register(reg_id);
+
+  if (!hw->is_on)
+    return;
+
+  hw->regs[reg_id] = data;
+  hw->regs[SIGNAL_REG_ID] |= reg_id;
+
+  __CPROVER_ASYNC_1: hw->interrupt_handler(hw->fw, reg_id);
+}
+
+struct Firmware
+{
+  struct Hardware* hw;
+};
+
+void handle_interrupt(struct Firmware *fw, RegisterId reg_id)
+{
+  assert(reg_id == DATA_A_REG_ID);
+  read_data_register(fw->hw, DATA_A_REG_ID);
+}
+
+void poll(struct Firmware *fw)
+{
+  char byte;
+  if (byte == '\0')
+  {
+    enable_interrupts(fw->hw, handle_interrupt);
+    return;
+  }
+}
+
+void write_reg_a(struct Hardware *hw)
+{
+  write_data_register(hw, DATA_A_REG_ID, nondet_char());
+}
+
+int main(void)
+{
+  // trivial bug
+  assert(false);
+
+  struct Hardware hardware;
+  struct Hardware* hw = &hardware;
+
+  struct Firmware firmware;
+  struct Firmware* fw = &firmware;
+
+  firmware.hw = hw;
+  hardware.fw = fw;
+
+  __CPROVER_ASYNC_1: write_reg_a(hw);
+
+  return 0;
+}

regression/cbmc-concurrency/dirty_local2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-symex/goto_symex_state.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/prefix.h>
 
+#include <analyses/dirty.h>
+
 #include "goto_symex_state.h"
 
 /*******************************************************************\
@@ -31,7 +33,8 @@ goto_symex_statet::goto_symex_statet():
   depth(0),
   symex_target(NULL),
   atomic_section_id(0),
-  record_events(true)
+  record_events(true),
+  dirty(0)
 {
   threads.resize(1);
   new_frame();
@@ -640,17 +643,16 @@ bool goto_symex_statet::l2_thread_read_encoding(
   ssa_exprt &expr,
   const namespacet &ns)
 {
-  if(!record_events)
-    return false;
-
   // do we have threads?
   if(threads.size()<=1)
     return false;
 
   // is it a shared object?
+  assert(dirty!=0);
   const irep_idt &obj_identifier=expr.get_object_name();
   if(obj_identifier=="goto_symex::\\guard" ||
-     !ns.lookup(obj_identifier).is_shared())
+     (!ns.lookup(obj_identifier).is_shared() &&
+      !(*dirty)(obj_identifier)))
     return false;
 
   ssa_exprt ssa_l1=expr;
@@ -754,9 +756,18 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return true;
   }
 
-  // produce a fresh L2 name
   if(level2.current_names.find(l1_identifier)==level2.current_names.end())
     level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
+
+  // No event and no fresh index, but avoid constant propagation
+  if(!record_events)
+  {
+    set_ssa_indices(ssa_l1, ns, L2);
+    expr=ssa_l1;
+    return true;
+  }
+
+  // produce a fresh L2 name
   level2.increase_counter(l1_identifier);
   set_ssa_indices(ssa_l1, ns, L2);
   expr=ssa_l1;
@@ -792,9 +803,11 @@ bool goto_symex_statet::l2_thread_write_encoding(
     return false;
 
   // is it a shared object?
+  assert(dirty!=0);
   const irep_idt &obj_identifier=expr.get_object_name();
   if(obj_identifier=="goto_symex::\\guard" ||
-     !ns.lookup(obj_identifier).is_shared())
+     (!ns.lookup(obj_identifier).is_shared() &&
+      !(*dirty)(obj_identifier)))
     return false; // not shared
 
   // see whether we are within an atomic section

src/goto-symex/goto_symex_state.h

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target.h"
 
+class dirtyt;
+
 // central data structure: state
 class goto_symex_statet
 {
@@ -331,6 +333,7 @@ class goto_symex_statet
 
   void switch_to_thread(unsigned t);
   bool record_events;
+  const dirtyt * dirty;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H

src/goto-symex/memory_model_pso.cpp

@@ -51,19 +51,19 @@ bool memory_model_psot::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(is_shared_read(e1) || is_shared_write(e1));
-  assert(is_shared_read(e2) || is_shared_write(e2));
+  assert(e1->is_shared_read() || e1->is_shared_write());
+  assert(e2->is_shared_read() || e2->is_shared_write());
 
   // no po relaxation within atomic sections
   if(e1->atomic_section_id!=0 &&
      e1->atomic_section_id==e2->atomic_section_id)
     return false;
 
   // no relaxation if induced wsi
-  if(is_shared_write(e1) && is_shared_write(e2) &&
+  if(e1->is_shared_write() && e2->is_shared_write() &&
      address(e1)==address(e2))
     return false;
 
   // only read/read and read/write are maintained
-  return is_shared_write(e1);
+  return e1->is_shared_write();
 }

src/goto-symex/memory_model_sc.cpp

@@ -69,8 +69,8 @@ bool memory_model_sct::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(is_shared_read(e1) || is_shared_write(e1));
-  assert(is_shared_read(e2) || is_shared_write(e2));
+  assert(e1->is_shared_read() || e1->is_shared_write());
+  assert(e2->is_shared_read() || e2->is_shared_write());
 
   return false;
 }
@@ -99,10 +99,10 @@ void memory_model_sct::build_per_thread_map(
       e_it++)
   {
     // concurreny-related?
-    if(!is_shared_read(e_it) &&
-       !is_shared_write(e_it) &&
-       !is_spawn(e_it) &&
-       !is_memory_barrier(e_it)) continue;
+    if(!e_it->is_shared_read() &&
+       !e_it->is_shared_write() &&
+       !e_it->is_spawn() &&
+       !e_it->is_memory_barrier()) continue;
 
     dest[e_it->source.thread_nr].push_back(e_it);
   }
@@ -133,7 +133,7 @@ void memory_model_sct::thread_spawn(
       e_it!=equation.SSA_steps.end();
       e_it++)
   {
-    if(is_spawn(e_it))
+    if(e_it->is_spawn())
     {
       per_thread_mapt::const_iterator next_thread=
         per_thread_map.find(++next_thread_id);
@@ -238,7 +238,7 @@ void memory_model_sct::program_order(
         e_it!=events.end();
         e_it++)
     {
-      if(is_memory_barrier(*e_it))
+      if((*e_it)->is_memory_barrier())
          continue;
 
       if(previous==equation.SSA_steps.end())

src/goto-symex/memory_model_tso.cpp

@@ -72,16 +72,16 @@ bool memory_model_tsot::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(is_shared_read(e1) || is_shared_write(e1));
-  assert(is_shared_read(e2) || is_shared_write(e2));
+  assert(e1->is_shared_read() || e1->is_shared_write());
+  assert(e2->is_shared_read() || e2->is_shared_write());
 
   // no po relaxation within atomic sections
   if(e1->atomic_section_id!=0 &&
      e1->atomic_section_id==e2->atomic_section_id)
     return false;
 
   // write to read program order is relaxed
-  return is_shared_write(e1) && is_shared_read(e2);
+  return e1->is_shared_write() && e2->is_shared_read();
 }
 
 /*******************************************************************\
@@ -120,7 +120,7 @@ void memory_model_tsot::program_order(
         e_it!=events.end();
         e_it++)
     {
-      if(is_memory_barrier(*e_it))
+      if((*e_it)->is_memory_barrier())
         continue;
 
       event_listt::const_iterator next=e_it;
@@ -135,30 +135,30 @@ void memory_model_tsot::program_order(
           e_it2!=events.end();
           e_it2++)
       {
-        if((is_spawn(*e_it) && !is_memory_barrier(*e_it2)) ||
-           is_spawn(*e_it2))
+        if(((*e_it)->is_spawn() && !(*e_it2)->is_memory_barrier()) ||
+           (*e_it2)->is_spawn())
         {
           add_constraint(
             equation,
             before(*e_it, *e_it2),
             "po",
             (*e_it)->source);
 
-          if(is_spawn(*e_it2))
+          if((*e_it2)->is_spawn())
             break;
           else
             continue;
         }
 
-        if(is_memory_barrier(*e_it2))
+        if((*e_it2)->is_memory_barrier())
         {
           const codet &code=to_code((*e_it2)->source.pc->code);
 
-          if(is_shared_read(*e_it) &&
+          if((*e_it)->is_shared_read() &&
              !code.get_bool(ID_RRfence) &&
              !code.get_bool(ID_RWfence))
             continue;
-          else if(is_shared_write(*e_it) &&
+          else if((*e_it)->is_shared_write() &&
              !code.get_bool(ID_WRfence) &&
              !code.get_bool(ID_WWfence))
             continue;
@@ -184,7 +184,7 @@ void memory_model_tsot::program_order(
         }
         else if(program_order_is_relaxed(*e_it, *e_it2))
         {
-          if(is_shared_read(*e_it2))
+          if((*e_it2)->is_shared_read())
             cond=mb_guard_r;
           else
             cond=mb_guard_w;