From 853e47078c603b53bdb2bd85afb19f4d7090c395 Mon Sep 17 00:00:00 2001 From: Lorenzo Manacorda Date: Mon, 17 Feb 2020 16:33:56 +0100 Subject: [PATCH 1/2] klab-prove: toggle deterministic functions This fixes the non-determinism we were seeing in some proofs. The reason was that there was more than one function defined for `sizeWordStack`, one of which is problematic, and they were being chosen non-deterministically. --- libexec/klab-prove | 1 + 1 file changed, 1 insertion(+) diff --git a/libexec/klab-prove b/libexec/klab-prove index ea8573f8..5984bdc1 100755 --- a/libexec/klab-prove +++ b/libexec/klab-prove @@ -132,6 +132,7 @@ timeout "$TIMEOUT" "$KLAB_EVMS_PATH/deps/k/k-distribution/target/release/k/bin/k --smt_prelude "$KLAB_OUT/prelude.smt2" \ --concrete-rules "$(join_by , ${concrete_rules[@]})" \ --z3-tactic "(or-else (using-params smt :random-seed 3) (using-params smt :random-seed 2) (using-params smt :random-seed 1))" \ + --deterministic-functions \ "$target_spec" >"$STDOUT" 2>"$STDERR" & kprove_child=$! wait "$kprove_child" result=$? From bf46cead78a991d1936c5fe1bd21246a3917f8bc Mon Sep 17 00:00:00 2001 From: Lorenzo Manacorda Date: Tue, 3 Mar 2020 15:53:27 +0100 Subject: [PATCH 2/2] rules.k: remove nested #ifte simplification It clashes with this rule in domains.k: ```k rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C ``` --- resources/rules.k.tmpl | 4 ---- 1 file changed, 4 deletions(-) diff --git a/resources/rules.k.tmpl b/resources/rules.k.tmpl index b9ccb9f6..c3e4998b 100644 --- a/resources/rules.k.tmpl +++ b/resources/rules.k.tmpl @@ -315,10 +315,6 @@ rule ACCTCODE in SetItem( 1 ) rule #if C #then (#if C #then B1 #else B2 #fi) -Int D #else (#if C #then B3 #else B4 #fi) -Int E #fi => #if C #then B1 -Int D #else B4 -Int E #fi - // avoid nested #ifte - rule #if C1 #then A #else (B +Int #if C2 #then B2 #else B3 #fi) #fi => - #if C1 #then A #else B #fi +Int #if (C2 andBool notBool C1) #then B2 #else 0 #fi +Int #if ((notBool C2) andBool (notBool C1)) #then B3 #else 0 #fi - //simplify trivial #ifs rule #if C1 #then A #else B #fi => A requires A ==K B