Skip to content

Commit 939f2a2

Browse files
klaaszhixing-xu
klaas
authored and
zhixing-xu
committed
Apply patch from diffblue#2646 
1 parent fae6a48 commit 939f2a2

18 files changed

+133
-49
lines changed

‎regression/goto-instrument/slice19/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--full-slice
44
^EXIT=0$

‎regression/goto-instrument/slice24/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
static void f(int *x) { *x = 5; }
5+
static void g(int *x) { assert(*x == 5); }
6+
7+
int main(int argc, char **argv)
8+
{
9+
int *x = (int*)malloc(sizeof(int));
10+
f(x);
11+
g(x);
12+
13+
return 0;
14+
}

‎regression/goto-instrument/slice24/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.c
3+
--full-slice --add-library
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
Data dependencies across function calls are still not working correctly.

‎src/analyses/dependence_graph.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies(
175175
{
176176
bool found=false;
177177
for(const auto &wr : w_range.second)
178+
{
178179
for(const auto &r_range : r_ranges)
180+
{
179181
if(!found &&
180182
may_be_def_use_pair(wr.first, wr.second,
181183
r_range.first, r_range.second))
@@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies(
184186
data_deps.insert(w_range.first);
185187
found=true;
186188
}
189+
}
190+
}
187191
}
188192

189193
dep_graph.reaching_definitions()[to].clear_cache(it->first);

‎src/analyses/goto_rw.cpp

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -128,8 +128,6 @@ void rw_range_sett::get_objects_dereference(
128128
{
129129
const exprt &pointer=deref.pointer();
130130
get_objects_rec(get_modet::READ, pointer);
131-
if(mode!=get_modet::READ)
132-
get_objects_rec(mode, pointer);
133131
}
134132

135133
void rw_range_sett::get_objects_byte_extract(
@@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast(
414412

415413
void rw_range_sett::get_objects_address_of(const exprt &object)
416414
{
417-
if(object.id() == ID_string_constant ||
415+
if(object.id() == ID_symbol ||
416+
object.id() == ID_string_constant ||
418417
object.id() == ID_label ||
419418
object.id() == ID_array ||
420419
object.id() == ID_null_object)
421420
// constant, nothing to do
421+
{
422422
return;
423-
else if(object.id()==ID_symbol)
424-
get_objects_rec(get_modet::READ, object);
423+
}
425424
else if(object.id()==ID_dereference)
425+
{
426426
get_objects_rec(get_modet::READ, object);
427+
}
427428
else if(object.id()==ID_index)
428429
{
429430
const index_exprt &index=to_index_expr(object);
@@ -524,6 +525,11 @@ void rw_range_sett::get_objects_rec(
524525
get_objects_array(mode, to_array_expr(expr), range_start, size);
525526
else if(expr.id()==ID_struct)
526527
get_objects_struct(mode, to_struct_expr(expr), range_start, size);
528+
else if(expr.id()==ID_dynamic_object)
529+
{
530+
const auto obj_instance = to_dynamic_object_expr(expr).get_instance();
531+
add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1);
532+
}
527533
else if(expr.id()==ID_symbol)
528534
{
529535
const symbol_exprt &symbol=to_symbol_expr(expr);
@@ -564,11 +570,6 @@ void rw_range_sett::get_objects_rec(
564570
{
565571
// dereferencing may yield some weird ones, ignore these
566572
}
567-
else if(mode==get_modet::LHS_W)
568-
{
569-
forall_operands(it, expr)
570-
get_objects_rec(mode, *it);
571-
}
572573
else
573574
throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
574575
}
@@ -605,6 +606,8 @@ void rw_range_set_value_sett::get_objects_dereference(
605606
exprt object=deref;
606607
dereference(target, object, ns, value_sets);
607608

609+
PRECONDITION(object.is_not_nil());
610+
608611
range_spect new_size=
609612
to_range_spect(pointer_offset_bits(object.type(), ns));
610613

‎src/analyses/reaching_definitions.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -307,19 +307,19 @@ void rd_range_domaint::transform_assign(
307307
{
308308
const irep_idt &identifier=it->first;
309309
// ignore symex::invalid_object
310-
const symbolt *symbol_ptr;
311-
if(ns.lookup(identifier, symbol_ptr))
310+
const symbolt *symbol_ptr = nullptr;
311+
bool not_found = ns.lookup(identifier, symbol_ptr);
312+
if(not_found && has_prefix(id2string(identifier), "symex::invalid_object"))
313+
{
312314
continue;
313-
INVARIANT_STRUCTURED(
314-
symbol_ptr!=nullptr,
315-
nullptr_exceptiont,
316-
"Symbol is in symbol table");
315+
}
317316

318317
const range_domaint &ranges=rw_set.get_ranges(it);
319318

320319
if(is_must_alias &&
321320
(!rd.get_is_threaded()(from) ||
322-
(!symbol_ptr->is_shared() &&
321+
(symbol_ptr != nullptr &&
322+
symbol_ptr->is_shared() &&
323323
!rd.get_is_dirty()(identifier))))
324324
for(const auto &range : ranges)
325325
kill(identifier, range.first, range.second);

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2141,7 +2141,7 @@ exprt c_typecheck_baset::do_special_functions(
21412141
throw 0;
21422142
}
21432143

2144-
exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
2144+
exprt dynamic_object_expr=exprt(ID_is_dynamic_object, expr.type());
21452145
dynamic_object_expr.operands()=expr.arguments();
21462146
dynamic_object_expr.add_source_location()=source_location;
21472147

‎src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3580,8 +3580,8 @@ std::string expr2ct::convert_with_precedence(
35803580
else if(src.id()==ID_invalid_pointer)
35813581
return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
35823582

3583-
else if(src.id()==ID_dynamic_object)
3584-
return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
3583+
else if(src.id()==ID_is_dynamic_object)
3584+
return convert_function(src, "IS_DYNAMIC_OBJECT", precedence=16);
35853585

35863586
else if(src.id()=="is_zero_string")
35873587
return convert_function(src, "IS_ZERO_STRING", precedence=16);

‎src/pointer-analysis/value_set_dereference.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -358,8 +358,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
358358
// this is also our guard
359359
result.pointer_guard = dynamic_object(pointer_expr);
360360

361-
// can't remove here, turn into *p
362-
result.value=dereference_exprt(pointer_expr, dereference_type);
361+
// TODO should this be object or root_object?
362+
// TODO It's unclear whether this is a good approach to take --- it
363+
// successfully ensures that every (non-null) dereference points to
364+
// something, making the write set computation work correctly, but dynamic
365+
// objects do not seem to be intended to be used in this way.
366+
result.value = object;
363367

364368
if(options.get_bool_option("pointer-check"))
365369
{

‎src/solvers/flattening/bv_pointers.cpp

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -45,21 +45,21 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
4545
}
4646
}
4747
}
48-
else if(expr.id()==ID_dynamic_object)
48+
else if(expr.id()==ID_is_dynamic_object)
4949
{
50-
if(operands.size()==1 &&
51-
operands[0].type().id()==ID_pointer)
52-
{
53-
// we postpone
54-
literalt l=prop.new_variable();
50+
DATA_INVARIANT(operands.size() == 1 &&
51+
operands[0].type().id() == ID_pointer,
52+
std::string("is_dynamic_object_exprt should have one") +
53+
"operand, which should have pointer type.");
54+
// we postpone
55+
literalt l=prop.new_variable();
5556

56-
postponed_list.push_back(postponedt());
57-
postponed_list.back().op=convert_bv(operands[0]);
58-
postponed_list.back().bv.push_back(l);
59-
postponed_list.back().expr=expr;
57+
postponed_list.push_back(postponedt());
58+
postponed_list.back().op=convert_bv(operands[0]);
59+
postponed_list.back().bv.push_back(l);
60+
postponed_list.back().expr=expr;
6061

61-
return l;
62-
}
62+
return l;
6363
}
6464
else if(expr.id()==ID_lt || expr.id()==ID_le ||
6565
expr.id()==ID_gt || expr.id()==ID_ge)
@@ -735,7 +735,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
735735
void bv_pointerst::do_postponed(
736736
const postponedt &postponed)
737737
{
738-
if(postponed.expr.id()==ID_dynamic_object)
738+
if(postponed.expr.id()==ID_is_dynamic_object)
739739
{
740740
const pointer_logict::objectst &objects=
741741
pointer_logic.objects;

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1367,7 +1367,7 @@ void smt2_convt::convert_expr(const exprt &expr)
13671367
if(ext>0)
13681368
out << ")"; // zero_extend
13691369
}
1370-
else if(expr.id()==ID_dynamic_object)
1370+
else if(expr.id()==ID_is_dynamic_object)
13711371
{
13721372
convert_is_dynamic_object(expr);
13731373
}

‎src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -448,6 +448,7 @@ IREP_ID_TWO(overflow_minus, overflow--)
448448
IREP_ID_TWO(overflow_mult, overflow-*)
449449
IREP_ID_TWO(overflow_unary_minus, overflow-unary-)
450450
IREP_ID_ONE(object_descriptor)
451+
IREP_ID_ONE(is_dynamic_object)
451452
IREP_ID_ONE(dynamic_object)
452453
IREP_ID_TWO(C_dynamic, #dynamic)
453454
IREP_ID_ONE(object_size)

‎src/util/pointer_predicates.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns)
7070

7171
exprt dynamic_object(const exprt &pointer)
7272
{
73-
exprt dynamic_expr(ID_dynamic_object, bool_typet());
73+
exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
7474
dynamic_expr.copy_to_operands(pointer);
7575
return dynamic_expr;
7676
}

‎src/util/simplify_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2266,8 +2266,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
22662266
result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
22672267
else if(expr.id()==ID_pointer_object)
22682268
result=simplify_pointer_object(expr) && result;
2269-
else if(expr.id()==ID_dynamic_object)
2270-
result=simplify_dynamic_object(expr) && result;
2269+
else if(expr.id()==ID_is_dynamic_object)
2270+
result=simplify_is_dynamic_object(expr) && result;
22712271
else if(expr.id()==ID_invalid_pointer)
22722272
result=simplify_invalid_pointer(expr) && result;
22732273
else if(expr.id()==ID_object_size)

‎src/util/simplify_expr_class.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ class simplify_exprt
9696
bool simplify_pointer_object(exprt &expr);
9797
bool simplify_object_size(exprt &expr);
9898
bool simplify_dynamic_size(exprt &expr);
99-
bool simplify_dynamic_object(exprt &expr);
99+
bool simplify_is_dynamic_object(exprt &expr);
100100
bool simplify_invalid_pointer(exprt &expr);
101101
bool simplify_same_object(exprt &expr);
102102
bool simplify_good_pointer(exprt &expr);

‎src/util/simplify_expr_int.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1699,7 +1699,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
16991699
expr.op0().operands().size()==1)
17001700
{
17011701
if(expr.op0().op0().id()==ID_symbol ||
1702-
expr.op0().op0().id()==ID_dynamic_object ||
1702+
expr.op0().op0().id()==ID_is_dynamic_object ||
17031703
expr.op0().op0().id()==ID_member ||
17041704
expr.op0().op0().id()==ID_index ||
17051705
expr.op0().op0().id()==ID_string_constant)
@@ -1715,7 +1715,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
17151715
expr.op0().op0().operands().size()==1)
17161716
{
17171717
if(expr.op0().op0().op0().id()==ID_symbol ||
1718-
expr.op0().op0().op0().id()==ID_dynamic_object ||
1718+
expr.op0().op0().op0().id()==ID_is_dynamic_object ||
17191719
expr.op0().op0().op0().id()==ID_member ||
17201720
expr.op0().op0().op0().id()==ID_index ||
17211721
expr.op0().op0().op0().id()==ID_string_constant)

‎src/util/simplify_expr_pointer.cpp

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -464,7 +464,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
464464
{
465465
if(op.operands().size()!=1 ||
466466
(op.op0().id()!=ID_symbol &&
467-
op.op0().id()!=ID_dynamic_object &&
467+
op.op0().id()!=ID_is_dynamic_object &&
468468
op.op0().id()!=ID_string_constant))
469469
return true;
470470
}
@@ -508,18 +508,20 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
508508
return result;
509509
}
510510

511-
bool simplify_exprt::simplify_dynamic_object(exprt &expr)
511+
bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
512512
{
513-
if(expr.operands().size()!=1)
514-
return true;
513+
DATA_INVARIANT(expr.operands().size() == 1 &&
514+
expr.op0().type().id() == ID_pointer,
515+
std::string("is_dynamic_object_exprt should have one") +
516+
"operand, which should have pointer type.");
515517

516518
exprt &op=expr.op0();
517519

518520
if(op.id()==ID_if && op.operands().size()==3)
519521
{
520522
if_exprt if_expr=lift_if(expr, 0);
521-
simplify_dynamic_object(if_expr.true_case());
522-
simplify_dynamic_object(if_expr.false_case());
523+
simplify_is_dynamic_object(if_expr.true_case());
524+
simplify_is_dynamic_object(if_expr.false_case());
523525
simplify_if(if_expr);
524526
expr.swap(if_expr);
525527

‎src/util/std_expr.h

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2106,6 +2106,54 @@ inline void validate_expr(const dynamic_object_exprt &value)
21062106
}
21072107

21082108

2109+
/*! \brief Evaluates to true if the operand is a pointer to a dynamic object.
2110+
*/
2111+
class is_dynamic_object_exprt:public unary_predicate_exprt
2112+
{
2113+
public:
2114+
is_dynamic_object_exprt():unary_predicate_exprt(ID_is_dynamic_object)
2115+
{
2116+
}
2117+
2118+
explicit is_dynamic_object_exprt(const exprt &op):
2119+
unary_predicate_exprt(ID_is_dynamic_object, op)
2120+
{
2121+
}
2122+
};
2123+
2124+
/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt
2125+
*
2126+
* This is an unchecked conversion. \a expr must be known to be \ref
2127+
* is_dynamic_object_exprt.
2128+
*
2129+
* \param expr Source expression
2130+
* \return Object of type \ref is_dynamic_object_exprt
2131+
*
2132+
* \ingroup gr_std_expr
2133+
*/
2134+
inline const is_dynamic_object_exprt &to_is_dynamic_object_expr(
2135+
const exprt &expr)
2136+
{
2137+
PRECONDITION(expr.id()==ID_is_dynamic_object);
2138+
DATA_INVARIANT(
2139+
expr.operands().size()==1,
2140+
"is_dynamic_object must have one operand");
2141+
return static_cast<const is_dynamic_object_exprt &>(expr);
2142+
}
2143+
2144+
/*! \copydoc to_is_dynamic_object_expr(const exprt &)
2145+
* \ingroup gr_std_expr
2146+
*/
2147+
inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr)
2148+
{
2149+
PRECONDITION(expr.id()==ID_is_dynamic_object);
2150+
DATA_INVARIANT(
2151+
expr.operands().size()==1,
2152+
"is_dynamic_object must have one operand");
2153+
return static_cast<is_dynamic_object_exprt &>(expr);
2154+
}
2155+
2156+
21092157
/*! \brief semantic type conversion
21102158
*/
21112159
class typecast_exprt:public unary_exprt

0 commit comments

Comments
 (0)