cprover
partial_order_concurrencyt Class Referenceabstract

Base class for implementing memory models via additional constraints for SSA equations. More...

#include <partial_order_concurrency.h>

+ Inheritance diagram for partial_order_concurrencyt:
+ Collaboration diagram for partial_order_concurrencyt:

Classes

struct  a_rect
 

Public Types

enum  axiomt { AX_SC_PER_LOCATION =1, AX_NO_THINAIR =2, AX_OBSERVATION =4, AX_PROPAGATION =8 }
 
typedef SSA_stept eventt
 
typedef symex_target_equationt::SSA_stepst eventst
 
typedef eventst::const_iterator event_it
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 partial_order_concurrencyt (const namespacet &_ns)
 
virtual ~partial_order_concurrencyt ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Static Public Member Functions

static irep_idt rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION)
 Build identifier for the read/write clock variable. More...
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 

Protected Types

typedef std::vector< event_itevent_listt
 
typedef std::map< irep_idt, a_rectaddress_mapt
 
typedef std::map< event_it, unsigned > numberingt
 

Protected Member Functions

void build_event_lists (symex_target_equationt &)
 First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (with a list of reads/writes for the address of each event) 2) the numbering map (with per-thread unique number of every event) More...
 
void add_init_writes (symex_target_equationt &)
 For each shared read event and for each shared write event that appears after spawn or has false guard prepend a shared write SSA step with non-deterministic value. More...
 
irep_idt address (event_it event) const
 Produce an address ID for an event. More...
 
symbol_exprt clock (event_it e, axiomt axiom)
 Produce a clock symbol for some event. More...
 
void build_clock_type ()
 Initialize the clock_type so that it can be used to number events. More...
 
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. More...
 
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 constrain with equality between their clocks otherwise constrain with e1 clock being less than e2 clock. More...
 
virtual exprt before (event_it e1, event_it e2)=0
 

Static Protected Member Functions

static irep_idt id (event_it event)
 Produce the symbol ID for an event. More...
 

Protected Attributes

const namespacetns
 
address_mapt address_map
 
numberingt numbering
 
typet clock_type
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Base class for implementing memory models via additional constraints for SSA equations.

Provides methods for encoding ordering of shared read/write events.

Definition at line 22 of file partial_order_concurrency.h.

Member Typedef Documentation

◆ address_mapt

Definition at line 60 of file partial_order_concurrency.h.

◆ event_it

typedef eventst::const_iterator partial_order_concurrencyt::event_it

Definition at line 30 of file partial_order_concurrency.h.

◆ event_listt

typedef std::vector<event_it> partial_order_concurrencyt::event_listt
protected

Definition at line 52 of file partial_order_concurrency.h.

◆ eventst

◆ eventt

◆ numberingt

typedef std::map<event_it, unsigned> partial_order_concurrencyt::numberingt
protected

Definition at line 79 of file partial_order_concurrency.h.

Member Enumeration Documentation

◆ axiomt

Enumerator
AX_SC_PER_LOCATION 
AX_NO_THINAIR 
AX_OBSERVATION 
AX_PROPAGATION 

Definition at line 33 of file partial_order_concurrency.h.

Constructor & Destructor Documentation

◆ partial_order_concurrencyt()

partial_order_concurrencyt::partial_order_concurrencyt ( const namespacet _ns)
explicit

Definition at line 19 of file partial_order_concurrency.cpp.

◆ ~partial_order_concurrencyt()

partial_order_concurrencyt::~partial_order_concurrencyt ( )
virtual

Definition at line 24 of file partial_order_concurrency.cpp.

Member Function Documentation

◆ add_constraint()

void partial_order_concurrencyt::add_constraint ( symex_target_equationt equation,
const exprt cond,
const std::string &  msg,
const symex_targett::sourcet source 
) const
protected

Simplify and add a constraint to equation.

Parameters
equationtarget equation to be constrained with the cond
condcondition expressing the constraint
msgmessage for the constraint
sourcethe location of the constraint

Definition at line 202 of file partial_order_concurrency.cpp.

◆ add_init_writes()

void partial_order_concurrencyt::add_init_writes ( symex_target_equationt equation)
protected

For each shared read event and for each shared write event that appears after spawn or has false guard prepend a shared write SSA step with non-deterministic value.

Parameters
equationthe target equation to be modified

Definition at line 28 of file partial_order_concurrency.cpp.

◆ address()

irep_idt partial_order_concurrencyt::address ( event_it  event) const
inlineprotected

Produce an address ID for an event.

Parameters
eventSSA step for the event
Returns
L1-renamed identifier

Definition at line 93 of file partial_order_concurrency.h.

◆ before() [1/2]

exprt partial_order_concurrencyt::before ( event_it  e1,
event_it  e2,
unsigned  axioms 
)
protected

Build the partial order constraint for two events: if e1 and e2 are in the same atomic section then constrain with equality between their clocks otherwise constrain with e1 clock being less than e2 clock.

Parameters
e1preceding event
e2succeeding event
axiomsclocks to be included in the resulting constraint
Returns
conjunction of constraints (one of each clock)

Definition at line 168 of file partial_order_concurrency.cpp.

◆ before() [2/2]

virtual exprt partial_order_concurrencyt::before ( event_it  e1,
event_it  e2 
)
protectedpure virtual

Implemented in memory_model_sct, and memory_model_tsot.

◆ build_clock_type()

void partial_order_concurrencyt::build_clock_type ( )
protected

Initialize the clock_type so that it can be used to number events.

Definition at line 160 of file partial_order_concurrency.cpp.

◆ build_event_lists()

void partial_order_concurrencyt::build_event_lists ( symex_target_equationt equation)
protected

First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (with a list of reads/writes for the address of each event) 2) the numbering map (with per-thread unique number of every event)

Parameters
equationthe target equation (containing the events to be processed)

Definition at line 75 of file partial_order_concurrency.cpp.

◆ clock()

symbol_exprt partial_order_concurrencyt::clock ( event_it  e,
axiomt  axiom 
)
protected

Produce a clock symbol for some event.

Parameters
eevent is either shared read/write or spawn
axiomclock variable
Returns
symbol of type clock_type with id from rw_clock_id

Definition at line 137 of file partial_order_concurrency.cpp.

◆ id()

static irep_idt partial_order_concurrencyt::id ( event_it  event)
inlinestaticprotected

Produce the symbol ID for an event.

Parameters
eventSSA step for the event
Returns
identifier

Definition at line 85 of file partial_order_concurrency.h.

◆ rw_clock_id()

irep_idt partial_order_concurrencyt::rw_clock_id ( event_it  e,
axiomt  axiom = AX_PROPAGATION 
)
static

Build identifier for the read/write clock variable.

Parameters
eeither shared read or shared write event
axiomthe clock variable to be used (as part of the identifier)
Returns
identifier representing the clock variable of the event

Definition at line 125 of file partial_order_concurrency.cpp.

Member Data Documentation

◆ address_map

address_mapt partial_order_concurrencyt::address_map
protected

Definition at line 61 of file partial_order_concurrency.h.

◆ clock_type

typet partial_order_concurrencyt::clock_type
protected

Definition at line 98 of file partial_order_concurrency.h.

◆ ns

const namespacet& partial_order_concurrencyt::ns
protected

Definition at line 50 of file partial_order_concurrency.h.

◆ numbering

numberingt partial_order_concurrencyt::numbering
protected

Definition at line 80 of file partial_order_concurrency.h.


The documentation for this class was generated from the following files: