From 5baedb28cac9be32eaac51038740d0f6b9a8c766 Mon Sep 17 00:00:00 2001 From: Owen Date: Thu, 21 Mar 2019 21:50:53 +0000 Subject: [PATCH] Update tests for symex excluding null pointers Value-set filtering means some of the tests pass that didn't before. Also add tests that only pass because of local safe pointer analysis, not value-set filtering, so we can tell if that stops working in future. --- .../symex_should_exclude_null_pointers/main.c | 73 +++++++++++++------ .../test.desc | 13 ++-- 2 files changed, 58 insertions(+), 28 deletions(-) diff --git a/regression/cbmc/symex_should_exclude_null_pointers/main.c b/regression/cbmc/symex_should_exclude_null_pointers/main.c index 4ee8d91e3b..3ccab5c958 100644 --- a/regression/cbmc/symex_should_exclude_null_pointers/main.c +++ b/regression/cbmc/symex_should_exclude_null_pointers/main.c @@ -1,3 +1,5 @@ +#include + static void noop() { } int main(int argc, char **argv) { @@ -5,12 +7,16 @@ int main(int argc, char **argv) { int x; int *maybe_null = argc & 1 ? &x : 0; - // Should work (guarded by assume): + // There are two features of symex that might exclude null pointers: local + // safe pointer analysis (LSPA for the rest of this file) and value-set + // filtering (i.e. goto_symext::try_filter_value_sets()). + + // Should be judged safe by LSPA and value-set filtering (guarded by assume): int *ptr1 = maybe_null; __CPROVER_assume(ptr1 != 0); int deref1 = *ptr1; - // Should work (guarded by else): + // Should be judged safe by LSPA and value-set filtering (guarded by else): int *ptr2 = maybe_null; if(ptr2 == 0) { @@ -20,14 +26,15 @@ int main(int argc, char **argv) { int deref2 = *ptr2; } - // Should work (guarded by if): + // Should be judged safe by LSPA and value-set filtering (guarded by if): int *ptr3 = maybe_null; if(ptr3 != 0) { int deref3 = *ptr3; } - // Shouldn't work yet despite being safe (guarded by backward goto): + // Should be judged unsafe by LSPA and safe by value-set filtering + // (guarded by backward goto): int *ptr4 = maybe_null; goto check; @@ -41,7 +48,8 @@ check: end_test4: - // Shouldn't work yet despite being safe (guarded by confluence): + // Should be judged unsafe by LSPA and safe by value-set filtering + // (guarded by confluence): int *ptr5 = maybe_null; if(argc == 5) __CPROVER_assume(ptr5 != 0); @@ -49,26 +57,49 @@ end_test4: __CPROVER_assume(ptr5 != 0); int deref5 = *ptr5; - // Shouldn't work (unsafe as only guarded on one branch): + // Should be judged unsafe by LSPA (due to suspicion write to ptr5 might alter + // ptr6) and safe by value-set filtering: int *ptr6 = maybe_null; - if(argc == 6) - __CPROVER_assume(ptr6 != 0); + __CPROVER_assume(ptr6 != 0); + ptr5 = 0; + int deref6 = *ptr6; + + // Should be judged unsafe by LSPA (due to suspicion noop() call might alter + // ptr7) and safe by value-set filtering: + int *ptr7 = maybe_null; + __CPROVER_assume(ptr7 != 0); + noop(); + int deref7 = *ptr7; + + // Should be judged safe by LSPA and unsafe by value-set filtering (it + // isn't known what symbol *ptr_ptr8 refers to, so null can't be removed + // from a specific value set): + int r8_a = 1, r8_b = 2; + int *q8_a = argc & 2 ? &r8_a : 0; + int *q8_b = argc & 4 ? &r8_b : 0; + int **ptr8 = argc & 8 ? &q8_a : &q8_b; + __CPROVER_assume(*ptr8 != 0); + int deref8 = **ptr8; + + // Should be judged safe by LSPA and unsafe by value-set filtering (it + // isn't known what symbol *ptr_ptr9 refers to, so null can't be removed + // from a specific value set): + int r9_a = 1, r9_b = 2; + int *q9_a = argc & 2 ? &r9_a : 0; + int *q9_b = argc & 4 ? &r9_b : 0; + int **ptr9 = argc & 8 ? &q9_a : &q9_b; + if(*ptr9 != 0) + int deref9 = **ptr9; + + // Should be judged unsafe by LSPA and value-set filtering + // (unsafe as only guarded on one branch): + int *ptr10 = maybe_null; + if(argc == 10) + __CPROVER_assume(ptr10 != 0); else { } - int deref6 = *ptr6; - - // Shouldn't work due to suspicion write to ptr6 might alter ptr7: - int *ptr7 = maybe_null; - __CPROVER_assume(ptr7 != 0); - ptr6 = 0; - int deref7 = *ptr7; - - // Shouldn't work due to suspicion noop() call might alter ptr8: - int *ptr8 = maybe_null; - __CPROVER_assume(ptr8 != 0); - noop(); - int deref8 = *ptr8; + int deref10 = *ptr10; assert(0); } diff --git a/regression/cbmc/symex_should_exclude_null_pointers/test.desc b/regression/cbmc/symex_should_exclude_null_pointers/test.desc index e5075fa576..493843ebfb 100644 --- a/regression/cbmc/symex_should_exclude_null_pointers/test.desc +++ b/regression/cbmc/symex_should_exclude_null_pointers/test.desc @@ -3,15 +3,14 @@ main.c --show-vcc ^EXIT=0$ ^SIGNAL=0$ -ptr4\$object -ptr5\$object -ptr6\$object -ptr7\$object -ptr8\$object +ptr10\$object -- -ptr[1-3]\$object +ptr[1-9]\$object ^warning: ignoring -- ptrX\$object appearing in the VCCs indicates symex was unsure whether the pointer had a valid target, and uses the $object symbol as a referred object of last resort. ptr1-3 should be judged -not-null by symex, so their $object symbols do not occur. +not-null by local safe pointer analysis, so their $object symbols do not occur. ptr4-7 are +not caught by local safe pointer analysis but they are judged safe by value-set filtering, i.e. +goto_symext::try_filter_value_sets(). ptr8-9 are judged safe by local safe pointer analysis but +not value-set filtering. ptr10 is not judged safe by either because it is not safe.