Skip to content

Commit 7a7880a

Browse files
caballacaballa
committed
fix: lowering of unsigned comparisons
Added more comments and tests
1 parent 75b5fb9 commit 7a7880a

File tree

12 files changed

+472
-229
lines changed

12 files changed

+472
-229
lines changed

‎lib/Clam/CfgBuilder.cc‎

Lines changed: 89 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -175,23 +175,21 @@ static void havoc(var_t v, std::string comment, basic_block_t &bb,
175175
}
176176
}
177177

178+
/**
179+
* Translating unsigned comparisons by using select operators
180+
* PRECONDITION: x cmp y, where cmp will be either <= or <
181+
*
182+
* For instance, x u< y will be translated into:
183+
*
184+
* select(x s>= 0, select(y s>= 0, x u< y, true), select(y s>= 0, false, x u< y)
185+
*
186+
* if isNegated is true then we logically negate cmp, true and false
187+
**/
178188
static void unsignedCmpIntoSignOnes(var_t &res, lin_exp_t &op0, lin_exp_t &op1,
179189
crabLitFactory &lfac, basic_block_t &bb,
180-
const bool isNegated, const bool isCmpULE) {
181-
// translating unsigned comparisons by using select operators
182-
// x cmp y, where cmp will be either <= or <
183-
// will be translated into:
184-
// if x >= 0
185-
// if y >= 0 then x cmp y
186-
// else // x >= 0 y < 0
187-
// false
188-
// else
189-
// if y >= 0 then // x < 0 y >= 0
190-
// true
191-
// else x cmp y
192-
// reverse cmp, true and false if isNegated is set
190+
const bool isNegated, const bool isNonStrict) {
193191
lin_cst_t cmp;
194-
if (isCmpULE) {
192+
if (isNonStrict) {
195193
if (!isNegated)
196194
cmp = lin_cst_t(op0 <= op1);
197195
else
@@ -202,70 +200,100 @@ static void unsignedCmpIntoSignOnes(var_t &res, lin_exp_t &op0, lin_exp_t &op1,
202200
else
203201
cmp = lin_cst_t(op0 >= op1);
204202
}
203+
lin_cst_t trueC = !isNegated ? lin_cst_t::get_true() : lin_cst_t::get_false();
204+
lin_cst_t falseC = !isNegated ? lin_cst_t::get_false() : lin_cst_t::get_true();
205205
lin_cst_t cst_op0 = lin_cst_t(op0 >= 0);
206206
lin_cst_t cst_op1 = lin_cst_t(op1 >= 0);
207+
207208
if (cst_op0.is_tautology()) { // if the first operand is >= 0
208209
if (cst_op1.is_tautology()) { // if the second operand is >= 0
210+
/**
211+
* x u< y
212+
**/
209213
bb.bool_assign(res, cmp);
210214
} else if (cst_op1.is_contradiction()) { // if the second operand is < 0
211-
bb.bool_assign(res, !isNegated ? lin_cst_t::get_false()
212-
: lin_cst_t::get_true());
215+
/**
216+
* true
217+
**/
218+
bb.bool_assign(res, trueC);
213219
} else { // don't know the value of the second operand
214-
var_t select_cond_1 = lfac.mkBoolVar();
215-
bb.bool_assign(select_cond_1, cst_op1);
216-
var_t cmp_var = lfac.mkBoolVar();
217-
bb.bool_assign(cmp_var, cmp);
218-
var_t v_false = lfac.mkBoolVar();
219-
bb.bool_assign(v_false, !isNegated ? lin_cst_t::get_false()
220-
: lin_cst_t::get_true());
221-
bb.bool_select(res, select_cond_1, cmp_var, v_false);
220+
/**
221+
* select(y s>= 0, x u< y, true)
222+
**/
223+
var_t condB = lfac.mkBoolVar();
224+
bb.bool_assign(condB, cst_op1);
225+
var_t thenB = lfac.mkBoolVar();
226+
bb.bool_assign(thenB, cmp);
227+
var_t elseB = lfac.mkBoolVar();
228+
bb.bool_assign(elseB, trueC);
229+
bb.bool_select(res, condB, thenB, elseB);
222230
}
223231
} else if (cst_op0.is_contradiction()) { // if the first operand is < 0
224232
if (cst_op1.is_tautology()) { // if the second operand is >= 0
225-
bb.bool_assign(res, !isNegated ? lin_cst_t::get_true()
226-
: lin_cst_t::get_false());
233+
/**
234+
* false
235+
**/
236+
bb.bool_assign(res, falseC);
227237
} else if (cst_op1.is_contradiction()) { // if the second operand is < 0
238+
/**
239+
* x u< y
240+
**/
228241
bb.bool_assign(res, cmp);
229242
} else { // don't know the value of the second operand
230-
var_t select_cond_1 = lfac.mkBoolVar();
231-
bb.bool_assign(select_cond_1, cst_op1);
232-
var_t v_true = lfac.mkBoolVar();
233-
bb.bool_assign(v_true, !isNegated ? lin_cst_t::get_true()
234-
: lin_cst_t::get_false());
235-
var_t cmp_var = lfac.mkBoolVar();
236-
bb.bool_assign(cmp_var, cmp);
237-
bb.bool_select(res, select_cond_1, v_true, cmp_var);
243+
/**
244+
* select(y s>= 0, false, x u< y)
245+
**/
246+
var_t condB = lfac.mkBoolVar();
247+
bb.bool_assign(condB, cst_op1);
248+
var_t thenB = lfac.mkBoolVar();
249+
bb.bool_assign(thenB, falseC);
250+
var_t elseB = lfac.mkBoolVar();
251+
bb.bool_assign(elseB, cmp);
252+
bb.bool_select(res, condB, thenB, elseB);
238253
}
239254
} else { // don't know the value of the first operand
240-
var_t select_cond_2 = lfac.mkBoolVar();
241-
var_t op0_ge_0 = lfac.mkBoolVar();
242-
var_t op0_lt_0 = lfac.mkBoolVar();
243-
bb.bool_assign(select_cond_2, cst_op0);
244255
if (cst_op1.is_tautology()) { // if the second operand is >= 0
245-
bb.bool_assign(op0_ge_0, cmp);
246-
bb.bool_assign(op0_lt_0, !isNegated ? lin_cst_t::get_true()
247-
: lin_cst_t::get_false());
256+
/**
257+
* select(x s>= 0, x u< y, false)
258+
**/
259+
var_t condB = lfac.mkBoolVar();
260+
bb.bool_assign(condB, cst_op0);
261+
var_t thenB = lfac.mkBoolVar();
262+
bb.bool_assign(thenB, cmp);
263+
var_t elseB = lfac.mkBoolVar();
264+
bb.bool_assign(elseB, falseC);
265+
bb.bool_select(res, condB, thenB, elseB);
248266
} else if (cst_op1.is_contradiction()) { // if the second operand is < 0
249-
bb.bool_assign(op0_ge_0, !isNegated ? lin_cst_t::get_false()
250-
: lin_cst_t::get_true());
251-
bb.bool_assign(op0_lt_0, cmp);
267+
/**
268+
* select(x s>= 0, true, x u< y)
269+
**/
270+
var_t condB = lfac.mkBoolVar();
271+
bb.bool_assign(condB, cst_op0);
272+
var_t thenB = lfac.mkBoolVar();
273+
bb.bool_assign(thenB, trueC);
274+
var_t elseB = lfac.mkBoolVar();
275+
bb.bool_assign(elseB, cmp);
276+
bb.bool_select(res, condB, thenB, elseB);
252277
} else { // don't know the value of those operands, general cases
253-
var_t select_cond_1 = lfac.mkBoolVar();
254-
bb.bool_assign(select_cond_1, cst_op1);
255-
var_t cmp_var_true = lfac.mkBoolVar();
256-
bb.bool_assign(cmp_var_true, cmp);
257-
var_t v_false = lfac.mkBoolVar();
258-
bb.bool_assign(v_false, !isNegated ? lin_cst_t::get_false()
259-
: lin_cst_t::get_true());
260-
bb.bool_select(op0_ge_0, select_cond_1, cmp_var_true, v_false);
261-
var_t cmp_var_false = lfac.mkBoolVar();
262-
bb.bool_assign(cmp_var_false, cmp);
263-
var_t v_true = lfac.mkBoolVar();
264-
bb.bool_assign(v_true, !isNegated ? lin_cst_t::get_true()
265-
: lin_cst_t::get_false());
266-
bb.bool_select(op0_lt_0, select_cond_1, v_true, cmp_var_false);
278+
/**
279+
* select(x s>= 0, select(y s>= 0, x u< y, true), select(y s>= 0, false, x u< y)
280+
**/
281+
var_t condB1 = lfac.mkBoolVar();
282+
bb.bool_assign(condB1, cst_op0);
283+
var_t condB2 = lfac.mkBoolVar();
284+
bb.bool_assign(condB2, cst_op1);
285+
var_t cmpB = lfac.mkBoolVar();
286+
bb.bool_assign(cmpB, cmp);
287+
var_t elseB2 = lfac.mkBoolVar();
288+
bb.bool_assign(elseB2, trueC);
289+
var_t thenB1 = lfac.mkBoolVar();
290+
bb.bool_select(thenB1, condB2, cmpB, elseB2);
291+
var_t thenB2 = lfac.mkBoolVar();
292+
bb.bool_assign(thenB2, falseC);
293+
var_t elseB1 = lfac.mkBoolVar();
294+
bb.bool_select(elseB1, condB2, thenB2, cmpB);
295+
bb.bool_select(res, condB1, thenB1, elseB1);
267296
}
268-
bb.bool_select(res, select_cond_2, op0_ge_0, op0_lt_0);
269297
}
270298
}
271299

@@ -332,7 +360,7 @@ static void cmpInstToCrabBool(CmpInst &I, crabLitFactory &lfac,
332360
case CmpInst::ICMP_ULT: {
333361
if (removeUnsignedCmp) {
334362
unsignedCmpIntoSignOnes(lhs, op0, op1, lfac, bb,
335-
false /*isNegated*/, false /* isCmpULE*/);
363+
false /*isNegated*/, false /* isNonStrict*/);
336364
} else {
337365
CLAM_WARNING("Crab does not support unsigned constraints. Use --crab-lower-unsigned-icmp option");
338366
}
@@ -341,7 +369,7 @@ static void cmpInstToCrabBool(CmpInst &I, crabLitFactory &lfac,
341369
case CmpInst::ICMP_ULE: {
342370
if (removeUnsignedCmp) {
343371
unsignedCmpIntoSignOnes(lhs, op0, op1, lfac, bb,
344-
false /*isNegated*/, true /*isCmpULE*/);
372+
false /*isNegated*/, true /*isNonStrict*/);
345373
} else {
346374
CLAM_WARNING("Crab does not support unsigned constraints. Use --crab-lower-unsigned-icmp option");
347375
}

0 commit comments

Comments
 (0)