From 646cf29941499e1d3c774f83739b3a84ad46de9a Mon Sep 17 00:00:00 2001 From: johndumbell Date: Thu, 3 May 2018 14:03:02 +0100 Subject: [PATCH 1/2] Add nondet assignment to non-zero'd allocations in symex This change means that if a generation zero symex variable is seen it can be assumed to not have been allocated at any point and still have its default values. We use this knowledge to then not add a guard on a phi merge that has a gen zero on its lhs or rhs, instead just simply assigning the other side directly. --- .../PhiMergeUninitialized.class | Bin 0 -> 1495 bytes .../PhiMergeUninitialized.java | 54 +++++++++++++++++ .../phi-merge_uninitialized_values/field.desc | 16 +++++ .../phi-merge_uninitialized_values/local.desc | 16 +++++ .../static_field.desc | 16 +++++ .../dynamic.desc | 16 +++++ .../global.desc | 16 +++++ .../phi-merge_uninitialized_values/local.desc | 16 +++++ .../static_local.desc | 16 +++++ .../phi-merge_uninitialized_values/test.c | 56 ++++++++++++++++++ src/goto-symex/goto_symex.cpp | 10 +++- src/goto-symex/goto_symex.h | 2 + src/goto-symex/symex_builtin_functions.cpp | 6 ++ src/goto-symex/symex_goto.cpp | 12 ++++ 14 files changed, 250 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.class create mode 100644 regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.java create mode 100644 regression/cbmc-java/phi-merge_uninitialized_values/field.desc create mode 100644 regression/cbmc-java/phi-merge_uninitialized_values/local.desc create mode 100644 regression/cbmc-java/phi-merge_uninitialized_values/static_field.desc create mode 100644 regression/cbmc/phi-merge_uninitialized_values/dynamic.desc create mode 100644 regression/cbmc/phi-merge_uninitialized_values/global.desc create mode 100644 regression/cbmc/phi-merge_uninitialized_values/local.desc create mode 100644 regression/cbmc/phi-merge_uninitialized_values/static_local.desc create mode 100644 regression/cbmc/phi-merge_uninitialized_values/test.c diff --git a/regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.class b/regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.class new file mode 100644 index 0000000000000000000000000000000000000000..1f36e928d7aa2be3ff88fd70e5d81944a6986b0a GIT binary patch literal 1495 zcmZ{k+fNfg6vn^lwk%y1DWxsN3l{~2f>Z@X1uw`YAt`EtlHl969bs|Vn(bnuZ~hHF z$%`*0y!hgkL=t`XZ!*Sjy0u%ibd%YcGiT=f&UeoC$FHy708HVIfi8?2n80}*lLj>8 zbzCqILq3j9T#VClNyn6dIL4J_S`C+VTrn_%t2(X;#OI~IB|Y161k4rJmEMA5Rjabf zt)-`1az}bL;c*rIFJghrXkpuWX5}5r-OS&qR2*r!vtuj7sT8*b zblD@g)51@nbIrF(Pgbp`H6ZFw(3(j9gvmCk@y}NKT*;|RV60Vky^>tERl>(x zYCNfEO=QuhFuecK7CHIQkvg8YNho-vNY`9_|`?}@qGH><)+v3FN5j9;=U7|fx?I>8L zuJFQI%d(ajx=w3uVn6 zK)mN9f)gCuYDR&RoST6IPNAPGDvUvn>hN1c83>pg|ANSCbRR<7$R&7Fbafxc4iV!j zb%3_j5776Jn)rnFMCuJX4iVotfbm@!-toLvi1H}GcacnT_tNLuNBu7UGP*|@V9;PiwvA7Snz5lC2| zgk0C?G9O?nxIz +#include + +void dynamicAllocationUninitialized(int trigger) +{ + int *obj; + if(trigger) + { + obj = (int *)malloc(sizeof(int)); + *obj = 42; + } + else + { + obj = (int *)malloc(sizeof(int)); + *obj = 76; + } + + assert(*obj == 42); +} + +int global; +void globalUninitialized(int trigger) +{ + if(trigger) + { + global = 44; + } + else + { + global = 20; + } + + assert(global == 44); +} + +void staticLocalUninitialized(int trigger) +{ + static int staticLocal; + if(trigger) + { + staticLocal = 43; + } + + assert(staticLocal == 43); +} + +void localUninitialized(int trigger) +{ + int local; + if(trigger) + { + local = 24; + } + + assert(local == 24); +} diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index bfd37cee334..3a5bea45c52 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -22,13 +22,19 @@ void goto_symext::do_simplify(exprt &expr) simplify(expr, ns); } +nondet_symbol_exprt goto_symext::build_symex_nondet(typet &type) +{ + irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++); + nondet_symbol_exprt new_expr(identifier, type); + return new_expr; +} + void goto_symext::replace_nondet(exprt &expr) { if(expr.id()==ID_side_effect && expr.get(ID_statement)==ID_nondet) { - irep_idt identifier="symex::nondet"+std::to_string(nondet_count++); - nondet_symbol_exprt new_expr(identifier, expr.type()); + nondet_symbol_exprt new_expr = build_symex_nondet(expr.type()); new_expr.add_source_location()=expr.source_location(); expr.swap(new_expr); } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 117693b8391..0c6c7e3b637 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -376,6 +376,8 @@ class goto_symext exprt &code, const irep_idt &identifier); + nondet_symbol_exprt build_symex_nondet(typet &type); + // exceptions void symex_throw(statet &); void symex_catch(statet &); diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index f827f1ecaea..1fff82d17fa 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -184,6 +184,12 @@ void goto_symext::symex_allocate( else throw "failed to zero initialize dynamic object"; } + else + { + exprt nondet = build_symex_nondet(object_type); + code_assignt assignment(value_symbol.symbol_expr(), nondet); + symex_assign(state, assignment); + } exprt rhs; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index e25add14741..90bb233e99b 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -425,10 +425,22 @@ void goto_symext::phi_function( exprt rhs; + // Don't add a conditional to the assignment when: + // 1. Either guard is false, so we can't follow that branch. + // 2. Either identifier is of generation zero, and so hasn't been + // initialized and therefor an invalid target. if(dest_state.guard.is_false()) rhs=goto_state_rhs; else if(goto_state.guard.is_false()) rhs=dest_state_rhs; + else if(goto_state.level2_current_count(l1_identifier) == 0) + { + rhs = dest_state_rhs; + } + else if(dest_state.level2.current_count(l1_identifier) == 0) + { + rhs = goto_state_rhs; + } else { rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs); From 6faf3762349920e3ee031b59a8cd8076186d3546 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Wed, 9 May 2018 11:35:10 +0100 Subject: [PATCH 2/2] Enable 'm' flag on regex for multi-line tests This is a change to the multi-line match option to enable traditional regex multi-line matching. The m flag causes ^ and $ to actually match correctly on new line/carriage returns, where before the match was actually on the entire file so ^ was just beginning of file $ was the end. This also fixes a few tests' failure condition where this subtle difference wasn't noticed and '^warning: ignoring' is used. --- regression/test.pl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/test.pl b/regression/test.pl index 92639accd3f..d137e2dbb84 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -174,7 +174,7 @@ ($$$$$$$$$) binmode $fh; my $whole_file = <$fh>; $whole_file =~ s/\r\n/\n/g; - my $is_match = $whole_file =~ /$result/; + my $is_match = $whole_file =~ /$result/m; $r = ($included ? !$is_match : $is_match); } else