Merge pull request #4346 from xbauch/doc/memory_model

Reword the read_from function and add documentation to memory_model

Author: petr-bauch

src/goto-symex/memory_model.cpp

@@ -13,29 +13,26 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
 
 #include <util/std_expr.h>
 
-memory_model_baset::memory_model_baset(const namespacet &_ns):
-  partial_order_concurrencyt(_ns),
-  var_cnt(0)
+memory_model_baset::memory_model_baset(const namespacet &_ns)
+  : partial_order_concurrencyt(_ns), var_cnt(0)
 {
 }
 
 memory_model_baset::~memory_model_baset()
 {
 }
 
-symbol_exprt memory_model_baset::nondet_bool_symbol(
-  const std::string &prefix)
+symbol_exprt memory_model_baset::nondet_bool_symbol(const std::string &prefix)
 {
   return symbol_exprt(
-    "memory_model::choice_"+prefix+std::to_string(var_cnt++),
-    bool_typet());
+    "memory_model::choice_" + prefix + std::to_string(var_cnt++), bool_typet());
 }
 
 bool memory_model_baset::po(event_it e1, event_it e2)
 {
   // within same thread
-  if(e1->source.thread_nr==e2->source.thread_nr)
-    return numbering[e1]<numbering[e2];
+  if(e1->source.thread_nr == e2->source.thread_nr)
+    return numbering[e1] < numbering[e2];
   else
   {
     // in general un-ordered, with exception of thread-spawning
@@ -49,83 +46,67 @@ void memory_model_baset::read_from(symex_target_equationt &equation)
   // make them match at least one
   // (internal or external) write.
 
-  for(address_mapt::const_iterator
-      a_it=address_map.begin();
-      a_it!=address_map.end();
-      a_it++)
+  for(const auto &address : address_map)
   {
-    const a_rect &a_rec=a_it->second;
-
-    for(event_listt::const_iterator
-        r_it=a_rec.reads.begin();
-        r_it!=a_rec.reads.end();
-        r_it++)
+    for(const auto &read_event : address.second.reads)
     {
-      const event_it r=*r_it;
-
-      exprt::operandst rf_some_operands;
-      rf_some_operands.reserve(a_rec.writes.size());
+      exprt::operandst rf_choice_symbols;
+      rf_choice_symbols.reserve(address.second.writes.size());
 
       // this is quadratic in #events per address
-      for(event_listt::const_iterator
-          w_it=a_rec.writes.begin();
-          w_it!=a_rec.writes.end();
-          ++w_it)
+      for(const auto &write_event : address.second.writes)
       {
-        const event_it w=*w_it;
-
         // rf cannot contradict program order
-        if(po(r, w))
-          continue; // contradicts po
-
-        bool is_rfi=
-          w->source.thread_nr==r->source.thread_nr;
-
-        symbol_exprt s=nondet_bool_symbol("rf");
-
-        // record the symbol
-        choice_symbols.emplace(std::make_pair(r, w), s);
-
-        // We rely on the fact that there is at least
-        // one write event that has guard 'true'.
-        implies_exprt read_from(s,
-            and_exprt(w->guard,
-              equal_exprt(r->ssa_lhs, w->ssa_lhs)));
-
-        // Uses only the write's guard as precondition, read's guard
-        // follows from rf_some
-        add_constraint(equation,
-          read_from, is_rfi?"rfi":"rf", r->source);
-
-        if(!is_rfi)
+        if(!po(read_event, write_event))
         {
-          // if r reads from w, then w must have happened before r
-          const implies_exprt cond(s, before(w, r));
-          add_constraint(equation,
-            cond, "rf-order", r->source);
+          rf_choice_symbols.push_back(register_read_from_choice_symbol(
+            read_event, write_event, equation));
         }
-
-        rf_some_operands.push_back(s);
       }
 
-      // value equals the one of some write
-      exprt rf_some;
-
       // uninitialised global symbol like symex_dynamic::dynamic_object*
       // or *$object
-      if(rf_some_operands.empty())
-        continue;
-      else if(rf_some_operands.size()==1)
-        rf_some=rf_some_operands.front();
-      else
+      if(!rf_choice_symbols.empty())
       {
-        rf_some = or_exprt(std::move(rf_some_operands));
+        // Add the read's guard, each of the writes' guards is implied
+        // by each entry in rf_some
+        add_constraint(
+          equation,
+          implies_exprt{read_event->guard, disjunction(rf_choice_symbols)},
+          "rf-some",
+          read_event->source);
       }
-
-      // Add the read's guard, each of the writes' guards is implied
-      // by each entry in rf_some
-      add_constraint(equation,
-        implies_exprt(r->guard, rf_some), "rf-some", r->source);
     }
   }
 }
+
+symbol_exprt memory_model_baset::register_read_from_choice_symbol(
+  const event_it &r,
+  const event_it &w,
+  symex_target_equationt &equation)
+{
+  symbol_exprt s = nondet_bool_symbol("rf");
+
+  // record the symbol
+  choice_symbols.emplace(std::make_pair(r, w), s);
+
+  bool is_rfi = w->source.thread_nr == r->source.thread_nr;
+  // Uses only the write's guard as precondition, read's guard
+  // follows from rf_some
+  add_constraint(
+    equation,
+    // We rely on the fact that there is at least
+    // one write event that has guard 'true'.
+    implies_exprt{s, and_exprt{w->guard, equal_exprt{r->ssa_lhs, w->ssa_lhs}}},
+    is_rfi ? "rfi" : "rf",
+    r->source);
+
+  if(!is_rfi)
+  {
+    // if r reads from w, then w must have happened before r
+    add_constraint(
+      equation, implies_exprt{s, before(w, r)}, "rf-order", r->source);
+  }
+
+  return s;
+}

src/goto-symex/memory_model.h

@@ -14,16 +14,19 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
 
 #include "partial_order_concurrency.h"
 
-class memory_model_baset:public partial_order_concurrencyt
+class memory_model_baset : public partial_order_concurrencyt
 {
 public:
   explicit memory_model_baset(const namespacet &_ns);
   virtual ~memory_model_baset();
 
-  virtual void operator()(symex_target_equationt &)=0;
+  virtual void operator()(symex_target_equationt &) = 0;
 
 protected:
-  // program order
+  /// In-thread program order
+  /// \param e1: preceding event
+  /// \param e2: following event
+  /// \return true if e1 precedes e2 in program order
   bool po(event_it e1, event_it e2);
 
   // produce fresh symbols
@@ -32,12 +35,27 @@ class memory_model_baset:public partial_order_concurrencyt
 
   // This gives us the choice symbol for an R-W pair;
   // built by the method below.
-  typedef std::map<
-    std::pair<event_it, event_it>, symbol_exprt> choice_symbolst;
+  typedef std::map<std::pair<event_it, event_it>, symbol_exprt> choice_symbolst;
   choice_symbolst choice_symbols;
 
+  /// For each read `r` from every address we collect the choice symbols `S`
+  ///   via \ref register_read_from_choice_symbol (for potential read-write
+  ///   pairs) and add a constraint r.guard => \/S.
+  /// \param equation: symex equation where the new constraint should be added
   void read_from(symex_target_equationt &equation);
 
+  /// Introduce a new choice symbol `s` for the pair (\p r, \p w)
+  /// add constraint s => (w.guard /\ r.lhs=w.lhs)
+  /// add constraint s => before(w,r) [if \p w is from another thread]
+  /// \param r: read event
+  /// \param w: write event
+  /// \param equation: symex equation where the new constraints should be added
+  /// \return the new choice symbol
+  symbol_exprt register_read_from_choice_symbol(
+    const event_it &r,
+    const event_it &w,
+    symex_target_equationt &equation);
+
   // maps thread numbers to an event list
   typedef std::map<unsigned, event_listt> per_thread_mapt;
 };