CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/memory_model.cpp Source File

CBMC
Loading...
Searching...
No Matches
memory_model.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Memory model for partial order concurrency
4
5Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6
7\*******************************************************************/
8
11
12#include "memory_model.h"
13
14#include <util/std_expr.h>
15
20
24
26{
27 return symbol_exprt(
28 "memory_model::choice_" + prefix + std::to_string(var_cnt++), bool_typet());
29}
30
32{
33 // within same thread
34 if(e1->source.thread_nr == e2->source.thread_nr)
35 return numbering[e1] < numbering[e2];
36 else
37 {
38 // in general un-ordered, with exception of thread-spawning
39 return false;
40 }
41}
42
44{
45 // We iterate over all the reads, and
46 // make them match at least one
47 // (internal or external) write.
48
49 for(const auto &address : address_map)
50 {
51 for(const auto &read_event : address.second.reads)
52 {
54 rf_choice_symbols.reserve(address.second.writes.size());
55
56 // this is quadratic in #events per address
57 for(const auto &write_event : address.second.writes)
58 {
59 // rf cannot contradict program order
61 {
63 read_event, write_event, equation));
64 }
65 }
66
67 // uninitialised global symbol like symex_dynamic::dynamic_object*
68 // or *$object
69 if(!rf_choice_symbols.empty())
70 {
71 // Add the read's guard, each of the writes' guards is implied
72 // by each entry in rf_some
74 equation,
76 "rf-some",
77 read_event->source);
78 }
79 }
80 }
81}
82
84 const event_it &r,
85 const event_it &w,
86 symex_target_equationt &equation)
87{
89
90 // record the symbol
91 choice_symbols.emplace(std::make_pair(r, w), s);
92
93 bool is_rfi = w->source.thread_nr == r->source.thread_nr;
94 // Uses only the write's guard as precondition, read's guard
95 // follows from rf_some
97 equation,
98 // We rely on the fact that there is at least
99 // one write event that has guard 'true'.
100 implies_exprt{s, and_exprt{w->guard, equal_exprt{r->ssa_lhs, w->ssa_lhs}}},
101 is_rfi ? "rfi" : "rf",
102 r->source);
103
104 if(!is_rfi)
105 {
106 // if r reads from w, then w must have happened before r
108 equation, implies_exprt{s, before(w, r)}, "rf-order", r->source);
109 }
110
111 return s;
112}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
The Boolean type.
Definition std_types.h:35
size_t size() const
Definition dstring.h:133
Equality.
Definition std_expr.h:1339
std::vector< exprt > operandst
Definition expr.h:59
Boolean implication.
Definition std_expr.h:2154
virtual ~memory_model_baset()
symbol_exprt nondet_bool_symbol(const std::string &prefix)
bool po(event_it e1, event_it e2)
In-thread program order.
symbol_exprt register_read_from_choice_symbol(const event_it &r, const event_it &w, symex_target_equationt &equation)
Introduce a new choice symbol s for the pair (r, w) add constraint s => (w.guard /\ r....
unsigned var_cnt
Definition memory_model.h:33
memory_model_baset(const namespacet &_ns)
void read_from(symex_target_equationt &equation)
For each read r from every address we collect the choice symbols S via register_read_from_choice_symb...
choice_symbolst choice_symbols
Definition memory_model.h:39
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Base class for implementing memory models via additional constraints for SSA equations.
address_mapt address_map
numberingt numbering
exprt before(event_it e1, event_it e2, unsigned axioms)
Build the partial order constraint for two events: if e1 and e2 are in the same atomic section then c...
irep_idt address(event_it event) const
Produce an address ID for an event.
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Simplify and add a constraint to equation.
eventst::const_iterator event_it
Expression to hold a symbol (variable)
Definition std_expr.h:132
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
r
static int8_t r
Definition irep_hash.h:60
Memory models for partial order concurrency.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:240
API to expression classes.

AltStyle によって変換されたページ (->オリジナル) /