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 }
invariant_sett::strengthen
void strengthen(const exprt &expr)
Definition: invariant_set.cpp:378
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
invariant_set_domain.h
Value Set.
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
invariant_sett::make_threaded
void make_threaded()
Definition: invariant_set.h:130
exprt
Base class for all expressions.
Definition: expr.h:54
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
invariant_sett::apply_code
void apply_code(const codet &code)
Definition: invariant_set.cpp:1052
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
THROW
@ THROW
Definition: goto_program.h:51
GOTO
@ GOTO
Definition: goto_program.h:35
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
boolean_negate
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
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
OTHER
@ OTHER
Definition: goto_program.h:38
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
simplify_expr.h
RETURN
@ RETURN
Definition: goto_program.h:46
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition: invariant_set_domain.h:32
CATCH
@ CATCH
Definition: goto_program.h:52
DECL
@ DECL
Definition: goto_program.h:48
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
invariant_sett::assignment
void assignment(const exprt &lhs, const exprt &rhs)
Definition: invariant_set.cpp:1035
ASSUME
@ ASSUME
Definition: goto_program.h:36
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
DEAD
@ DEAD
Definition: goto_program.h:49
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
LOCATION
@ LOCATION
Definition: goto_program.h:42
ASSERT
@ ASSERT
Definition: goto_program.h:37
invariant_set_domaint::transform
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...
Definition: invariant_set_domain.cpp:17
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53