cprover
invariant_set_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Invariant Set Domain
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "invariant_set_domain.h"
13 
14 #include <util/expr_util.h>
15 #include <util/simplify_expr.h>
16 
18  const irep_idt &function_from,
19  trace_ptrt trace_from,
20  const irep_idt &function_to,
21  trace_ptrt trace_to,
22  ai_baset &ai,
23  const namespacet &ns)
24 {
25  locationt from_l(trace_from->current_location());
26  locationt to_l(trace_to->current_location());
27 
28  switch(from_l->type)
29  {
30  case GOTO:
31  {
32  // Comparing iterators is safe as the target must be within the same list
33  // of instructions because this is a GOTO.
34  exprt tmp(from_l->get_condition());
35 
36  if(std::next(from_l) == to_l)
37  tmp = boolean_negate(tmp);
38 
39  simplify(tmp, ns);
41  }
42  break;
43 
44  case ASSERT:
45  case ASSUME:
46  {
47  exprt tmp(from_l->get_condition());
48  simplify(tmp, ns);
50  }
51  break;
52 
53  case RETURN:
54  // ignore
55  break;
56 
57  case ASSIGN:
58  {
59  const code_assignt &assignment=to_code_assign(from_l->code);
60  invariant_set.assignment(assignment.lhs(), assignment.rhs());
61  }
62  break;
63 
64  case OTHER:
65  if(from_l->get_other().is_not_nil())
66  invariant_set.apply_code(from_l->code);
67  break;
68 
69  case DECL:
70  invariant_set.apply_code(from_l->code);
71  break;
72 
73  case FUNCTION_CALL:
74  invariant_set.apply_code(from_l->code);
75  break;
76 
77  case START_THREAD:
79  break;
80 
81  case CATCH:
82  case THROW:
83  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
84  break;
85  case DEAD: // No action required
86  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
87  case ATOMIC_END: // Ignoring is a valid over-approximation
88  case END_FUNCTION: // No action required
89  case LOCATION: // No action required
90  case END_THREAD: // Require a concurrent analysis at higher level
91  case SKIP: // No action required
92  break;
93  case INCOMPLETE_GOTO:
95  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
96  break;
97  }
98 }
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::const_targett locationt
Definition: ai_domain.h:77
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void apply_code(const codet &code)
void strengthen(const exprt &expr)
void make_threaded()
void assignment(const exprt &lhs, const exprt &rhs)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
Deprecated expression utility functions.
@ FUNCTION_CALL
Definition: goto_program.h:50
@ ATOMIC_END
Definition: goto_program.h:45
@ DEAD
Definition: goto_program.h:49
@ END_FUNCTION
Definition: goto_program.h:43
@ RETURN
Definition: goto_program.h:46
@ ASSIGN
Definition: goto_program.h:47
@ ASSERT
Definition: goto_program.h:37
@ ATOMIC_BEGIN
Definition: goto_program.h:44
@ CATCH
Definition: goto_program.h:52
@ END_THREAD
Definition: goto_program.h:41
@ SKIP
Definition: goto_program.h:39
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
@ START_THREAD
Definition: goto_program.h:40
@ THROW
Definition: goto_program.h:51
@ DECL
Definition: goto_program.h:48
@ OTHER
Definition: goto_program.h:38
@ GOTO
Definition: goto_program.h:35
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
@ ASSUME
Definition: goto_program.h:36
bool simplify(exprt &expr, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383