cprover
guard.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "guard.h"
13 
14 #include <ostream>
15 
16 #include "std_expr.h"
17 #include "simplify_utils.h"
18 
19 void guardt::guard_expr(exprt &dest) const
20 {
21  if(is_true())
22  {
23  // do nothing
24  }
25  else
26  {
27  if(dest.is_false())
28  {
29  dest=as_expr();
30  dest.make_not();
31  }
32  else
33  {
34  implies_exprt tmp;
35  tmp.op0()=as_expr();
36  tmp.op1().swap(dest);
37  dest.swap(tmp);
38  }
39  }
40 }
41 
42 #if 0
43 exprt guardt::as_expr(guard_listt::const_iterator it) const
44 {
45  if(it==guard_list.end())
46  return true_exprt();
47  else if(it==--guard_list.end())
48  return guard_list.back();
49 
50  exprt dest;
51  dest=exprt(ID_and, typet(ID_bool));
52  dest.reserve_operands(guard_list.size());
53  for(; it!=guard_list.end(); it++)
54  {
55  if(!it->is_boolean())
56  throw "guard is expected to be Boolean";
57  dest.copy_to_operands(*it);
58  }
59 
60  return dest;
61 }
62 #endif
63 
64 void guardt::add(const exprt &expr)
65 {
66  assert(expr.type().id()==ID_bool);
67 
68  if(is_false() || expr.is_true())
69  return;
70  else if(is_true() || expr.is_false())
71  {
72  *this=expr;
73 
74  return;
75  }
76  else if(id()!=ID_and)
77  {
78  and_exprt a;
79  a.copy_to_operands(*this);
80  *this=a;
81  }
82 
83  operandst &op=operands();
84 
85  if(expr.id()==ID_and)
86  op.insert(op.end(),
87  expr.operands().begin(),
88  expr.operands().end());
89  else
90  op.push_back(expr);
91 }
92 
93 guardt &operator -= (guardt &g1, const guardt &g2)
94 {
95  if(g1.id()!=ID_and || g2.id()!=ID_and)
96  return g1;
97 
98  sort_and_join(g1);
99  guardt g2_sorted=g2;
100  sort_and_join(g2_sorted);
101 
102  exprt::operandst &op1=g1.operands();
103  const exprt::operandst &op2=g2_sorted.operands();
104 
105  exprt::operandst::iterator it1=op1.begin();
106  for(exprt::operandst::const_iterator
107  it2=op2.begin();
108  it2!=op2.end();
109  ++it2)
110  {
111  while(it1!=op1.end() && *it1<*it2)
112  ++it1;
113  if(it1!=op1.end() && *it1==*it2)
114  it1=op1.erase(it1);
115  }
116 
117  g1=conjunction(op1);
118 
119  return g1;
120 }
121 
123 {
124  if(g2.is_false() || g1.is_true())
125  return g1;
126  if(g1.is_false() || g2.is_true())
127  {
128  g1=g2;
129  return g1;
130  }
131 
132  if(g1.id()!=ID_and || g2.id()!=ID_and)
133  {
134  exprt tmp(g2);
135  tmp.make_not();
136 
137  if(tmp==g1)
138  g1.make_true();
139  else
140  g1=or_exprt(g1, g2);
141 
142  // TODO: make simplify more capable and apply here
143 
144  return g1;
145  }
146 
147  // find common prefix
148  sort_and_join(g1);
149  guardt g2_sorted=g2;
150  sort_and_join(g2_sorted);
151 
152  exprt::operandst &op1=g1.operands();
153  const exprt::operandst &op2=g2_sorted.operands();
154 
155  exprt::operandst n_op1, n_op2;
156  n_op1.reserve(op1.size());
157  n_op2.reserve(op2.size());
158 
159  exprt::operandst::iterator it1=op1.begin();
160  for(exprt::operandst::const_iterator
161  it2=op2.begin();
162  it2!=op2.end();
163  ++it2)
164  {
165  while(it1!=op1.end() && *it1<*it2)
166  {
167  n_op1.push_back(*it1);
168  it1=op1.erase(it1);
169  }
170  if(it1!=op1.end() && *it1==*it2)
171  ++it1;
172  else
173  n_op2.push_back(*it2);
174  }
175  while(it1!=op1.end())
176  {
177  n_op1.push_back(*it1);
178  it1=op1.erase(it1);
179  }
180 
181  if(n_op2.empty())
182  return g1;
183 
184  // end of common prefix
185  exprt and_expr1=conjunction(n_op1);
186  exprt and_expr2=conjunction(n_op2);
187 
188  g1=conjunction(op1);
189 
190  exprt tmp(and_expr2);
191  tmp.make_not();
192 
193  if(tmp!=and_expr1)
194  {
195  if(and_expr1.is_true() || and_expr2.is_true())
196  {
197  }
198  else
199  // TODO: make simplify more capable and apply here
200  g1.add(or_exprt(and_expr1, and_expr2));
201  }
202 
203  return g1;
204 }
205 
206 #if 0
207 std::ostream &operator << (std::ostream &out, const guardt &g)
208 {
209  forall_expr_list(it, g.guard_list)
210  out << "*** " << it->pretty() << '\n';
211  return out;
212 }
213 
214 #define forall_guard(it, guard_list) \
215  for(guardt::guard_listt::const_iterator it=(guard_list).begin(); \
216  it!=(guard_list).end(); ++it)
217 
218 bool guardt::is_false() const
219 {
220  forall_guard(it, guard_list)
221  if(it->is_false())
222  return true;
223 
224  return false;
225 }
226 
227 void guardt::make_false()
228 {
229  guard_list.clear();
230  guard_list.push_back(exprt());
231  guard_list.back()=false_exprt();
232 }
233 #endif
The type of an expression.
Definition: type.h:20
exprt as_expr() const
Definition: guard.h:43
void guard_expr(exprt &dest) const
Definition: guard.cpp:19
guardt & operator-=(guardt &g1, const guardt &g2)
Definition: guard.cpp:93
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
exprt()
Definition: expr.h:52
bool is_false() const
Definition: expr.cpp:140
guardt & operator|=(guardt &g1, const guardt &g2)
Definition: guard.cpp:122
bool is_true() const
Definition: expr.cpp:133
Definition: guard.h:19
typet & type()
Definition: expr.h:60
boolean implication
Definition: std_expr.h:1926
void make_true()
Definition: expr.cpp:153
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
boolean AND
Definition: std_expr.h:1852
API to expression classes.
exprt & op1()
Definition: expr.h:87
Guard Data Structure.
#define forall_expr_list(it, expr)
Definition: expr.h:36
The boolean constant false.
Definition: std_expr.h:3753
std::vector< exprt > operandst
Definition: expr.h:49
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
void make_false()
Definition: expr.cpp:159
void swap(irept &irep)
Definition: irep.h:231
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
operandst & operands()
Definition: expr.h:70
void add(const exprt &expr)
Definition: guard.cpp:64
void reserve_operands(operandst::size_type n)
Definition: expr.h:108