From 9740142bed5a089fac0c1da14cb89dddfe72db2d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Jun 2016 12:55:43 +0100 Subject: [PATCH 01/33] Handle array initialization with a non-array gracefully clang -Wall says: Struct_Initialization1/main.c:16:38: warning: suggest braces around initialization of subobject [-Wmissing-braces] struct _classinfo nullclass1 = { 42, 1, 2, 3, 4 }; ^~~~ { } and then constructs a suitable object. Our implementation now attempts to build an initializer list if a variable-length array is encountered; if this succeeds, the same suitable object is constructed. Variable-length arrays in the middle of a struct are not permitted (neither by GCC nor Clang or our C front-end). --- .../ansi-c/Struct_Initialization1/main.c | 10 ++- .../ansi-c/Struct_Initialization1/test.desc | 2 +- .../ansi-c/Struct_Initialization2/main.c | 24 ++++++ .../ansi-c/Struct_Initialization2/test.desc | 10 +++ src/ansi-c/c_typecheck_base.h | 5 +- src/ansi-c/c_typecheck_initializer.cpp | 77 ++++++++++++++----- src/ansi-c/designator.h | 4 +- 7 files changed, 105 insertions(+), 27 deletions(-) create mode 100644 regression/ansi-c/Struct_Initialization2/main.c create mode 100644 regression/ansi-c/Struct_Initialization2/test.desc diff --git a/regression/ansi-c/Struct_Initialization1/main.c b/regression/ansi-c/Struct_Initialization1/main.c index b497a0b60dd..f2e75463d6c 100644 --- a/regression/ansi-c/Struct_Initialization1/main.c +++ b/regression/ansi-c/Struct_Initialization1/main.c @@ -1,13 +1,19 @@ #define STATIC_ASSERT(condition) \ int some_array##__LINE__[(condition) ? 1 : -1] +struct A { + int x; + int y; +}; + struct _classinfo { char a; + struct A s; int *interfaces[]; }; -struct _classinfo nullclass1 = { 42, 0, 0 }; -struct _classinfo nullclass2 = { 42, { 0, 0 } }; +struct _classinfo nullclass1 = { 42, 1, 2, 3, 4 }; +struct _classinfo nullclass2 = { 42, { 1, 2 }, { 3, 4 } }; STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo)); STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo)); diff --git a/regression/ansi-c/Struct_Initialization1/test.desc b/regression/ansi-c/Struct_Initialization1/test.desc index fc2b1874059..466da18b2b5 100644 --- a/regression/ansi-c/Struct_Initialization1/test.desc +++ b/regression/ansi-c/Struct_Initialization1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=0$ diff --git a/regression/ansi-c/Struct_Initialization2/main.c b/regression/ansi-c/Struct_Initialization2/main.c new file mode 100644 index 00000000000..98cce21ebc8 --- /dev/null +++ b/regression/ansi-c/Struct_Initialization2/main.c @@ -0,0 +1,24 @@ +#define STATIC_ASSERT(condition) \ + int some_array##__LINE__[(condition) ? 1 : -1] + +struct A { + int x; + int y; + int arr[]; +}; + +struct _classinfo { + char a; + struct A s; + int *interfaces[]; +}; + +struct _classinfo nullclass1 = { 42, 1, 2, 0, 3, 4 }; +struct _classinfo nullclass2 = { 42, { 1, 2, 0 }, { 3, 4 } }; + +STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo)); +STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo)); + +int main() +{ +} diff --git a/regression/ansi-c/Struct_Initialization2/test.desc b/regression/ansi-c/Struct_Initialization2/test.desc new file mode 100644 index 00000000000..73c2caa52cd --- /dev/null +++ b/regression/ansi-c/Struct_Initialization2/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +^EXIT=(64|1)$ +^SIGNAL=0$ +^CONVERSION ERROR$ +-- +^warning: ignoring +-- +variable-length arrays in the middle of a struct are not permitted diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 521ae29aa4a..eec934736d5 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -89,10 +89,11 @@ class c_typecheck_baset: const typet &type, bool force_constant); - virtual void do_designated_initializer( + virtual exprt::operandst::const_iterator do_designated_initializer( exprt &result, designatort &designator, - const exprt &value, + const exprt &initializer_list, + exprt::operandst::const_iterator init_it, bool force_constant); designatort make_designator(const typet &type, const exprt &src); diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index fd098259796..1bc494c8d4a 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -256,9 +256,7 @@ void c_typecheck_baset::designator_enter( const typet &type, designatort &designator) { - designatort::entryt entry; - entry.type=type; - entry.index=0; + designatort::entryt entry(type); const typet &full_type=follow(type); @@ -268,6 +266,8 @@ void c_typecheck_baset::designator_enter( entry.size=struct_type.components().size(); entry.subtype.make_nil(); + // only a top-level struct may end with a variable-length array + entry.vla_permitted=designator.empty(); for(struct_typet::componentst::const_iterator it=struct_type.components().begin(); @@ -351,12 +351,16 @@ void c_typecheck_baset::designator_enter( /// \param pre:initialized result, designator /// \return sets result -void c_typecheck_baset::do_designated_initializer( +exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( exprt &result, designatort &designator, - const exprt &value, + const exprt &initializer_list, + exprt::operandst::const_iterator init_it, bool force_constant) { + // copy the value, we may need to adjust it + exprt value=*init_it; + assert(!designator.empty()); if(value.id()==ID_designated_initializer) @@ -370,8 +374,10 @@ void c_typecheck_baset::do_designated_initializer( assert(!designator.empty()); - return do_designated_initializer( - result, designator, value.op0(), force_constant); + // discard the return value + do_designated_initializer( + result, designator, value, value.operands().begin(), force_constant); + return ++init_it; } exprt *dest=&result; @@ -503,7 +509,7 @@ void c_typecheck_baset::do_designated_initializer( assert(full_type==follow(dest->type())); - return; // done + return ++init_it; // done } // union? The component in the zero initializer might @@ -537,7 +543,7 @@ void c_typecheck_baset::do_designated_initializer( if(value.id()==ID_initializer_list) { *dest=do_initializer_rec(value, type, force_constant); - return; // done + return ++init_it; // done } else if(value.id()==ID_string_constant) { @@ -549,7 +555,7 @@ void c_typecheck_baset::do_designated_initializer( follow(full_type.subtype()).id()==ID_unsignedbv)) { *dest=do_initializer_rec(value, type, force_constant); - return; // done + return ++init_it; // done } } else if(follow(value.type())==full_type) @@ -562,7 +568,7 @@ void c_typecheck_baset::do_designated_initializer( full_type.id()==ID_vector) { *dest=value; - return; // done + return ++init_it; // done } } @@ -574,21 +580,49 @@ void c_typecheck_baset::do_designated_initializer( // we are initializing a compound type, and enter it! // this may change the type, full_type might not be valid any more const typet dest_type=full_type; + const bool vla_permitted=designator.back().vla_permitted; designator_enter(type, designator); + // GCC permits (though issuing a warning with -Wall) composite + // types built from flat initializer lists if(dest->operands().empty()) { - err_location(value); - error() << "cannot initialize type `" - << to_string(dest_type) << "' using value `" - << to_string(value) << "'" << eom; - throw 0; + warning().source_location=value.find_source_location(); + warning() << "initialisation of " << full_type.id() + << " requires initializer list, found " + << value.id() << " instead" << eom; + + // in case of a variable-length array consume all remaining + // initializer elements + if(vla_permitted && + dest_type.id()==ID_array && + (to_array_type(dest_type).size().is_zero() || + to_array_type(dest_type).size().is_nil())) + { + value.id(ID_initializer_list); + value.operands().clear(); + for( ; init_it!=initializer_list.operands().end(); ++init_it) + value.copy_to_operands(*init_it); + *dest=do_initializer_rec(value, dest_type, force_constant); + + return init_it; + } + else + { + err_location(value); + error() << "cannot initialize type `" + << to_string(dest_type) << "' using value `" + << to_string(value) << "'" << eom; + throw 0; + } } dest=&(dest->op0()); // we run into another loop iteration } + + return ++init_it; } void c_typecheck_baset::increment_designator(designatort &designator) @@ -651,8 +685,7 @@ designatort c_typecheck_baset::make_designator( forall_operands(it, src) { const exprt &d_op=*it; - designatort::entryt entry; - entry.type=type; + designatort::entryt entry(type); const typet &full_type=follow(entry.type); if(full_type.id()==ID_array) @@ -856,10 +889,12 @@ exprt c_typecheck_baset::do_initializer_list( designator_enter(type, current_designator); - forall_operands(it, value) + const exprt::operandst &operands=value.operands(); + for(exprt::operandst::const_iterator it=operands.begin(); + it!=operands.end(); ) // no ++it { - do_designated_initializer( - result, current_designator, *it, force_constant); + it=do_designated_initializer( + result, current_designator, value, it, force_constant); // increase designator -- might go up increment_designator(current_designator); diff --git a/src/ansi-c/designator.h b/src/ansi-c/designator.h index d31d3bb3e66..957bbbb6821 100644 --- a/src/ansi-c/designator.h +++ b/src/ansi-c/designator.h @@ -24,9 +24,11 @@ class designatort { size_t index; size_t size; + bool vla_permitted; typet type, subtype; - entryt():index(0), size(0) + explicit entryt(const typet &type): + index(0), size(0), vla_permitted(false), type(type) { } }; From 564f64c6850aed39c8090f5b3dae865bafb7718d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 15 Jul 2017 15:23:11 +0100 Subject: [PATCH 02/33] added a non-recursive variant of APPLY --- src/solvers/miniBDD/miniBDD.cpp | 120 +++++++++++++++++++++++++++++--- 1 file changed, 111 insertions(+), 9 deletions(-) diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp index d32330a0995..fc47235b076 100644 --- a/src/solvers/miniBDD/miniBDD.cpp +++ b/src/solvers/miniBDD/miniBDD.cpp @@ -194,18 +194,19 @@ class mini_bdd_applyt mini_bddt operator()(const mini_bddt &x, const mini_bddt &y) { - return APP(x, y); + return APP_non_rec(x, y); } protected: bool (*fkt)(bool, bool); - mini_bddt APP(const mini_bddt &x, const mini_bddt &y); + mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y); + mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y); typedef std::map, mini_bddt> Gt; Gt G; }; -mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y) +mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y) { assert(x.is_initialized() && y.is_initialized()); assert(x.node->mgr==y.node->mgr); @@ -224,22 +225,123 @@ mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y) u=mini_bddt(fkt(x.is_true(), y.is_true())?mgr->True():mgr->False()); else if(x.var()==y.var()) u=mgr->mk(x.var(), - APP(x.low(), y.low()), - APP(x.high(), y.high())); + APP_rec(x.low(), y.low()), + APP_rec(x.high(), y.high())); else if(x.var()mk(x.var(), - APP(x.low(), y), - APP(x.high(), y)); + APP_rec(x.low(), y), + APP_rec(x.high(), y)); else /* x.var() > y.var() */ u=mgr->mk(y.var(), - APP(x, y.low()), - APP(x, y.high())); + APP_rec(x, y.low()), + APP_rec(x, y.high())); G[key]=u; return u; } +mini_bddt mini_bdd_applyt::APP_non_rec( + const mini_bddt &_x, + const mini_bddt &_y) +{ + struct stack_elementt + { + stack_elementt( + mini_bddt &_result, + const mini_bddt &_x, + const mini_bddt &_y): + result(_result), x(_x), y(_y), + key(x.node_number(), y.node_number()), + var(0), phase(phaset::INIT) { } + mini_bddt &result, x, y, lr, hr; + std::pair key; + unsigned var; + enum class phaset { INIT, FINISH } phase; + }; + + mini_bddt u; // return value + + std::stack stack; + stack.push(stack_elementt(u, _x, _y)); + + while(!stack.empty()) + { + auto &t=stack.top(); + const mini_bddt &x=t.x; + const mini_bddt &y=t.y; + assert(x.is_initialized() && y.is_initialized()); + assert(x.node->mgr==y.node->mgr); + + switch(t.phase) + { + case stack_elementt::phaset::INIT: + { + // dynamic programming + Gt::const_iterator G_it=G.find(t.key); + if(G_it!=G.end()) + { + t.result=G_it->second; + stack.pop(); + } + else + { + if(x.is_constant() && y.is_constant()) + { + bool result_truth=fkt(x.is_true(), y.is_true()); + const mini_bdd_mgrt &mgr=*x.node->mgr; + t.result=result_truth?mgr.True():mgr.False(); + stack.pop(); + } + else if(x.var()==y.var()) + { + t.var=x.var(); + t.phase=stack_elementt::phaset::FINISH; + assert(x.low().var()>t.var); + assert(y.low().var()>t.var); + assert(x.high().var()>t.var); + assert(y.high().var()>t.var); + stack.push(stack_elementt(t.lr, x.low(), y.low())); + stack.push(stack_elementt(t.hr, x.high(), y.high())); + } + else if(x.var()t.var); + assert(x.high().var()>t.var); + stack.push(stack_elementt(t.lr, x.low(), y)); + stack.push(stack_elementt(t.hr, x.high(), y)); + } + else /* x.var() > y.var() */ + { + t.var=y.var(); + t.phase=stack_elementt::phaset::FINISH; + assert(y.low().var()>t.var); + assert(y.high().var()>t.var); + stack.push(stack_elementt(t.lr, x, y.low())); + stack.push(stack_elementt(t.hr, x, y.high())); + } + } + } + break; + + case stack_elementt::phaset::FINISH: + { + mini_bdd_mgrt *mgr=x.node->mgr; + t.result=mgr->mk(t.var, t.lr, t.hr); + G[t.key]=t.result; + stack.pop(); + } + break; + } + } + + assert(u.is_initialized()); + + return u; +} + bool equal_fkt(bool x, bool y) { return x==y; From a71ca413f8ae145161911ce939dd6b31a8c57b7b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 20 Jul 2017 22:29:42 +0100 Subject: [PATCH 03/33] disable linter for assertions --- src/solvers/miniBDD/miniBDD.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp index fc47235b076..aebe4e0a3a4 100644 --- a/src/solvers/miniBDD/miniBDD.cpp +++ b/src/solvers/miniBDD/miniBDD.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com void mini_bdd_nodet::remove_reference() { + // NOLINTNEXTLINE(build/deprecated) assert(reference_counter!=0); reference_counter--; @@ -208,7 +209,9 @@ class mini_bdd_applyt mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y) { + // NOLINTNEXTLINE(build/deprecated) assert(x.is_initialized() && y.is_initialized()); + // NOLINTNEXTLINE(build/deprecated) assert(x.node->mgr==y.node->mgr); // dynamic programming @@ -270,7 +273,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec( auto &t=stack.top(); const mini_bddt &x=t.x; const mini_bddt &y=t.y; + // NOLINTNEXTLINE(build/deprecated) assert(x.is_initialized() && y.is_initialized()); + // NOLINTNEXTLINE(build/deprecated) assert(x.node->mgr==y.node->mgr); switch(t.phase) @@ -297,9 +302,13 @@ mini_bddt mini_bdd_applyt::APP_non_rec( { t.var=x.var(); t.phase=stack_elementt::phaset::FINISH; + // NOLINTNEXTLINE(build/deprecated) assert(x.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(y.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(x.high().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(y.high().var()>t.var); stack.push(stack_elementt(t.lr, x.low(), y.low())); stack.push(stack_elementt(t.hr, x.high(), y.high())); @@ -308,7 +317,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec( { t.var=x.var(); t.phase=stack_elementt::phaset::FINISH; + // NOLINTNEXTLINE(build/deprecated) assert(x.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(x.high().var()>t.var); stack.push(stack_elementt(t.lr, x.low(), y)); stack.push(stack_elementt(t.hr, x.high(), y)); @@ -317,7 +328,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec( { t.var=y.var(); t.phase=stack_elementt::phaset::FINISH; + // NOLINTNEXTLINE(build/deprecated) assert(y.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(y.high().var()>t.var); stack.push(stack_elementt(t.lr, x, y.low())); stack.push(stack_elementt(t.hr, x, y.high())); @@ -337,6 +350,7 @@ mini_bddt mini_bdd_applyt::APP_non_rec( } } + // NOLINTNEXTLINE(build/deprecated) assert(u.is_initialized()); return u; @@ -364,6 +378,7 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const mini_bddt mini_bddt::operator!() const { + // NOLINTNEXTLINE(build/deprecated) assert(is_initialized()); return node->mgr->True()^*this; } @@ -406,8 +421,11 @@ mini_bddt mini_bdd_mgrt::mk( const mini_bddt &low, const mini_bddt &high) { + // NOLINTNEXTLINE(build/deprecated) assert(var<=var_table.size()); + // NOLINTNEXTLINE(build/deprecated) assert(low.var()>var); + // NOLINTNEXTLINE(build/deprecated) assert(high.var()>var); if(low.node_number()==high.node_number()) @@ -501,6 +519,7 @@ mini_bddt restrictt::RES(const mini_bddt &u) { // replace 'var' in 'u' by constant 'value' + // NOLINTNEXTLINE(build/deprecated) assert(u.is_initialized()); mini_bdd_mgrt *mgr=u.node->mgr; From d078dd89e5f57eb8a975972fe714513a710aeebc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 20 Jul 2017 08:40:47 +0100 Subject: [PATCH 04/33] Support out-of-bounds checks on arrays of dynamic size Previously the code would rely on type sizes being constant when building a subtraction; this is unnecessary as the expression is sent to the solver for evaluation anyway. --- regression/cbmc/dynamic_size1/main.c | 14 +++++++++ regression/cbmc/dynamic_size1/test.desc | 9 ++++++ .../value_set_dereference.cpp | 29 ++++++++++++------- 3 files changed, 42 insertions(+), 10 deletions(-) create mode 100644 regression/cbmc/dynamic_size1/main.c create mode 100644 regression/cbmc/dynamic_size1/test.desc diff --git a/regression/cbmc/dynamic_size1/main.c b/regression/cbmc/dynamic_size1/main.c new file mode 100644 index 00000000000..6cf9465f50f --- /dev/null +++ b/regression/cbmc/dynamic_size1/main.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + unsigned x; + + int *A=malloc(x*sizeof(int)); + + char *p=&A[1]; + + char c=*p; + + return c; +} diff --git a/regression/cbmc/dynamic_size1/test.desc b/regression/cbmc/dynamic_size1/test.desc new file mode 100644 index 00000000000..d110065a9cf --- /dev/null +++ b/regression/cbmc/dynamic_size1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +^unknown or invalid type size: diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index d2098ece102..87712e13bee 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -858,16 +859,24 @@ bool value_set_dereferencet::memory_model_bytes( { // upper bound { - mp_integer from_width=pointer_offset_size(from_type, ns); - if(from_width<=0) - throw "unknown or invalid type size:\n"+from_type.pretty(); - - mp_integer to_width= - to_type.id()==ID_empty?0: pointer_offset_size(to_type, ns); - if(to_width<0) - throw "unknown or invalid type size:\n"+to_type.pretty(); - - exprt bound=from_integer(from_width-to_width, offset.type()); + exprt from_width=size_of_expr(from_type, ns); + INVARIANT( + from_width.is_not_nil(), + "unknown or invalid type size:\n"+from_type.pretty()); + + exprt to_width= + to_type.id()==ID_empty? + from_integer(0, size_type()):size_of_expr(to_type, ns); + INVARIANT( + to_width.is_not_nil(), + "unknown or invalid type size:\n"+to_type.pretty()); + INVARIANT( + from_width.type()==to_width.type(), + "type mismatch on result of size_of_expr"); + + minus_exprt bound(from_width, to_width); + if(bound.type()!=offset.type()) + bound.make_typecast(offset.type()); binary_relation_exprt offset_upper_bound(offset, ID_gt, bound); From 6eef691b3cc0c95a4122d50c0405883921adda14 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 22 Jul 2017 12:12:16 +0100 Subject: [PATCH 05/33] More complete modelling of fgets fgets may (and certainly does when successful) change the contents of the buffer passed in. Building a regression test showed further deficiences in the stdio library model: 1) MacOS uses _fdopen; 2) fclose uses free from stdlib.h. --- regression/cbmc/fgets1/main.c | 22 ++++++++++++ regression/cbmc/fgets1/test.desc | 10 ++++++ src/ansi-c/library/stdio.c | 61 +++++++++++++++++++++++++++++++- 3 files changed, 92 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc/fgets1/main.c create mode 100644 regression/cbmc/fgets1/test.desc diff --git a/regression/cbmc/fgets1/main.c b/regression/cbmc/fgets1/main.c new file mode 100644 index 00000000000..8c4e418885b --- /dev/null +++ b/regression/cbmc/fgets1/main.c @@ -0,0 +1,22 @@ +#include +#include + +int main() +{ + char buffer[3]={'a', 'b', '\0'}; + FILE *f=fdopen(0, "r"); + if(!f) + return 1; + + char *p=fgets(buffer, 3, f); + if(p) + { + assert(buffer[1]==p[1]); + assert(buffer[2]=='\0'); + assert(p[1]=='b'); // expected to fail + } + + fclose(f); + + return 0; +} diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc new file mode 100644 index 00000000000..3a8c4e6a733 --- /dev/null +++ b/regression/cbmc/fgets1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--bounds-check --pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[main.assertion.3\] assertion p\[1\]=='b': FAILURE +\*\* 1 of 38 failed \(2 iterations\) +-- +^warning: ignoring diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index 5a9ab1e9d57..548e817e4b4 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -65,7 +65,14 @@ inline FILE *fopen(const char *filename, const char *mode) FILE *fopen_result; _Bool fopen_error; + + #if !defined(__linux__) || defined(__GLIBC__) fopen_result=fopen_error?NULL:malloc(sizeof(FILE)); + #else + // libraries need to expose the definition of FILE; this is the + // case for musl + fopen_result=fopen_error?NULL:malloc(sizeof(int)); + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_set_must(fopen_result, "open"); @@ -99,6 +106,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f) #define __CPROVER_STDIO_H_INCLUDED #endif +#ifndef __CPROVER_STDLIB_H_INCLUDED +#include +#define __CPROVER_STDLIB_H_INCLUDED +#endif + inline int fclose(FILE *stream) { __CPROVER_HIDE:; @@ -135,10 +147,47 @@ inline FILE *fdopen(int handle, const char *mode) "fdopen zero-termination of 2nd argument"); #endif + #if !defined(__linux__) || defined(__GLIBC__) + FILE *f=malloc(sizeof(FILE)); + #else + // libraries need to expose the definition of FILE; this is the + // case for musl + FILE *f=malloc(sizeof(int)); + #endif + + return f; +} + +/* FUNCTION: _fdopen */ + +// This is for Apple + +#ifndef __CPROVER_STDIO_H_INCLUDED +#include +#define __CPROVER_STDIO_H_INCLUDED +#endif + +#ifndef __CPROVER_STDLIB_H_INCLUDED +#include +#define __CPROVER_STDLIB_H_INCLUDED +#endif + +#ifdef __APPLE__ +inline FILE *_fdopen(int handle, const char *mode) +{ + __CPROVER_HIDE:; + (void)handle; + (void)*mode; + #ifdef __CPROVER_STRING_ABSTRACTION + __CPROVER_assert(__CPROVER_is_zero_string(mode), + "fdopen zero-termination of 2nd argument"); + #endif + FILE *f=malloc(sizeof(FILE)); return f; } +#endif /* FUNCTION: fgets */ @@ -147,7 +196,7 @@ inline FILE *fdopen(int handle, const char *mode) #define __CPROVER_STDIO_H_INCLUDED #endif -inline char *fgets(char *str, int size, FILE *stream) +char *fgets(char *str, int size, FILE *stream) { __CPROVER_HIDE:; __CPROVER_bool error; @@ -169,6 +218,16 @@ inline char *fgets(char *str, int size, FILE *stream) __CPROVER_is_zero_string(str)=!error; __CPROVER_zero_string_length(str)=resulting_size; } + #else + if(size>0) + { + int str_length; + __CPROVER_assume(str_length>=0 && str_length Date: Sat, 22 Jul 2017 12:15:14 +0100 Subject: [PATCH 06/33] Import getopt{,_long} and vasprintf models from SV-COMP/busybox Licensing: I had contributed these myself to the SV-COMP benchmarks. --- src/ansi-c/library/getopt.c | 63 +++++++++++++++++++++++++++++++------ src/ansi-c/library/stdio.c | 40 +++++++++++++++++++++++ 2 files changed, 94 insertions(+), 9 deletions(-) diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index d3eedda9814..458f9d2e414 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -3,22 +3,67 @@ extern char *optarg; extern int optind; +#ifndef __CPROVER_STRING_H_INCLUDED +#include +#define __CPROVER_STRING_H_INCLUDED +#endif + inline int getopt(int argc, char * const argv[], const char *optstring) { __CPROVER_HIDE:; - int result_index; - __CPROVER_assume(result_index>=0); - (void)*optstring; - if(optind>=argc) + int result=-1; + + if(optind==0) + optind=1; + + if(optind>=argc || argv[optind][0]!='-') return -1; - __CPROVER_assume(result_index=optind); + + size_t result_index; + __CPROVER_assume( + result_index +#define __CPROVER_STDIO_H_INCLUDED +#endif + +#ifndef __CPROVER_STDARG_H_INCLUDED +#include +#define __CPROVER_STDARG_H_INCLUDED +#endif + +#ifndef __CPROVER_STDLIB_H_INCLUDED +#include +#define __CPROVER_STDLIB_H_INCLUDED +#endif + +inline int vasprintf(char **ptr, const char *fmt, va_list ap) +{ + (void)*fmt; + (void)ap; + + int result_buffer_size; + if(result_buffer_size<=0) + return -1; + + *ptr=malloc(result_buffer_size); + for(int i=0; i Date: Thu, 3 Aug 2017 22:45:58 +0200 Subject: [PATCH 07/33] increased version number in preparation for release 5.8 --- src/cbmc/version.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cbmc/version.h b/src/cbmc/version.h index 017ded44272..58bdccf0018 100644 --- a/src/cbmc/version.h +++ b/src/cbmc/version.h @@ -1,6 +1,6 @@ #ifndef CPROVER_CBMC_VERSION_H #define CPROVER_CBMC_VERSION_H -#define CBMC_VERSION "5.7" +#define CBMC_VERSION "5.8" #endif // CPROVER_CBMC_VERSION_H From 439ef97b2b4dfb8b0c8a9831b373c0279e91e402 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 26 Jun 2017 23:30:53 +0100 Subject: [PATCH 08/33] fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc --- src/solvers/miniBDD/miniBDD.cpp | 16 +++++++++++----- src/solvers/miniBDD/miniBDD.h | 2 +- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp index aebe4e0a3a4..4c00b1de85b 100644 --- a/src/solvers/miniBDD/miniBDD.cpp +++ b/src/solvers/miniBDD/miniBDD.cpp @@ -463,14 +463,20 @@ mini_bddt mini_bdd_mgrt::mk( } bool mini_bdd_mgrt::reverse_keyt::operator<( - const mini_bdd_mgrt::reverse_keyt &other) const + const mini_bdd_mgrt::reverse_keyt &y) const { - if(varother.var || low>other.low) + else if(x.var>y.var) return false; - - return highy.low) + return false; + else + return x.high reverse_mapt; From 393256f5d2f6ede4d671c34494f80e17a38076b4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 4 Aug 2017 00:06:27 +0200 Subject: [PATCH 09/33] invariant_violated does not return --- src/util/invariant.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/invariant.h b/src/util/invariant.h index 325020a0d6e..a7df274e81d 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -149,6 +149,9 @@ void report_exception_to_stderr(const invariant_failedt &); /// \param params : (variadic) parameters to forward to ET's constructor /// its backtrace member will be set before it is used. template +#ifdef __GNUC__ +__attribute__((noreturn)) +#endif typename std::enable_if::value>::type invariant_violated_structured( const std::string &file, @@ -171,6 +174,9 @@ invariant_violated_structured( /// \param function : C string giving the name of the function. /// \param line : The line number of the invariant /// \param reason : brief description of the invariant violation. +#ifdef __GNUC__ +__attribute__((noreturn)) +#endif inline void invariant_violated_string( const std::string &file, const std::string &function, From ff945b3e2b56d8190a83d98473b5f5c9cda9800d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 23 Jul 2017 15:58:27 +0100 Subject: [PATCH 10/33] test for miniBDD --- unit/Makefile | 1 + unit/miniBDD_new.cpp | 277 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 278 insertions(+) create mode 100644 unit/miniBDD_new.cpp diff --git a/unit/Makefile b/unit/Makefile index 3e5bb48afbe..409402af1f1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -11,6 +11,7 @@ SRC += unit_tests.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ + miniBDD_new.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/miniBDD_new.cpp b/unit/miniBDD_new.cpp new file mode 100644 index 00000000000..0c176c7f82e --- /dev/null +++ b/unit/miniBDD_new.cpp @@ -0,0 +1,277 @@ +/*******************************************************************\ + + Module: Unit tests for miniBDD + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Unit tests for miniBDD + +#include + +#include +#include + +#include +#include +#include + +#include + +class bdd_propt:public propt +{ +public: + mini_bdd_mgrt &mgr; + + explicit bdd_propt(mini_bdd_mgrt &_mgr):mgr(_mgr) + { + // True and False + bdd_map.push_back(mgr.False()); + bdd_map.push_back(mgr.True()); + } + + mini_bddt to_bdd(literalt a) + { + if(a.is_true()) + return mgr.True(); + if(a.is_false()) + return mgr.False(); + INVARIANT(a.var_no() bdd_map; + + bool has_set_to() const override { return false; } + bool cnf_handled_well() const override { return false; } +}; + +SCENARIO("miniBDD", "[core][solver][miniBDD]") +{ + GIVEN("A bdd for x&!x") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + prop_conv_solvert solver(ns, bdd_prop); + + symbol_exprt var("x", bool_typet()); + literalt result= + solver.convert(and_exprt(var, not_exprt(var))); + + REQUIRE(result.is_false()); + } + + GIVEN("A bdd for x&!x==0") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(2); + symbol_exprt var("x", type); + equal_exprt equality( + bitand_exprt(var, bitnot_exprt(var)), + from_integer(0, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_true()); + } + + GIVEN("A bdd for x+x==1") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(32); + symbol_exprt var("x", type); + equal_exprt equality( + plus_exprt(var, var), + from_integer(1, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_false()); + } + + GIVEN("A bdd for x*y==y*x") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(4); + symbol_exprt var_x("x", type); + symbol_exprt var_y("y", type); + equal_exprt equality( + mult_exprt(var_x, var_y), + mult_exprt(var_y, var_x)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_true()); + } + + GIVEN("A bdd for x*x==2") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(8); + symbol_exprt var_x("x", type); + equal_exprt equality( + mult_exprt(var_x, var_x), + from_integer(2, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_false()); + } + + GIVEN("A bdd for x*x==4") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(8); + symbol_exprt var_x("x", type); + equal_exprt equality( + mult_exprt(var_x, var_x), + from_integer(4, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(!result.is_constant()); + } +} From 879a47b4622cfc19e7be712b716c9e720f989109 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 08:11:09 +0000 Subject: [PATCH 11/33] Symex support for lhs-typecasts and side effects --- src/path-symex/path_symex.cpp | 8 ++++++++ src/path-symex/path_symex_state_read.cpp | 9 ++++++++- src/path-symex/var_map.h | 10 ++++++++-- 3 files changed, 24 insertions(+), 3 deletions(-) diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index f64071ec617..6c86d9c416c 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -422,6 +422,14 @@ void path_symext::assign_rec( var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt(); } } + else if(ssa_lhs.id()==ID_typecast) + { + // dereferencing might yield a typecast + const exprt &new_lhs=to_typecast_expr(ssa_lhs).op(); + typecast_exprt new_rhs(ssa_rhs, new_lhs.type()); + + assign_rec(state, guard, new_lhs, new_rhs); + } else if(ssa_lhs.id()==ID_member) { #ifdef DEBUG diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp index 87dea21be4a..06a7f10f59d 100644 --- a/src/path-symex/path_symex_state_read.cpp +++ b/src/path-symex/path_symex_state_read.cpp @@ -247,7 +247,14 @@ exprt path_symex_statet::instantiate_rec( { irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count); var_map.nondet_count++; - return symbol_exprt(id, src.type()); + + auxiliary_symbolt nondet_symbol; + nondet_symbol.name=id; + nondet_symbol.base_name=id; + nondet_symbol.type=src.type(); + var_map.new_symbols.add(nondet_symbol); + + return nondet_symbol.symbol_expr(); } else throw "instantiate_rec: unexpected side effect "+id2string(statement); diff --git a/src/path-symex/var_map.h b/src/path-symex/var_map.h index 7b17169c441..09511174cab 100644 --- a/src/path-symex/var_map.h +++ b/src/path-symex/var_map.h @@ -18,12 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include class var_mapt { public: explicit var_mapt(const namespacet &_ns): - ns(_ns), shared_count(0), local_count(0), nondet_count(0), dynamic_count(0) + ns(_ns.get_symbol_table(), new_symbols), + shared_count(0), + local_count(0), + nondet_count(0), + dynamic_count(0) { } @@ -93,7 +98,8 @@ class var_mapt void init(var_infot &var_info); - const namespacet &ns; + const namespacet ns; + symbol_tablet new_symbols; void output(std::ostream &) const; From 08f1a9e1dc5e546d81baf1620a8d792b183dfa74 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:30:19 +0000 Subject: [PATCH 12/33] Extract elements of array, struct directly instead of simplifying vectors don't need to be handled, they have been removed via remove_vector. --- src/path-symex/path_symex.cpp | 78 ++++++++++++++++++++--------------- 1 file changed, 44 insertions(+), 34 deletions(-) diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index 6c86d9c416c..043ac0fb05c 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -549,14 +549,30 @@ void path_symext::assign_rec( assert(operands.size()==components.size()); - for(std::size_t i=0; i Date: Sun, 26 Jun 2016 13:32:51 +0000 Subject: [PATCH 13/33] Removed redundant get_pc() (there is pc()) --- src/path-symex/path_symex_state.cpp | 6 ------ src/path-symex/path_symex_state.h | 7 ++++--- src/symex/path_search.cpp | 4 ++-- 3 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 495f598202a..fe663da5b7c 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -41,12 +41,6 @@ path_symex_statet initial_state( return s; } -loc_reft path_symex_statet::get_pc() const -{ - assert(current_thread + #include "locs.h" #include "var_map.h" #include "path_symex_history.h" @@ -111,11 +113,9 @@ struct path_symex_statet current_thread=_thread; } - loc_reft get_pc() const; - goto_programt::const_targett get_instruction() const { - return locs[get_pc()].target; + return locs[pc()].target; } bool is_executable() const @@ -145,6 +145,7 @@ struct path_symex_statet loc_reft pc() const { + PRECONDITION(current_thread Date: Sun, 26 Jun 2016 13:42:44 +0000 Subject: [PATCH 14/33] Fix symex thread statistics --- src/symex/path_search.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 4a510d1840a..42de78a32f7 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -103,7 +103,7 @@ path_searcht::resultt path_searcht::operator()( if(number_of_steps%1000==0) { status() << "Queue " << queue.size() - << " thread " << state.get_current_thread() + << " thread " << state.get_current_thread()+1 << '/' << state.threads.size() << " PC " << state.pc() << messaget::eom; } From c69a21b1923f94a06f0ddb82415119aa197353f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:45:11 +0000 Subject: [PATCH 15/33] Extended symex progres statistics --- src/symex/path_search.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 42de78a32f7..2d7d8faedb6 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -102,10 +102,13 @@ path_searcht::resultt path_searcht::operator()( if(number_of_steps%1000==0) { + time_periodt running_time=current_time()-start_time; status() << "Queue " << queue.size() << " thread " << state.get_current_thread()+1 << '/' << state.threads.size() - << " PC " << state.pc() << messaget::eom; + << " PC " << state.pc() + << " [" << number_of_steps << " steps, " + << running_time << "s]" << messaget::eom; } // an error, possibly? From acdc797f7bdbab7fb255ec0d1dfdb4ba606134fd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:47:58 +0000 Subject: [PATCH 16/33] Symex: output instruction processing and loop unwinding like CBMC Unlike CBMC, all output is enabled in debug mode only. --- src/symex/path_search.cpp | 55 +++++++++++++++++++++++++++++++++++++-- src/symex/path_search.h | 2 ++ 2 files changed, 55 insertions(+), 2 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 2d7d8faedb6..639ee701d9d 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -267,6 +267,19 @@ bool path_searcht::drop_state(const statet &state) { goto_programt::const_targett pc=state.get_instruction(); + const source_locationt &source_location=pc->source_location; + + if(!source_location.is_nil() && + last_source_location!=source_location) + { + debug() << "SYMEX at file " << source_location.get_file() + << " line " << source_location.get_line() + << " function " << source_location.get_function() + << eom; + + last_source_location=source_location; + } + // depth limit if(depth_limit_set && state.get_depth()>depth_limit) return true; @@ -282,17 +295,55 @@ bool path_searcht::drop_state(const statet &state) // unwinding limit -- loops if(unwind_limit_set && state.get_instruction()->is_backwards_goto()) { + bool stop=false; + for(const auto &loop_info : state.unwinding_map) if(loop_info.second>unwind_limit) - return true; + { + stop=true; + break; + } + + const irep_idt id=goto_programt::loop_id(pc); + path_symex_statet::unwinding_mapt::const_iterator entry= + state.unwinding_map.find(state.pc()); + debug() << (stop?"Not unwinding":"Unwinding") + << " loop " << id << " iteration " + << (entry==state.unwinding_map.end()?-1:entry->second) + << " (" << unwind_limit << " max)" + << " " << source_location + << " thread " << state.get_current_thread() << eom; + + if(stop) + return true; } // unwinding limit -- recursion if(unwind_limit_set && state.get_instruction()->is_function_call()) { + bool stop=false; + for(const auto &rec_info : state.recursion_map) if(rec_info.second>unwind_limit) - return true; + { + stop=true; + break; + } + + exprt function=to_code_function_call(pc->code).function(); + const irep_idt id=function.get(ID_identifier); // could be nil + path_symex_statet::recursion_mapt::const_iterator entry= + state.recursion_map.find(id); + if(entry!=state.recursion_map.end()) + debug() << (stop?"Not unwinding":"Unwinding") + << " recursion " << id << " iteration " + << entry->second + << " (" << unwind_limit << " max)" + << " " << source_location + << " thread " << state.get_current_thread() << eom; + + if(stop) + return true; } if(pc->is_assume() && diff --git a/src/symex/path_search.h b/src/symex/path_search.h index ca570819cc8..e0a64270e22 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -137,6 +137,8 @@ class path_searcht:public safety_checkert bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set; enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; + + source_locationt last_source_location; }; #endif // CPROVER_SYMEX_PATH_SEARCH_H From 260e03d4184d8114ec58506662ffc31f18a69902 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:49:57 +0000 Subject: [PATCH 17/33] symex --max-search-time limit and cleanup All symex limits use value -1 as marking "not set". Use size_t for counting statistics. --- src/symex/path_search.cpp | 15 ++++++--- src/symex/path_search.h | 52 ++++++++++++++++--------------- src/symex/symex_parse_options.cpp | 5 +++ src/symex/symex_parse_options.h | 2 +- 4 files changed, 43 insertions(+), 31 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 639ee701d9d..b6743063401 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -281,19 +281,19 @@ bool path_searcht::drop_state(const statet &state) } // depth limit - if(depth_limit_set && state.get_depth()>depth_limit) + if(depth_limit>=0 && state.get_depth()>depth_limit) return true; // context bound - if(context_bound_set && state.get_no_thread_interleavings()>context_bound) + if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound) return true; // branch bound - if(branch_bound_set && state.get_no_branches()>branch_bound) + if(branch_bound>=0 && state.get_no_branches()>branch_bound) return true; // unwinding limit -- loops - if(unwind_limit_set && state.get_instruction()->is_backwards_goto()) + if(unwind_limit>=0 && pc->is_backwards_goto()) { bool stop=false; @@ -319,7 +319,7 @@ bool path_searcht::drop_state(const statet &state) } // unwinding limit -- recursion - if(unwind_limit_set && state.get_instruction()->is_function_call()) + if(unwind_limit>=0 && pc->is_function_call()) { bool stop=false; @@ -346,6 +346,11 @@ bool path_searcht::drop_state(const statet &state) return true; } + // search time limit (--max-search-time) + if(time_limit>=0 && + current_time().get_t()>start_time.get_t()+time_limit*1000) + return true; + if(pc->is_assume() && simplify_expr(pc->guard, ns).is_false()) { diff --git a/src/symex/path_search.h b/src/symex/path_search.h index e0a64270e22..4823998ef8a 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -26,10 +26,11 @@ class path_searcht:public safety_checkert safety_checkert(_ns), show_vcc(false), eager_infeasibility(false), - depth_limit_set(false), // no limit - context_bound_set(false), - unwind_limit_set(false), - branch_bound_set(false), + depth_limit(-1), // no limit + context_bound(-1), + branch_bound(-1), + unwind_limit(-1), + time_limit(-1), search_heuristic(search_heuristict::DFS) { } @@ -37,42 +38,43 @@ class path_searcht:public safety_checkert virtual resultt operator()( const goto_functionst &goto_functions); - void set_depth_limit(unsigned limit) + void set_depth_limit(int limit) { - depth_limit_set=true; depth_limit=limit; } - void set_context_bound(unsigned limit) + void set_context_bound(int limit) { - context_bound_set=true; context_bound=limit; } - void set_branch_bound(unsigned limit) + void set_branch_bound(int limit) { - branch_bound_set=true; branch_bound=limit; } - void set_unwind_limit(unsigned limit) + void set_unwind_limit(int limit) { - unwind_limit_set=true; unwind_limit=limit; } + void set_time_limit(int limit) + { + time_limit=limit; + } + bool show_vcc; bool eager_infeasibility; // statistics - unsigned number_of_dropped_states; - unsigned number_of_paths; - unsigned number_of_steps; - unsigned number_of_feasible_paths; - unsigned number_of_infeasible_paths; - unsigned number_of_VCCs; - unsigned number_of_VCCs_after_simplification; - unsigned number_of_failed_properties; + std::size_t number_of_dropped_states; + std::size_t number_of_paths; + std::size_t number_of_steps; + std::size_t number_of_feasible_paths; + std::size_t number_of_infeasible_paths; + std::size_t number_of_VCCs; + std::size_t number_of_VCCs_after_simplification; + std::size_t number_of_failed_properties; std::size_t number_of_locs; absolute_timet start_time; time_periodt sat_time; @@ -130,11 +132,11 @@ class path_searcht:public safety_checkert void initialize_property_map( const goto_functionst &goto_functions); - unsigned depth_limit; - unsigned context_bound; - unsigned branch_bound; - unsigned unwind_limit; - bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set; + int depth_limit; + int context_bound; + int branch_bound; + int unwind_limit; + int time_limit; enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 5fc475ee154..03a5486f0e1 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -186,6 +186,10 @@ int symex_parse_optionst::doit() path_search.set_unwind_limit( unsafe_string2unsigned(cmdline.get_value("unwind"))); + if(cmdline.isset("max-search-time")) + path_search.set_time_limit( + safe_string2unsigned(cmdline.get_value("max-search-time"))); + if(cmdline.isset("dfs")) path_search.set_dfs(); @@ -607,6 +611,7 @@ void symex_parse_optionst::help() " --depth nr limit search depth\n" " --context-bound nr limit number of context switches\n" " --branch-bound nr limit number of branches taken\n" + " --max-search-time s limit search to approximately s seconds\n" "\n" "Other options:\n" " --version show version and exit\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index b4fc6fe2e1c..a9f3d9e3e83 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -30,7 +30,7 @@ class optionst; #define SYMEX_OPTIONS \ "(function):" \ "D:I:" \ - "(depth):(context-bound):(branch-bound):(unwind):" \ + "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ From 73adfb0fe4bfd2337895bda90bfe1cfe092869fc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 19 Apr 2017 16:28:05 +0000 Subject: [PATCH 18/33] Perform function-pointer removal in symex --- src/symex/symex_parse_options.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 03a5486f0e1..c2e567cc643 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -304,6 +305,12 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // remove stuff remove_complex(goto_model); remove_vector(goto_model); + // remove function pointers + status() << "Removal of function pointers and virtual functions" << eom; + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); // Java throw and catch -> explicit exceptional return variables: From e2ed0df33a8f165cb11f1ab95dfc00e448a47eae Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 19 Jun 2017 13:54:56 +0100 Subject: [PATCH 19/33] Avoid using integer_typet where unsuitable The solver back end cannot necessarily handle unbounded integers. Do not use them unless explicitly requested/supported. --- .../java_bytecode_convert_method.cpp | 127 ++++++++++++------ src/java_bytecode/java_bytecode_parser.cpp | 50 +++---- .../java_local_variable_table.cpp | 11 +- src/solvers/flattening/boolbv_member.cpp | 3 +- src/solvers/flattening/pointer_logic.cpp | 3 +- src/util/std_expr.cpp | 10 +- src/util/std_expr.h | 2 - unit/analyses/ai/ai_simplify_lhs.cpp | 5 +- 8 files changed, 131 insertions(+), 80 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 5c2135e8afe..d97a769d59f 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -163,9 +164,11 @@ const exprt java_bytecode_convert_methodt::variable( size_t address, java_bytecode_convert_methodt::variable_cast_argumentt do_cast) { - irep_idt number=to_constant_expr(arg).get_value(); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg), number); + CHECK_RETURN(!ret); - std::size_t number_int=safe_string2size_t(id2string(number)); + std::size_t number_int=integer2size_t(number); typet t=java_type_from_char(type_char); variablest &var_list=variables[number_int]; @@ -176,7 +179,7 @@ const exprt java_bytecode_convert_methodt::variable( if(var.symbol_expr.get_identifier().empty()) { // an unnamed local variable - irep_idt base_name="anonlocal::"+id2string(number)+type_char; + irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char; irep_idt identifier=id2string(current_method)+"::"+id2string(base_name); symbol_exprt result(identifier, t); @@ -848,8 +851,9 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(!i_it->args.empty()); - const unsigned target=safe_string2unsigned( - id2string(to_constant_expr(i_it->args[0]).get_value())); + unsigned target; + bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target); + DATA_INVARIANT(!ret, "target expected to be unsigned integer"); targets.insert(target); a_entry.first->second.successors.push_back(target); @@ -873,8 +877,9 @@ codet java_bytecode_convert_methodt::convert_instructions( { if(is_label) { - const unsigned target=safe_string2unsigned( - id2string(to_constant_expr(arg).get_value())); + unsigned target; + bool ret=to_unsigned_integer(to_constant_expr(arg), target); + DATA_INVARIANT(!ret, "target expected to be unsigned integer"); targets.insert(target); a_entry.first->second.successors.push_back(target); } @@ -955,9 +960,11 @@ codet java_bytecode_convert_methodt::convert_instructions( statement[statement.size()-2]=='_' && isdigit(statement[statement.size()-1])) { - arg0=constant_exprt( - std::string(id2string(statement), statement.size()-1, 1), - integer_typet()); + arg0= + from_integer( + string2integer( + std::string(id2string(statement), statement.size()-1, 1)), + java_int_type()); statement=std::string(id2string(statement), 0, statement.size()-2); } @@ -1353,16 +1360,20 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="goto" || statement=="goto_w") { assert(op.empty() && results.empty()); - irep_idt number=to_constant_expr(arg0).get_value(); - code_gotot code_goto(label(number)); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + INVARIANT(!ret, "goto argument should be an integer"); + code_gotot code_goto(label(integer2string(number))); c=code_goto; } else if(statement=="jsr" || statement=="jsr_w") { // As 'goto', except we must also push the subroutine return address: assert(op.empty() && results.size()==1); - irep_idt number=to_constant_expr(arg0).get_value(); - code_gotot code_goto(label(number)); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + INVARIANT(!ret, "jsr argument should be an integer"); + code_gotot code_goto(label(integer2string(number))); c=code_goto; results[0]= from_integer( @@ -1422,9 +1433,13 @@ codet java_bytecode_convert_methodt::convert_instructions( ieee_float_spect::double_precision()); ieee_floatt value(spec); - const typet &arg_type(arg0.type()); - if(ID_integer==arg_type.id()) - value.from_integer(arg0.get_int(ID_value)); + if(arg0.type().id()!=ID_floatbv) + { + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + DATA_INVARIANT(!ret, "failed to convert constant"); + value.from_integer(number); + } else value.from_expr(to_constant_expr(arg0)); @@ -1432,23 +1447,29 @@ codet java_bytecode_convert_methodt::convert_instructions( } else { - const unsigned value(arg0.get_unsigned_int(ID_value)); + mp_integer value; + bool ret=to_integer(to_constant_expr(arg0), value); + DATA_INVARIANT(!ret, "failed to convert constant"); const typet type=java_type_from_char(statement[0]); results[0]=from_integer(value, type); } } else if(statement==patternt("?ipush")) { - assert(results.size()==1); - mp_integer int_value; - bool ret=to_integer(to_constant_expr(arg0), int_value); - INVARIANT(!ret, "?ipush argument should be an integer"); - results[0]=from_integer(int_value, java_int_type()); + PRECONDITION(results.size()==1); + DATA_INVARIANT( + arg0.id()==ID_constant, + "ipush argument expected to be constant"); + results[0]=arg0; + if(arg0.type()!=java_int_type()) + results[0].make_typecast(java_int_type()); } else if(statement==patternt("if_?cmp??")) { - irep_idt number=to_constant_expr(arg0).get_value(); assert(op.size()==2 && results.empty()); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + INVARIANT(!ret, "if_?cmp?? argument should be an integer"); code_ifthenelset code_branch; const irep_idt cmp_op=get_if_cmp_operator(statement); @@ -1463,7 +1484,7 @@ codet java_bytecode_convert_methodt::convert_instructions( code_branch.cond()=condition; code_branch.cond().add_source_location()=i_it->source_location; - code_branch.then_case()=code_gotot(label(number)); + code_branch.then_case()=code_gotot(label(integer2string(number))); code_branch.then_case().add_source_location()=i_it->source_location; code_branch.add_source_location()=i_it->source_location; @@ -1480,15 +1501,17 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=="ifle"?ID_le: (assert(false), ""); - irep_idt number=to_constant_expr(arg0).get_value(); assert(op.size()==1 && results.empty()); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + INVARIANT(!ret, "if?? argument should be an integer"); code_ifthenelset code_branch; code_branch.cond()= binary_relation_exprt(op[0], id, from_integer(0, op[0].type())); code_branch.cond().add_source_location()=i_it->source_location; code_branch.cond().add_source_location().set_function(method_id); - code_branch.then_case()=code_gotot(label(number)); + code_branch.then_case()=code_gotot(label(integer2string(number))); code_branch.then_case().add_source_location()=i_it->source_location; code_branch.then_case().add_source_location().set_function(method_id); code_branch.add_source_location()=i_it->source_location; @@ -1498,13 +1521,15 @@ codet java_bytecode_convert_methodt::convert_instructions( } else if(statement==patternt("ifnonnull")) { - irep_idt number=to_constant_expr(arg0).get_value(); assert(op.size()==1 && results.empty()); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + INVARIANT(!ret, "ifnonnull argument should be an integer"); code_ifthenelset code_branch; const typecast_exprt lhs(op[0], java_reference_type(empty_typet())); const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs); - code_branch.then_case()=code_gotot(label(number)); + code_branch.then_case()=code_gotot(label(integer2string(number))); code_branch.then_case().add_source_location()=i_it->source_location; code_branch.add_source_location()=i_it->source_location; @@ -1513,12 +1538,14 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement==patternt("ifnull")) { assert(op.size()==1 && results.empty()); - irep_idt number=to_constant_expr(arg0).get_value(); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg0), number); + INVARIANT(!ret, "ifnull argument should be an integer"); code_ifthenelset code_branch; const typecast_exprt lhs(op[0], java_reference_type(empty_typet())); const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs); - code_branch.then_case()=code_gotot(label(number)); + code_branch.then_case()=code_gotot(label(integer2string(number))); code_branch.then_case().add_source_location()=i_it->source_location; code_branch.add_source_location()=i_it->source_location; @@ -1540,9 +1567,12 @@ codet java_bytecode_convert_methodt::convert_instructions( code_assignt code_assign; code_assign.lhs()= variable(arg0, 'i', i_it->address, NO_CAST); + exprt arg1_int_type=arg1; + if(arg1.type()!=java_int_type()) + arg1_int_type.make_typecast(java_int_type()); code_assign.rhs()=plus_exprt( variable(arg0, 'i', i_it->address, CAST_AS_NEEDED), - typecast_exprt(arg1, java_int_type())); + arg1_int_type); block.copy_to_operands(code_assign); c=block; } @@ -1579,10 +1609,16 @@ codet java_bytecode_convert_methodt::convert_instructions( const std::size_t width=type.get_size_t(ID_width); typet target=unsignedbv_typet(width); - const typecast_exprt lhs(op[0], target); - const typecast_exprt rhs(op[1], target); + exprt lhs=op[0]; + if(lhs.type()!=target) + lhs.make_typecast(target); + exprt rhs=op[1]; + if(rhs.type()!=target) + rhs.make_typecast(target); - results[0]=typecast_exprt(lshr_exprt(lhs, rhs), op[0].type()); + results[0]=lshr_exprt(lhs, rhs); + if(results[0].type()!=op[0].type()) + results[0].make_typecast(op[0].type()); } else if(statement==patternt("?add")) { @@ -1815,7 +1851,10 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement==patternt("?2?")) // i2c etc. { assert(op.size()==1 && results.size()==1); - results[0]=typecast_exprt(op[0], java_type_from_char(statement[2])); + typet type=java_type_from_char(statement[2]); + results[0]=op[0]; + if(results[0].type()!=type) + results[0].make_typecast(type); } else if(statement=="new") { @@ -1901,8 +1940,10 @@ codet java_bytecode_convert_methodt::convert_instructions( { // The first argument is the type, the second argument is the number of // dimensions. The size of each dimension is on the stack. - irep_idt number=to_constant_expr(arg1).get_value(); - std::size_t dimension=safe_string2size_t(id2string(number)); + mp_integer number; + bool ret=to_integer(to_constant_expr(arg1), number); + INVARIANT(!ret, "multianewarray argument should be an integer"); + std::size_t dimension=integer2size_t(number); op=pop(dimension); assert(results.size()==1); @@ -1976,8 +2017,10 @@ codet java_bytecode_convert_methodt::convert_instructions( code_switch_caset code_case; code_case.add_source_location()=i_it->source_location; - irep_idt number=to_constant_expr(*a_it).get_value(); - code_case.code()=code_gotot(label(number)); + mp_integer number; + bool ret=to_integer(to_constant_expr(*a_it), number); + DATA_INVARIANT(!ret, "case label expected to be integer"); + code_case.code()=code_gotot(label(integer2string(number))); code_case.code().add_source_location()=i_it->source_location; if(a_it==i_it->args.begin()) @@ -1986,7 +2029,9 @@ codet java_bytecode_convert_methodt::convert_instructions( { instructiont::argst::const_iterator prev=a_it; prev--; - code_case.case_op()=typecast_exprt(*prev, op[0].type()); + code_case.case_op()=*prev; + if(code_case.case_op().type()!=op[0].type()) + code_case.case_op().make_typecast(op[0].type()); code_case.case_op().add_source_location()=i_it->source_location; } diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index d24141b76da..f93818eb274 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -703,7 +703,7 @@ void java_bytecode_parsert::rbytecode( case 'b': // a signed byte { s1 c=read_u1(); - instruction.args.push_back(from_integer(c, integer_typet())); + instruction.args.push_back(from_integer(c, signedbv_typet(8))); } address+=1; @@ -712,8 +712,8 @@ void java_bytecode_parsert::rbytecode( case 'o': // two byte branch offset, signed { s2 offset=read_u2(); - instruction - .args.push_back(from_integer(address+offset, integer_typet())); + instruction.args.push_back( + from_integer(address+offset, signedbv_typet(16))); } address+=2; break; @@ -721,8 +721,8 @@ void java_bytecode_parsert::rbytecode( case 'O': // four byte branch offset, signed { s4 offset=read_u4(); - instruction - .args.push_back(from_integer(address+offset, integer_typet())); + instruction.args.push_back( + from_integer(address+offset, signedbv_typet(32))); } address+=4; break; @@ -730,7 +730,7 @@ void java_bytecode_parsert::rbytecode( case 'v': // local variable index (one byte) { u1 v=read_u1(); - instruction.args.push_back(from_integer(v, integer_typet())); + instruction.args.push_back(from_integer(v, unsignedbv_typet(8))); } address+=1; break; @@ -740,17 +740,17 @@ void java_bytecode_parsert::rbytecode( if(wide_instruction) { u2 v=read_u2(); - instruction.args.push_back(from_integer(v, integer_typet())); + instruction.args.push_back(from_integer(v, unsignedbv_typet(16))); s2 c=read_u2(); - instruction.args.push_back(from_integer(c, integer_typet())); + instruction.args.push_back(from_integer(c, signedbv_typet(16))); address+=4; } else // local variable index (one byte) plus one signed byte { u1 v=read_u1(); - instruction.args.push_back(from_integer(v, integer_typet())); + instruction.args.push_back(from_integer(v, unsignedbv_typet(8))); s1 c=read_u1(); - instruction.args.push_back(from_integer(c, integer_typet())); + instruction.args.push_back(from_integer(c, signedbv_typet(8))); address+=2; } break; @@ -760,9 +760,9 @@ void java_bytecode_parsert::rbytecode( u2 c=read_u2(); instruction.args.push_back(constant(c)); u1 b1=read_u1(); - instruction.args.push_back(from_integer(b1, integer_typet())); + instruction.args.push_back(from_integer(b1, unsignedbv_typet(8))); u1 b2=read_u1(); - instruction.args.push_back(from_integer(b2, integer_typet())); + instruction.args.push_back(from_integer(b2, unsignedbv_typet(8))); } address+=4; break; @@ -776,8 +776,8 @@ void java_bytecode_parsert::rbytecode( // now default value s4 default_value=read_u4(); - instruction.args - .push_back(from_integer(base_offset+default_value, integer_typet())); + instruction.args.push_back( + from_integer(base_offset+default_value, signedbv_typet(32))); address+=4; // number of pairs @@ -788,9 +788,10 @@ void java_bytecode_parsert::rbytecode( { s4 match=read_u4(); s4 offset=read_u4(); - instruction.args.push_back(from_integer(match, integer_typet())); - instruction.args - .push_back(from_integer(base_offset+offset, integer_typet())); + instruction.args.push_back( + from_integer(match, signedbv_typet(32))); + instruction.args.push_back( + from_integer(base_offset+offset, signedbv_typet(32))); address+=8; } } @@ -805,8 +806,8 @@ void java_bytecode_parsert::rbytecode( // now default value s4 default_value=read_u4(); - instruction.args - .push_back(from_integer(base_offset+default_value, integer_typet())); + instruction.args.push_back( + from_integer(base_offset+default_value, signedbv_typet(32))); address+=4; // now low value @@ -821,9 +822,9 @@ void java_bytecode_parsert::rbytecode( for(s4 i=low_value; i<=high_value; i++) { s4 offset=read_u4(); - instruction.args.push_back(from_integer(i, integer_typet())); - instruction.args - .push_back(from_integer(base_offset+offset, integer_typet())); + instruction.args.push_back(from_integer(i, signedbv_typet(32))); + instruction.args.push_back( + from_integer(base_offset+offset, signedbv_typet(32))); address+=4; } } @@ -834,7 +835,8 @@ void java_bytecode_parsert::rbytecode( u2 c=read_u2(); // constant-pool index instruction.args.push_back(constant(c)); u1 dimensions=read_u1(); // number of dimensions - instruction.args.push_back(from_integer(dimensions, integer_typet())); + instruction.args.push_back( + from_integer(dimensions, unsignedbv_typet(8))); address+=3; } break; @@ -862,7 +864,7 @@ void java_bytecode_parsert::rbytecode( case 's': // a signed short { s2 s=read_u2(); - instruction.args.push_back(from_integer(s, integer_typet())); + instruction.args.push_back(from_integer(s, signedbv_typet(16))); } address+=2; break; diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index 94d5062fb24..70b2568476a 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -13,6 +13,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_types.h" +#include +#include #include #include @@ -177,21 +179,22 @@ static bool is_store_to_slot( if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store")) return false; - std::string storeslot; + unsigned storeslotidx; if(inst.args.size()==1) { // Store with an argument: const auto &arg=inst.args[0]; - storeslot=id2string(to_constant_expr(arg).get_value()); + bool ret=to_unsigned_integer(to_constant_expr(arg), storeslotidx); + CHECK_RETURN(!ret); } else { // Store shorthands, like "store_0", "store_1" assert(prevstatement[6]=='_' && prevstatement.size()==8); - storeslot=prevstatement[7]; + std::string storeslot(1, prevstatement[7]); assert(isdigit(storeslot[0])); + storeslotidx=safe_string2unsigned(storeslot); } - auto storeslotidx=safe_string2unsigned(storeslot); return storeslotidx==slotidx; } diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp index 448e80f5653..0f01e2be959 100644 --- a/src/solvers/flattening/boolbv_member.cpp +++ b/src/solvers/flattening/boolbv_member.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include bvt boolbvt::convert_member(const member_exprt &expr) { @@ -24,7 +25,7 @@ bvt boolbvt::convert_member(const member_exprt &expr) return convert_bv( byte_extract_exprt(byte_extract_id(), struct_op, - from_integer(0, integer_typet()), + from_integer(0, index_type()), expr.type())); } else if(struct_op_type.id()==ID_struct) diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index 3f1ffd47798..1018dfca2b7 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -87,7 +88,7 @@ exprt pointer_logict::pointer_expr( constant_exprt null(type); null.set_value(ID_NULL); return plus_exprt(null, - from_integer(pointer.offset, integer_typet())); + from_integer(pointer.offset, pointer_diff_type())); } } else if(pointer.object==invalid_object) // INVALID? diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index cef9446e2e1..f57f4979630 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -135,7 +135,7 @@ void object_descriptor_exprt::build( assert(root_object().type().id()!=ID_empty); } -constant_exprt constant_exprt::integer_constant(unsigned v) +static constant_exprt integer_constant(unsigned v) { return constant_exprt(std::to_string(v), integer_typet()); } @@ -144,7 +144,7 @@ shift_exprt::shift_exprt( const exprt &_src, const irep_idt &_id, const std::size_t _distance): - binary_exprt(_src, _id, constant_exprt::integer_constant(_distance)) + binary_exprt(_src, _id, integer_constant(_distance)) { } @@ -152,7 +152,7 @@ extractbit_exprt::extractbit_exprt( const exprt &_src, const std::size_t _index): binary_predicate_exprt( - _src, ID_extractbit, constant_exprt::integer_constant(_index)) + _src, ID_extractbit, integer_constant(_index)) { } @@ -166,8 +166,8 @@ extractbits_exprt::extractbits_exprt( assert(_upper>=_lower); operands().resize(3); src()=_src; - upper()=constant_exprt::integer_constant(_upper); - lower()=constant_exprt::integer_constant(_lower); + upper()=integer_constant(_upper); + lower()=integer_constant(_lower); } /*******************************************************************\ diff --git a/src/util/std_expr.h b/src/util/std_expr.h index c4837be001a..a47c3afd684 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3710,8 +3710,6 @@ class constant_exprt:public exprt } bool value_is_zero_string() const; - - static constant_exprt integer_constant(unsigned); }; /*! \brief Cast a generic exprt to a \ref constant_exprt diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 2d276fdbbd8..d161df0bffb 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -16,6 +16,7 @@ #include #include +#include #include #include #include @@ -73,7 +74,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", const unsigned int array_size=5; array_typet array_type( - signedbv_typet(32), constant_exprt::integer_constant(array_size)); + signedbv_typet(32), from_integer(array_size, size_type())); // Verify the results of the setup REQUIRE_FALSE(compile_failed);\ @@ -137,7 +138,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", { REQUIRE(constant_array.operands().size()==i); constant_array.operands().push_back( - constant_exprt::integer_constant(i)); + from_integer(i, signedbv_typet(32))); } const index_exprt &index_expr= From a3578c0ae977fc8cb6967b0be55b0292943f2721 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Aug 2017 07:21:14 +0100 Subject: [PATCH 20/33] Avoid spurious signed/unsigned comparison warnings Follow-up to 260e03d4184d8: instead of using negative numbers to represent "limit not set", use the maximum value as default. --- src/symex/path_search.cpp | 10 +++++----- src/symex/path_search.h | 22 ++++++++++++---------- 2 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index b6743063401..2748119a320 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -281,15 +281,15 @@ bool path_searcht::drop_state(const statet &state) } // depth limit - if(depth_limit>=0 && state.get_depth()>depth_limit) + if(state.get_depth()>=depth_limit) return true; // context bound - if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound) + if(state.get_no_thread_interleavings()>=context_bound) return true; // branch bound - if(branch_bound>=0 && state.get_no_branches()>branch_bound) + if(state.get_no_branches()>=branch_bound) return true; // unwinding limit -- loops @@ -298,7 +298,7 @@ bool path_searcht::drop_state(const statet &state) bool stop=false; for(const auto &loop_info : state.unwinding_map) - if(loop_info.second>unwind_limit) + if(loop_info.second>=unwind_limit) { stop=true; break; @@ -324,7 +324,7 @@ bool path_searcht::drop_state(const statet &state) bool stop=false; for(const auto &rec_info : state.recursion_map) - if(rec_info.second>unwind_limit) + if(rec_info.second>=unwind_limit) { stop=true; break; diff --git a/src/symex/path_search.h b/src/symex/path_search.h index 4823998ef8a..f02b617ee40 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + class path_searcht:public safety_checkert { public: @@ -26,11 +28,11 @@ class path_searcht:public safety_checkert safety_checkert(_ns), show_vcc(false), eager_infeasibility(false), - depth_limit(-1), // no limit - context_bound(-1), - branch_bound(-1), - unwind_limit(-1), - time_limit(-1), + depth_limit(std::numeric_limits::max()), + context_bound(std::numeric_limits::max()), + branch_bound(std::numeric_limits::max()), + unwind_limit(std::numeric_limits::max()), + time_limit(std::numeric_limits::max()), search_heuristic(search_heuristict::DFS) { } @@ -132,11 +134,11 @@ class path_searcht:public safety_checkert void initialize_property_map( const goto_functionst &goto_functions); - int depth_limit; - int context_bound; - int branch_bound; - int unwind_limit; - int time_limit; + unsigned depth_limit; + unsigned context_bound; + unsigned branch_bound; + unsigned unwind_limit; + unsigned time_limit; enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; From de40333ebb808da1fe2e4a3bd4b9c3ca221ecd43 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 4 Aug 2017 14:27:34 +0200 Subject: [PATCH 21/33] fix vacuous conjuncts --- src/symex/path_search.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 2748119a320..54f15543430 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -293,7 +293,8 @@ bool path_searcht::drop_state(const statet &state) return true; // unwinding limit -- loops - if(unwind_limit>=0 && pc->is_backwards_goto()) + if(unwind_limit!=std::numeric_limits::max() && + pc->is_backwards_goto()) { bool stop=false; @@ -319,7 +320,8 @@ bool path_searcht::drop_state(const statet &state) } // unwinding limit -- recursion - if(unwind_limit>=0 && pc->is_function_call()) + if(unwind_limit!=std::numeric_limits::max() && + pc->is_function_call()) { bool stop=false; @@ -347,7 +349,7 @@ bool path_searcht::drop_state(const statet &state) } // search time limit (--max-search-time) - if(time_limit>=0 && + if(time_limit!=std::numeric_limits::max() && current_time().get_t()>start_time.get_t()+time_limit*1000) return true; From 548aeba6b9db02ddfe26ac6ddb4c079ae1284768 Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 4 Aug 2017 14:48:48 +0100 Subject: [PATCH 22/33] Stop using C headers --- src/util/ieee_float.cpp | 4 +--- src/util/pipe_stream.cpp | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 154ba29c558..ba9fb9ac857 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -8,9 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ieee_float.h" -// is yet to come -#include - +#include #include #include #include diff --git a/src/util/pipe_stream.cpp b/src/util/pipe_stream.cpp index 4306bce8e00..1ed29eb415c 100644 --- a/src/util/pipe_stream.cpp +++ b/src/util/pipe_stream.cpp @@ -23,9 +23,9 @@ Module: A stdin/stdout pipe as STL stream #else #include #include -#include #include #include +#include #endif #define READ_BUFFER_SIZE 1024 From 33811ce31d488789899ba6b4ad7b4fb5ecaf8730 Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 4 Aug 2017 14:53:24 +0100 Subject: [PATCH 23/33] Update coding standard --- CODING_STANDARD.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index 4d57b09da31..06c6bf53666 100644 --- a/CODING_STANDARD.md +++ b/CODING_STANDARD.md @@ -107,6 +107,9 @@ Here a few minimalistic coding rules for the CPROVER source tree. include in the source file. For example, given `foo.h` and `foo.cpp`, the line `#include "foo.h"` should precede all other include statements in `foo.cpp`. +- Use the C++ versions of C headers (e.g. `cmath` instead of `math.h`). + Some of the C headers use macros instead of functions which can have + unexpected consequences. # Makefiles - Each source file should appear on a separate line From 2f550767afc0c6767c85f9f11aae51d206a15f52 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Aug 2017 18:46:46 +0100 Subject: [PATCH 24/33] Enable extractbits over arbitrary types, fix byte extract omission Extractbits can safely be applied to any type as it just turns the bit sequence into a bitvector; thus use extractbits directly instead of performing type casts (which are not as generic) first. Fix a missing struct operands push where the operand had been constructed but was never used. Fixes: #1209 --- regression/cbmc/union9/main.c | 35 +++++++++++++++++++ regression/cbmc/union9/test.desc | 8 +++++ src/solvers/flattening/boolbv_extractbits.cpp | 9 ----- .../flattening/flatten_byte_operators.cpp | 17 ++++----- 4 files changed, 50 insertions(+), 19 deletions(-) create mode 100644 regression/cbmc/union9/main.c create mode 100644 regression/cbmc/union9/test.desc diff --git a/regression/cbmc/union9/main.c b/regression/cbmc/union9/main.c new file mode 100644 index 00000000000..676048e49c8 --- /dev/null +++ b/regression/cbmc/union9/main.c @@ -0,0 +1,35 @@ +#include +#include + +typedef union { + struct { + uint8_t x; + uint8_t z; + } b; +} union_t; + +typedef struct { + uint32_t magic; + union_t unions[]; +} flex; + +int flex_init(flex * flex, size_t num) +{ + if (num == 0 || num >= 200) { + return -1; + } + flex->unions[num - 1].b.z = 255; + return 0; +} + +int main() { + uint8_t num = nondet_size(); + flex * pool = (flex *) malloc(sizeof(flex) + num * sizeof(union_t)); + int ret = flex_init(pool, num); + if (num > 0 && num < 200) { + __CPROVER_assert(ret == 0, "Accept inside range"); + } else { + __CPROVER_assert(ret != 0, "Reject outside range"); + } +} + diff --git a/regression/cbmc/union9/test.desc b/regression/cbmc/union9/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/union9/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 3b363a6367d..4f549139feb 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -17,15 +17,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) if(width==0) return conversion_failed(expr); - const irep_idt &type_id=expr.type().id(); - - if(type_id!=ID_signedbv && - type_id!=ID_unsignedbv && - type_id!=ID_c_enum && - type_id!=ID_c_enum_tag && - type_id!=ID_bv) - return conversion_failed(expr); - if(expr.operands().size()!=3) { error().source_location=expr.find_source_location(); diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index b5837f3206e..1d431c083c4 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -109,8 +109,8 @@ static exprt unpack_rec( } else if(type.id()!=ID_empty) { - // a basic type; we turn that into logical right shift and - // extractbits while considering endianness + // a basic type; we turn that into extractbits while considering + // endianness mp_integer bits=pointer_offset_bits(type, ns); if(bits<0) { @@ -121,17 +121,12 @@ static exprt unpack_rec( bits*=8; } - // cast to generic bit-vector - typecast_exprt src_tc(src, unsignedbv_typet(integer2size_t(bits))); - for(mp_integer i=0; i Date: Fri, 11 Mar 2016 17:37:49 +0000 Subject: [PATCH 25/33] goto-analyzer needs solvers (once BDDs are used in guardt), add binary --- src/goto-analyzer/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index da9e1c50d7d..07d8afa2050 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -18,7 +18,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../json/json$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../solvers/solvers$(LIBEXT) INCLUDES= -I .. From 0fc38547164a8a790edd335d0b6c3962325b0d75 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Jan 2016 14:39:55 +0100 Subject: [PATCH 26/33] Use BDDs to simplify guard expressions --- src/util/guard.cpp | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/util/guard.cpp b/src/util/guard.cpp index 693b48602c9..3c5289ca2ee 100644 --- a/src/util/guard.cpp +++ b/src/util/guard.cpp @@ -13,8 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + +#include "namespace.h" #include "std_expr.h" #include "simplify_utils.h" +#include "symbol_table.h" void guardt::guard_expr(exprt &dest) const { @@ -139,7 +143,11 @@ guardt &operator |= (guardt &g1, const guardt &g2) else g1=or_exprt(g1, g2); - // TODO: make simplify more capable and apply here + symbol_tablet symbol_table; + namespacet ns(symbol_table); + bdd_exprt t(ns); + t.from_expr(g1); + g1=t.as_expr(); return g1; } @@ -196,8 +204,15 @@ guardt &operator |= (guardt &g1, const guardt &g2) { } else - // TODO: make simplify more capable and apply here + { g1.add(or_exprt(and_expr1, and_expr2)); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + bdd_exprt t(ns); + t.from_expr(g1); + g1=t.as_expr(); + } } return g1; From db496e8fbf839e099da8de01b41123f4b80bd050 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 2 Aug 2016 03:19:05 +0200 Subject: [PATCH 27/33] BDDs require a namespace - pass one to guardt's or operator --- src/goto-symex/goto_symex_state.cpp | 4 ++-- src/goto-symex/symex_atomic_section.cpp | 4 ++-- src/goto-symex/symex_goto.cpp | 6 ++++-- src/util/guard.cpp | 17 +++++------------ src/util/guard.h | 4 +++- 5 files changed, 16 insertions(+), 19 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 6402923c4cf..c210f6bb327 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -575,7 +575,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // that implies the current one return false; - write_guard|=*it; + write_guard.logical_or(*it, ns); } } @@ -600,7 +600,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // that implies the current one return false; - read_guard|=*it; + read_guard.logical_or(*it, ns); } exprt cond=read_guard.as_expr(); diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp index c243cafbcd4..1922ffb8e76 100644 --- a/src/goto-symex/symex_atomic_section.cpp +++ b/src/goto-symex/symex_atomic_section.cpp @@ -57,7 +57,7 @@ void goto_symext::symex_atomic_end(statet &state) it=++(r_it->second.second.begin()); it!=r_it->second.second.end(); ++it) - read_guard|=*it; + read_guard.logical_or(*it, ns); exprt read_guard_expr=read_guard.as_expr(); do_simplify(read_guard_expr); @@ -83,7 +83,7 @@ void goto_symext::symex_atomic_end(statet &state) it=++(w_it->second.begin()); it!=w_it->second.end(); ++it) - write_guard|=*it; + write_guard.logical_or(*it, ns); exprt write_guard_expr=write_guard.as_expr(); do_simplify(write_guard_expr); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index a86efc0815e..02689b9baed 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -235,9 +235,11 @@ void goto_symext::merge_goto( const statet::goto_statet &goto_state, statet &state) { + statet::goto_statet &goto_state=*list_it; + // check atomic section if(state.atomic_section_id!=goto_state.atomic_section_id) - throw "atomic sections differ across branches"; + throw "Atomic sections differ across branches"; // do SSA phi functions phi_function(goto_state, state); @@ -245,7 +247,7 @@ void goto_symext::merge_goto( merge_value_sets(goto_state, state); // adjust guard - state.guard|=goto_state.guard; + state.guard.logical_or(goto_state.guard, ns); // adjust depth state.depth=std::min(state.depth, goto_state.depth); diff --git a/src/util/guard.cpp b/src/util/guard.cpp index 3c5289ca2ee..53b27103e33 100644 --- a/src/util/guard.cpp +++ b/src/util/guard.cpp @@ -123,15 +123,12 @@ guardt &operator -= (guardt &g1, const guardt &g2) return g1; } -guardt &operator |= (guardt &g1, const guardt &g2) +guardt& guardt::logical_or(const guardt &g2, const namespacet &ns) { - if(g2.is_false() || g1.is_true()) - return g1; - if(g1.is_false() || g2.is_true()) - { - g1=g2; - return g1; - } + guardt &g1=*this; + + if(g2.is_false() || g1.is_true()) return g1; + if(g1.is_false() || g2.is_true()) { g1=g2; return g1; } if(g1.id()!=ID_and || g2.id()!=ID_and) { @@ -143,8 +140,6 @@ guardt &operator |= (guardt &g1, const guardt &g2) else g1=or_exprt(g1, g2); - symbol_tablet symbol_table; - namespacet ns(symbol_table); bdd_exprt t(ns); t.from_expr(g1); g1=t.as_expr(); @@ -207,8 +202,6 @@ guardt &operator |= (guardt &g1, const guardt &g2) { g1.add(or_exprt(and_expr1, and_expr2)); - symbol_tablet symbol_table; - namespacet ns(symbol_table); bdd_exprt t(ns); t.from_expr(g1); g1=t.as_expr(); diff --git a/src/util/guard.h b/src/util/guard.h index a923680e2ad..5fe8f75dec9 100644 --- a/src/util/guard.h +++ b/src/util/guard.h @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr.h" +class namespacet; + class guardt:public exprt { public: @@ -61,7 +63,7 @@ class guardt:public exprt #endif friend guardt &operator -= (guardt &g1, const guardt &g2); - friend guardt &operator |= (guardt &g1, const guardt &g2); + guardt& logical_or(const guardt &g2, const namespacet &ns); #if 0 void swap(guardt &g) From 5a0c4889b7c99f845268da548507d86d77867680 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 2 Aug 2016 03:19:50 +0200 Subject: [PATCH 28/33] guardt::operator-=: use member function instead of friend --- src/util/guard.cpp | 4 +++- src/util/guard.h | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/util/guard.cpp b/src/util/guard.cpp index 53b27103e33..73102e0aea2 100644 --- a/src/util/guard.cpp +++ b/src/util/guard.cpp @@ -94,8 +94,10 @@ void guardt::add(const exprt &expr) op.push_back(expr); } -guardt &operator -= (guardt &g1, const guardt &g2) +guardt& guardt::operator -= (const guardt &g2) { + guardt &g1=*this; + if(g1.id()!=ID_and || g2.id()!=ID_and) return g1; diff --git a/src/util/guard.h b/src/util/guard.h index 5fe8f75dec9..6cef54f7580 100644 --- a/src/util/guard.h +++ b/src/util/guard.h @@ -62,7 +62,7 @@ class guardt:public exprt void make_false(); #endif - friend guardt &operator -= (guardt &g1, const guardt &g2); + guardt& operator -= (const guardt &g2); guardt& logical_or(const guardt &g2, const namespacet &ns); #if 0 From a3b580811b70c66665d32f69907cc5d48908da7c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Dec 2016 01:12:54 +0000 Subject: [PATCH 29/33] fixup! goto-analyzer needs solvers (once BDDs are used in guardt), add binary --- src/goto-cc/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 576a5e39505..c9b5fa4b732 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -28,7 +28,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../miniz/miniz$(OBJEXT) \ - ../json/json$(LIBEXT) + ../json/json$(LIBEXT) \ + ../solvers/solvers$(LIBEXT) INCLUDES= -I .. From 4b2774bca13fde38a84419359b905eeff86dd33d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Dec 2016 01:13:52 +0000 Subject: [PATCH 30/33] bdd -> exprt: fix copy&paste error to avoid a && TRUE --- src/solvers/prop/bdd_expr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 2a5b4ffa786..01dacc19048 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -122,7 +122,7 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const } else if(r.high().is_false()) { - if(r.high().is_true()) + if(r.low().is_true()) return not_exprt(n_expr); else return and_exprt(not_exprt(n_expr), as_expr(r.low())); From 255f431ba7e5e53562b9ea669bb7f0e78f8ca021 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Dec 2016 01:16:00 +0000 Subject: [PATCH 31/33] Alternative bdd -> exprt translation expanding ID_if Quantifier flatting presently cannot cope with ID_if. --- src/solvers/prop/bdd_expr.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 01dacc19048..251a70ef97e 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -132,7 +132,14 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const else if(r.high().is_true()) return or_exprt(n_expr, as_expr(r.low())); else + #if 0 + return + and_exprt( + or_exprt(not_exprt(n_expr), as_expr(r.high())), + or_exprt(n_expr, as_expr(r.low()))); + #else return if_exprt(n_expr, as_expr(r.high()), as_expr(r.low())); + #endif } exprt bdd_exprt::as_expr() const From 0696c4e52d1b42ae67c0bd48c31899e26a671175 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Dec 2016 01:19:25 +0000 Subject: [PATCH 32/33] Simplify ID_and, ID_or, ID_xor via BDDs - disabled At present, this breaks several cbmc/Quantifier* regression tests as it seemingly yields expressions of a shape not expected by that code. --- src/util/simplify_expr_boolean.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 238dfd384c9..bb8579bd3c1 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -11,8 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "expr.h" #include "namespace.h" +#include "simplify_utils.h" #include "std_expr.h" bool simplify_exprt::simplify_boolean(exprt &expr) @@ -79,6 +82,21 @@ bool simplify_exprt::simplify_boolean(exprt &expr) if(operands.empty()) return true; + #if 0 + bdd_exprt t(ns); + t.from_expr(expr); + exprt tmp=t.as_expr(); + sort_and_join(tmp); + + if(tmp!=expr) + { + expr.swap(tmp); + return false; + } + + return true; + #else + bool result=true; exprt::operandst::const_iterator last; @@ -183,6 +201,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr) } return result; + #endif } return true; From 02a62887e49d1b1be783acc05c0c611782a44a71 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 31 Dec 2016 18:02:15 +0100 Subject: [PATCH 33/33] Avoid use of sort_and_join in guard operations --- src/goto-symex/goto_symex_state.h | 1 + src/goto-symex/symex_goto.cpp | 33 +++++++++++++++++++++++++++++-- src/util/guard.cpp | 16 +++++++++++++++ 3 files changed, 48 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index d62d4a66af9..bfe52a44779 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -193,6 +193,7 @@ class goto_symex_statet value_sett value_set; guardt guard; symex_targett::sourcet source; + guardt guard_before_branch; propagationt propagation; unsigned atomic_section_id; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 02689b9baed..0784a408e54 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -175,6 +175,7 @@ void goto_symext::symex_goto(statet &state) state.rename(guard_expr, ns); } + new_state.guard_before_branch=state.guard; if(forward) { new_state.guard.add(guard_expr); @@ -280,10 +281,38 @@ void goto_symext::phi_function( if(!variables.empty()) { - diff_guard=goto_state.guard; + guardt tmp_guard(goto_state.guard); + guardt tmp_guard2(goto_state.guard); // this gets the diff between the guards - diff_guard-=dest_state.guard; + // tmp_guard-=dest_state.guard; + if(!goto_state.guard_before_branch.is_constant()) + { + assert(tmp_guard2.id()==ID_and); + + if(goto_state.guard_before_branch.id()==ID_and) + { + assert(tmp_guard2.operands().size()> + goto_state.guard_before_branch.operands().size()); + for(const auto & op : goto_state.guard_before_branch.operands()) + { + // assert(tmp_guard2.operands().front()==op); + (void)op; + tmp_guard2.operands().erase(tmp_guard2.operands().begin()); + } + } + else + { + assert(tmp_guard2.operands().front()== + goto_state.guard_before_branch); + tmp_guard2.operands().erase(tmp_guard2.operands().begin()); + } + + if(tmp_guard2.operands().size()==1) + tmp_guard2=tmp_guard2.op0(); + } + // assert(tmp_guard==tmp_guard2); + diff_guard=tmp_guard2; } for(std::unordered_set::const_iterator diff --git a/src/util/guard.cpp b/src/util/guard.cpp index 73102e0aea2..220684914f8 100644 --- a/src/util/guard.cpp +++ b/src/util/guard.cpp @@ -132,6 +132,22 @@ guardt& guardt::logical_or(const guardt &g2, const namespacet &ns) if(g2.is_false() || g1.is_true()) return g1; if(g1.is_false() || g2.is_true()) { g1=g2; return g1; } + { + exprt tmp(g2); + tmp.make_not(); + + if(tmp==g1) + g1.make_true(); + else + g1=or_exprt(g1, g2); + + bdd_exprt t(ns); + t.from_expr(g1); + g1=t.as_expr(); + + return g1; + } + if(g1.id()!=ID_and || g2.id()!=ID_and) { exprt tmp(g2);