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
51  final override
52  {
54  "Transformers are only applied at reachable locations");
55 
56  if(from->is_start_thread())
57  is_threaded=true;
58  }
59 
60  void make_bottom() final override
61  {
62  reachable=false;
63  is_threaded=false;
64  }
65 
66  void make_top() final override
67  {
68  reachable=true;
69  is_threaded=true;
70  }
71 
72  void make_entry() final override
73  {
74  reachable=true;
75  is_threaded=false;
76  }
77 
78  bool is_bottom() const override final
79  {
81  "A location cannot be threaded if it is not reachable.");
82 
83  return !reachable;
84  }
85 
86  bool is_top() const override final
87  {
88  return reachable && is_threaded;
89  }
90 };
91 
92 void is_threadedt::compute(const goto_functionst &goto_functions)
93 {
94  // the analysis doesn't actually use the namespace, fake one
95  symbol_tablet symbol_table;
96  const namespacet ns(symbol_table);
97 
98  ait<is_threaded_domaint> is_threaded_analysis;
99 
100  is_threaded_analysis(goto_functions, ns);
101 
102  forall_goto_functions(f_it, goto_functions)
103  forall_goto_program_instructions(i_it, f_it->second.body)
104  if(is_threaded_analysis[i_it].is_threaded)
105  is_threaded_set.insert(i_it);
106 }
Over-approximate Concurrency for Threaded Goto Programs.
void compute(const goto_functionst &goto_functions)
Definition: is_threaded.cpp:92
Definition: ai.h:294
bool merge(const is_threaded_domaint &src, locationt, locationt)
Definition: is_threaded.cpp:31
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
bool is_top() const override final
Definition: is_threaded.cpp:86
void make_entry() final override
a reasonable entry-point state
Definition: is_threaded.cpp:72
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
is_threaded_sett is_threaded_set
Definition: is_threaded.h:48
void transform(locationt from, locationt, ai_baset &, const namespacet &) final 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:50
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_bottom() const override final
Definition: is_threaded.cpp:78
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
void make_bottom() final override
no states
Definition: is_threaded.cpp:60
goto_programt::const_targett locationt
Definition: ai_domain.h:40
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it...
Definition: is_threaded.cpp:66