From d64e80d488da71480ed70ae9069b0f0315e3343d Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Sun, 19 Jan 2025 09:27:54 +0100 Subject: [PATCH] ensure some cheats are not used --- src/tools/symbexec/aux_setLib.sml | 1 + src/tools/symbexec/birs_utilsLib.sml | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/tools/symbexec/aux_setLib.sml b/src/tools/symbexec/aux_setLib.sml index 9eb6d4c6a..dbb5cfda7 100644 --- a/src/tools/symbexec/aux_setLib.sml +++ b/src/tools/symbexec/aux_setLib.sml @@ -360,6 +360,7 @@ in (* local *) print "the symbolic environments seem to be unequal, but they might be equal\n"; raise ERR "birs_env_EQ_CONV" "the symbolic environments seem to be unequal, but they might be equal"); val eq_thm = mk_oracle_thm "BIRS_ENV_EQ" ([], mk_eq (tm, if is_eq then T else F)); + val _ = print "oracle used: BIRS_ENV_EQ\n"; in eq_thm end; diff --git a/src/tools/symbexec/birs_utilsLib.sml b/src/tools/symbexec/birs_utilsLib.sml index b3e780da7..203432dbe 100644 --- a/src/tools/symbexec/birs_utilsLib.sml +++ b/src/tools/symbexec/birs_utilsLib.sml @@ -261,7 +261,7 @@ in (* local *) end (* ---------------------------------------------------------------------------------------- *) - + (* val birs_exp_imp_DROP_R_thm = prove(`` !be1 be2. birs_exp_imp (BExp_BinExp BIExp_And be1 be2) be1 @@ -299,6 +299,7 @@ in (* local *) else NONE end; + *) (* general path condition weakening with z3 (to throw away path condition conjuncts (to remove branch path condition conjuncts)) *) fun birs_Pi_first_pcond_RULE pcond_new thm = @@ -319,10 +320,12 @@ in (* local *) val _ = holba_z3Lib.debug_print := true; val _ = print "sending a z3 query\n"; *) + (* val pcond_drop_ok = isSome (is_DROP_R_imp imp_tm) orelse isSome (is_DROP_L_imp imp_tm) orelse isSome (is_conjunct_inclusion_imp imp_tm); - val pcond_imp_ok = pcond_drop_ok orelse (* TODO: something might be wrong in expression simplification before smtlib-z3 exporter *) + *) + val pcond_imp_ok = (*pcond_drop_ok orelse (* TODO: something might be wrong in expression simplification before smtlib-z3 exporter *)*) isSome (check_imp_tm imp_tm); val _ = if pcond_imp_ok then () else (print "widening failed, path condition is not weaker\n";