cprover
is_threaded.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Over-approximate Concurrency for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: October 2012
8 
9 \*******************************************************************/
10 
13 
14 #include "is_threaded.h"
15 
16 #include "ai.h"
17 
19 {
20 public:
21  bool reachable;
23 
25  reachable(false),
26  is_threaded(false)
27  {
28  // this is bottom
29  }
30 
31  bool merge(
32  const is_threaded_domaint &src,
33  locationt,
34  locationt)
35  {
36  INVARIANT(src.reachable,
37  "Abstract states are only merged at reachable locations");
38 
39  bool old_reachable=reachable;
40  bool old_is_threaded=is_threaded;
41 
42  reachable=true;
44 
45  return old_reachable!=reachable ||
46  old_is_threaded!=is_threaded;
47  }
48 
49  void transform(
50  const irep_idt &,
51  locationt from,
52  const irep_idt &,
53  locationt,
54  ai_baset &,
55  const namespacet &) final override
56  {
58  "Transformers are only applied at reachable locations");
59 
60  if(from->is_start_thread())
61  is_threaded=true;
62  }
63 
64  void make_bottom() final override
65  {
66  reachable=false;
67  is_threaded=false;
68  }
69 
70  void make_top() final override
71  {
72  reachable=true;
73  is_threaded=true;
74  }
75 
76  void make_entry() final override
77  {
78  reachable=true;
79  is_threaded=false;
80  }
81 
82  bool is_bottom() const override final
83  {
85  "A location cannot be threaded if it is not reachable.");
86 
87  return !reachable;
88  }
89 
90  bool is_top() const override final
91  {
92  return reachable && is_threaded;
93  }
94 };
95 
96 void is_threadedt::compute(const goto_functionst &goto_functions)
97 {
98  // the analysis doesn't actually use the namespace, fake one
99  symbol_tablet symbol_table;
100  const namespacet ns(symbol_table);
101 
102  ait<is_threaded_domaint> is_threaded_analysis;
103 
104  is_threaded_analysis(goto_functions, ns);
105 
106  forall_goto_functions(f_it, goto_functions)
107  forall_goto_program_instructions(i_it, f_it->second.body)
108  {
109  auto domain_ptr = is_threaded_analysis.abstract_state_before(i_it);
110  if(static_cast<const is_threaded_domaint &>(*domain_ptr).is_threaded)
111  is_threaded_set.insert(i_it);
112  }
113 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
is_threaded_domaint::make_bottom
void make_bottom() final override
no states
Definition: is_threaded.cpp:64
is_threaded_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: is_threaded.cpp:70
is_threaded_domaint::is_threaded_domaint
is_threaded_domaint()
Definition: is_threaded.cpp:24
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
ai_baset::abstract_state_before
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition: ai.h:221
is_threaded_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: is_threaded.cpp:76
is_threaded_domaint
Definition: is_threaded.cpp:19
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
is_threaded_domaint::is_bottom
bool is_bottom() const override final
Definition: is_threaded.cpp:82
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
is_threadedt::compute
void compute(const goto_functionst &goto_functions)
Definition: is_threaded.cpp:96
is_threaded_domaint::transform
void transform(const irep_idt &, locationt from, const irep_idt &, locationt, ai_baset &, const namespacet &) final override
Definition: is_threaded.cpp:49
is_threadedt::is_threaded_set
is_threaded_sett is_threaded_set
Definition: is_threaded.h:48
ai.h
Abstract Interpretation.
is_threaded_domaint::is_top
bool is_top() const override final
Definition: is_threaded.cpp:90
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
is_threaded_domaint::merge
bool merge(const is_threaded_domaint &src, locationt, locationt)
Definition: is_threaded.cpp:31
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
is_threaded_domaint::reachable
bool reachable
Definition: is_threaded.cpp:21
is_threaded_domaint::is_threaded
bool is_threaded
Definition: is_threaded.cpp:22
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
validation_modet::INVARIANT
@ INVARIANT