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  trace_ptrt trace_from,
52  const irep_idt &,
53  trace_ptrt,
54  ai_baset &,
55  const namespacet &) override
56  {
57  locationt from{trace_from->current_location()};
58 
60  "Transformers are only applied at reachable locations");
61 
62  if(from->is_start_thread())
63  is_threaded=true;
64  }
65 
66  void make_bottom() final override
67  {
68  reachable=false;
69  is_threaded=false;
70  }
71 
72  void make_top() final override
73  {
74  reachable=true;
75  is_threaded=true;
76  }
77 
78  void make_entry() final override
79  {
80  reachable=true;
81  is_threaded=false;
82  }
83 
84  bool is_bottom() const override final
85  {
87  "A location cannot be threaded if it is not reachable.");
88 
89  return !reachable;
90  }
91 
92  bool is_top() const override final
93  {
94  return reachable && is_threaded;
95  }
96 };
97 
98 void is_threadedt::compute(const goto_functionst &goto_functions)
99 {
100  // the analysis doesn't actually use the namespace, fake one
101  symbol_tablet symbol_table;
102  const namespacet ns(symbol_table);
103 
104  ait<is_threaded_domaint> is_threaded_analysis;
105 
106  is_threaded_analysis(goto_functions, ns);
107 
108  for(const auto &gf_entry : goto_functions.function_map)
109  {
110  forall_goto_program_instructions(i_it, gf_entry.second.body)
111  {
112  auto domain_ptr = is_threaded_analysis.abstract_state_before(i_it);
113  if(static_cast<const is_threaded_domaint &>(*domain_ptr).is_threaded)
114  is_threaded_set.insert(i_it);
115  }
116  }
117 }
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:66
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:72
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:559
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:222
is_threaded_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: is_threaded.cpp:78
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
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:84
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
is_threadedt::compute
void compute(const goto_functionst &goto_functions)
Definition: is_threaded.cpp:98
is_threadedt::is_threaded_set
is_threaded_sett is_threaded_set
Definition: is_threaded.h:48
ai.h
Abstract Interpretation.
is_threaded_domaint::transform
void transform(const irep_idt &, trace_ptrt trace_from, const irep_idt &, trace_ptrt, ai_baset &, const namespacet &) override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Definition: is_threaded.cpp:49
is_threaded_domaint::is_top
bool is_top() const override final
Definition: is_threaded.cpp:92
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:77
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
is_threaded_domaint::merge
bool merge(const is_threaded_domaint &src, locationt, locationt)
Definition: is_threaded.cpp:31
is_threaded_domaint::reachable
bool reachable
Definition: is_threaded.cpp:21
is_threaded_domaint::is_threaded
bool is_threaded
Definition: is_threaded.cpp:22
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1167