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 &,
19  locationt from_l,
20  const irep_idt &,
21  locationt to_l,
22  ai_baset &,
23  const namespacet &ns)
24 {
25  switch(from_l->type)
26  {
27  case GOTO:
28  {
29  // Comparing iterators is safe as the target must be within the same list
30  // of instructions because this is a GOTO.
31  exprt tmp(from_l->get_condition());
32 
33  if(std::next(from_l) == to_l)
34  tmp = boolean_negate(tmp);
35 
36  simplify(tmp, ns);
38  }
39  break;
40 
41  case ASSERT:
42  case ASSUME:
43  {
44  exprt tmp(from_l->get_condition());
45  simplify(tmp, ns);
47  }
48  break;
49 
50  case RETURN:
51  // ignore
52  break;
53 
54  case ASSIGN:
55  {
56  const code_assignt &assignment=to_code_assign(from_l->code);
57  invariant_set.assignment(assignment.lhs(), assignment.rhs());
58  }
59  break;
60 
61  case OTHER:
62  if(from_l->get_other().is_not_nil())
63  invariant_set.apply_code(from_l->code);
64  break;
65 
66  case DECL:
67  invariant_set.apply_code(from_l->code);
68  break;
69 
70  case FUNCTION_CALL:
71  invariant_set.apply_code(from_l->code);
72  break;
73 
74  case START_THREAD:
76  break;
77 
78  case CATCH:
79  case THROW:
80  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
81  break;
82  case DEAD: // No action required
83  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
84  case ATOMIC_END: // Ignoring is a valid over-approximation
85  case END_FUNCTION: // No action required
86  case LOCATION: // No action required
87  case END_THREAD: // Require a concurrent analysis at higher level
88  case SKIP: // No action required
89  break;
90  case INCOMPLETE_GOTO:
92  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
93  break;
94  }
95 }
invariant_sett::strengthen
void strengthen(const exprt &expr)
Definition: invariant_set.cpp:377
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:53
invariant_sett::apply_code
void apply_code(const codet &code)
Definition: invariant_set.cpp:1051
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:50
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
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:127
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
OTHER
@ OTHER
Definition: goto_program.h:37
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
simplify_expr.h
RETURN
@ RETURN
Definition: goto_program.h:45
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition: invariant_set_domain.h:32
CATCH
@ CATCH
Definition: goto_program.h:51
DECL
@ DECL
Definition: goto_program.h:47
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:1034
ASSUME
@ ASSUME
Definition: goto_program.h:35
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
DEAD
@ DEAD
Definition: goto_program.h:48
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
ASSERT
@ ASSERT
Definition: goto_program.h:36
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
invariant_set_domaint::transform
virtual void transform(const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l, ai_baset &ai, const namespacet &ns) final override
Definition: invariant_set_domain.cpp:17