From 18e8b81b8eb4c4e313b03f4616271a0ea8e65e9b Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 4 Feb 2021 11:59:56 -0300 Subject: [PATCH] [proof-new] Catch trivial cycles in SAT proof generation (#5853) Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which we generate a trivial cycle during SAT proof generation, which can lead to problematic cycles when expanding MACRO_RESOLUTION steps. For example, we can go from l1 v l2 ~l1 v l3 ~l2 v l3 (ok) ------------------------------ l3 in which l3 = l1 v l2, to l1 v l2 ~l1 v l3 ~l2 v l3 (bad) ------------------------------ l3 v l3 --------- l3 This commit now catches the trivial cycle before it's generated. --- src/prop/sat_proof_manager.cpp | 11 + test/regress/CMakeLists.txt | 1 + .../regress1/proofs/sat-trivial-cycle.smt2 | 189 ++++++++++++++++++ 3 files changed, 201 insertions(+) create mode 100644 test/regress/regress1/proofs/sat-trivial-cycle.smt2 diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index aae11ae51..dd7e94f03 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -228,6 +228,17 @@ void SatProofManager::endResChain(Node conclusion, << children[0] << "\n"; return; } + // whether trivial cycle + for (const Node& child : children) + { + if (conclusion == child) + { + Trace("sat-proof") + << "SatProofManager::endResChain: no-op. The conclusion " + << conclusion << " is equal to a premise\n"; + return; + } + } if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion)) { Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of " diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5e0fa2495..e158f629a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1633,6 +1633,7 @@ set(regress_1_tests regress1/proof00.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 + regress1/proofs/sat-trivial-cycle.smt2 regress1/push-pop/arith_lra_01.smt2 regress1/push-pop/arith_lra_02.smt2 regress1/push-pop/bug-fmf-fun-skolem.smt2 diff --git a/test/regress/regress1/proofs/sat-trivial-cycle.smt2 b/test/regress/regress1/proofs/sat-trivial-cycle.smt2 new file mode 100644 index 000000000..e8d163c2a --- /dev/null +++ b/test/regress/regress1/proofs/sat-trivial-cycle.smt2 @@ -0,0 +1,189 @@ +; EXPECT: unsat +;; minimized from UFLIA/tokeneer/enclave/progressadminactivity-3.smt2 +(set-info :smt-lib-version 2.6) +(set-logic UFLIA) +(set-info :source | + Tokeneer case study + |) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun field.statetype.status () Int) +(declare-fun admin__archivelog () Int) +(declare-fun admin__nullop () Int) +(declare-fun admin__opandnullt__base__first () Int) +(declare-fun admin__opandnullt__base__last () Int) +(declare-fun admin__opandnullt__first () Int) +(declare-fun admin__opandnullt__last () Int) +(declare-fun admin__opandnullt__size () Int) +(declare-fun admin__overridelock () Int) +(declare-fun admin__shutdownop () Int) +(declare-fun admin__updateconfigdata () Int) +(declare-fun alarmtypes__alarming () Int) +(declare-fun alarmtypes__silent () Int) +(declare-fun alarmtypes__statust__base__first () Int) +(declare-fun alarmtypes__statust__base__last () Int) +(declare-fun alarmtypes__statust__first () Int) +(declare-fun alarmtypes__statust__last () Int) +(declare-fun alarmtypes__statust__size () Int) +(declare-fun door__closed () Int) +(declare-fun door__open () Int) +(declare-fun door__t__base__first () Int) +(declare-fun door__t__base__last () Int) +(declare-fun door__t__first () Int) +(declare-fun door__t__last () Int) +(declare-fun door__t__size () Int) +(declare-fun enclavequiescent () Int) +(declare-fun gotadmintoken () Int) +(declare-fun nonquiescentstates__base__first () Int) +(declare-fun nonquiescentstates__base__last () Int) +(declare-fun nonquiescentstates__first () Int) +(declare-fun nonquiescentstates__last () Int) +(declare-fun nonquiescentstates__size () Int) +(declare-fun notenrolled () Int) +(declare-fun privtypes__auditmanager () Int) +(declare-fun privtypes__guard () Int) +(declare-fun privtypes__privileget__base__first () Int) +(declare-fun privtypes__privileget__base__last () Int) +(declare-fun privtypes__privileget__first () Int) +(declare-fun privtypes__privileget__last () Int) +(declare-fun privtypes__privileget__size () Int) +(declare-fun privtypes__securityofficer () Int) +(declare-fun privtypes__useronly () Int) +(declare-fun shutdown () Int) +(declare-fun statust__base__first () Int) +(declare-fun statust__base__last () Int) +(declare-fun statust__first () Int) +(declare-fun statust__last () Int) +(declare-fun statust__size () Int) +(declare-fun waitingendenrol () Int) +(declare-fun waitingenrol () Int) +(declare-fun waitingfinishadminop () Int) +(declare-fun waitingremoveadmintokenfail () Int) +(declare-fun waitingstartadminop () Int) +(declare-fun admintoken__state () Int) +(declare-fun admintoken__state__1 () Int) +(declare-fun init.admintoken__state__1 () Int) +(declare-fun admintoken__state__2 () Int) +(declare-fun init.admintoken__state__2 () Int) +(declare-fun admintoken__state__3 () Int) +(declare-fun init.admintoken__state__3 () Int) +(declare-fun init.admintoken__state () Int) +(declare-fun clock__currenttime () Int) +(declare-fun init.clock__currenttime () Int) +(declare-fun door__state () Int) +(declare-fun door__state__3 () Int) +(declare-fun init.door__state__3 () Int) +(declare-fun init.door__state () Int) +(declare-fun latch__state () Int) +(declare-fun latch__state__3 () Int) +(declare-fun init.latch__state__3 () Int) +(declare-fun init.latch__state () Int) +(declare-fun state () Int) +(declare-fun init.state () Int) +(declare-fun |status'| () Int) +(declare-fun status__1 () Int) +(declare-fun init.status__1 () Int) +(declare-fun status__2 () Int) +(declare-fun init.status__2 () Int) +(declare-fun status__3 () Int) +(declare-fun init.status__3 () Int) +(declare-fun init.status () Int) +(declare-fun theadmin () Int) +(declare-fun theadmin__1 () Int) +(declare-fun init.theadmin__1 () Int) +(declare-fun theadmin__3 () Int) +(declare-fun init.theadmin__3 () Int) +(declare-fun init.theadmin () Int) +(declare-fun admin__opandnullt__pos (Int) Int) +(declare-fun admin__opandnullt__pred (Int) Int) +(declare-fun admin__opandnullt__succ (Int) Int) +(declare-fun admin__opandnullt__val (Int) Int) +(declare-fun admin__prf_rolepresent (Int) Int) +(declare-fun admin__thecurrentop (Int) Int) +(declare-fun admintoken__theauthcertrole (Int) Int) +(declare-fun alarmtypes__statust__pos (Int) Int) +(declare-fun alarmtypes__statust__pred (Int) Int) +(declare-fun alarmtypes__statust__succ (Int) Int) +(declare-fun alarmtypes__statust__val (Int) Int) +(declare-fun bit__and (Int Int) Int) +(declare-fun bit__not (Int Int) Int) +(declare-fun bit__or (Int Int) Int) +(declare-fun bit__xor (Int Int) Int) +(declare-fun character__pos (Int) Int) +(declare-fun character__val (Int) Int) +(declare-fun clock__thecurrenttime (Int) Int) +(declare-fun door__prf_alarmtimeout (Int) Int) +(declare-fun door__t__pos (Int) Int) +(declare-fun door__t__pred (Int) Int) +(declare-fun door__t__succ (Int) Int) +(declare-fun door__t__val (Int) Int) +(declare-fun door__thecurrentdoor (Int) Int) +(declare-fun door__thedooralarm (Int) Int) +(declare-fun integer__pred (Int) Int) +(declare-fun integer__succ (Int) Int) +(declare-fun privtypes__privileget__pos (Int) Int) +(declare-fun privtypes__privileget__pred (Int) Int) +(declare-fun privtypes__privileget__succ (Int) Int) +(declare-fun privtypes__privileget__val (Int) Int) +(declare-fun round__ (Int) Int) +(declare-fun statust__pos (Int) Int) +(declare-fun statust__pred (Int) Int) +(declare-fun statust__succ (Int) Int) +(declare-fun statust__val (Int) Int) +(declare-fun i.div (Int Int) Int) +(declare-fun i.mod (Int Int) Int) +(declare-fun i.mult (Int Int) Int) +(declare-fun i.exp (Int Int) Int) +(declare-fun tm.true () Int) +(declare-fun tm.false () Int) +(declare-fun tm.not (Int) Int) +(declare-fun tm.and (Int Int) Int) +(declare-fun tm.or (Int Int) Int) +(declare-fun tm.iff (Int Int) Int) +(declare-fun tm.eq (Int Int) Int) +(declare-fun tm.ne (Int Int) Int) +(declare-fun tm.lt (Int Int) Int) +(declare-fun tm.le (Int Int) Int) +(declare-fun tuple.2 (Int Int) Int) +(declare-fun a.store (Int Int Int) Int) +(declare-fun a.select (Int Int) Int) +(declare-fun a.mk_const_array (Int) Int) +(declare-fun a.default_array () Int) +(declare-fun r.default_record () Int) +(declare-fun admin__isdoingop (Int) Bool) +(declare-fun admin__ispresent (Int) Bool) +(declare-fun admin__opandnullt__LE (Int Int) Bool) +(declare-fun admin__opandnullt__LT (Int Int) Bool) +(declare-fun admintoken__prf_authcertvalid (Int) Bool) +(declare-fun admintoken__prf_isgood (Int) Bool) +(declare-fun alarmtypes__statust__LE (Int Int) Bool) +(declare-fun alarmtypes__statust__LT (Int Int) Bool) +(declare-fun clock__greaterthanorequal (Int Int) Bool) +(declare-fun currentadminactivitypossible (Int Int) Bool) +(declare-fun door__t__LE (Int Int) Bool) +(declare-fun door__t__LT (Int Int) Bool) +(declare-fun enclave__currentadminactivitypossible (Int Int) Bool) +(declare-fun enclave__enrolmentisinprogress (Int) Bool) +(declare-fun enrolmentisinprogress (Int) Bool) +(declare-fun latch__islocked (Int) Bool) +(declare-fun prf_statusisenclavequiescent (Int) Bool) +(declare-fun prf_statusisgotadmintoken (Int) Bool) +(declare-fun prf_statusisshutdown (Int) Bool) +(declare-fun prf_statusiswaitingfinishadminop (Int) Bool) +(declare-fun prf_statusiswaitingremoveadmintokenfail (Int) Bool) +(declare-fun prf_statusiswaitingstartadminop (Int) Bool) +(declare-fun privtypes__privileget__LE (Int Int) Bool) +(declare-fun privtypes__privileget__LT (Int Int) Bool) +(declare-fun statust__LE (Int Int) Bool) +(declare-fun statust__LT (Int Int) Bool) +(assert (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming))) +(assert (=> (not (admin__ispresent theadmin)) (not (admin__isdoingop theadmin)))) +(assert (=> (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)) (and (admin__ispresent theadmin) (admin__isdoingop theadmin)))) +(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__shutdownop)) (= |status'| waitingstartadminop))) +(assert (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard))))) +(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__overridelock)) (= (admin__prf_rolepresent theadmin) privtypes__guard))) +(assert (let ((?v_0 (admin__isdoingop theadmin))) (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (or (and ?v_0 (= (admin__thecurrentop theadmin) admin__overridelock)) (not ?v_0))))) +(assert (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop))) +(assert (let ((?v_1 (admin__isdoingop theadmin)) (?v_0 (= |status'| waitingstartadminop)) (?v_2 (admin__thecurrentop theadmin)) (?v_3 (= (admin__prf_rolepresent theadmin) privtypes__guard))) (let ((?v_4 (and ?v_1 (= ?v_2 admin__overridelock)))) (not (and (or ?v_0 (= |status'| waitingfinishadminop)) (=> (and ?v_1 (= ?v_2 admin__shutdownop)) ?v_0) (admin__ispresent theadmin) ?v_1 (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)) (=> ?v_3 (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))) (=> ?v_4 ?v_3) (=> ?v_3 (or ?v_4 (not ?v_1)))))))) +(check-sat) +(exit) -- 2.30.2