From 0541738be67c34fee8a9ae44e13691b23f82cbe0 Mon Sep 17 00:00:00 2001 From: dewert99 Date: Fri, 2 Aug 2024 19:58:07 -0700 Subject: [PATCH 1/3] Fix bug in creation of spec axioms --- creusot/src/backend/logic.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs index 472a9b57f0..6ff01fd64e 100644 --- a/creusot/src/backend/logic.rs +++ b/creusot/src/backend/logic.rs @@ -185,9 +185,9 @@ pub(crate) fn lower_logical_defn<'tcx, N: Namer<'tcx>>( ); if has_axioms { - if sig.uses_simple_triggers() { + if sig.uses_simple_triggers() && !sig_contract.contract.variant.is_empty() { let lim_name = Ident::from_string(format!("{}_lim", &*sig.name)); - let mut lim_sig = sig.clone(); + let mut lim_sig = sig_contract; lim_sig.name = lim_name; lim_sig.trigger = Some(Trigger::single(function_call(&lim_sig))); lim_sig.attrs = vec![]; From cf202718f74827bdb47c68c528976ed7a9c2d0b0 Mon Sep 17 00:00:00 2001 From: dewert99 Date: Sat, 3 Aug 2024 09:39:53 -0700 Subject: [PATCH 2/3] Added simple_triggers test --- .../tests/should_succeed/simple_trigger.coma | 52 ++++++++++++++++++ .../tests/should_succeed/simple_trigger.rs | 19 +++++++ .../simple_trigger/why3session.xml | 19 +++++++ .../simple_trigger/why3shapes.gz | Bin 0 -> 220 bytes 4 files changed, 90 insertions(+) create mode 100644 creusot/tests/should_succeed/simple_trigger.coma create mode 100644 creusot/tests/should_succeed/simple_trigger.rs create mode 100644 creusot/tests/should_succeed/simple_trigger/why3session.xml create mode 100644 creusot/tests/should_succeed/simple_trigger/why3shapes.gz diff --git a/creusot/tests/should_succeed/simple_trigger.coma b/creusot/tests/should_succeed/simple_trigger.coma new file mode 100644 index 0000000000..a4438753d5 --- /dev/null +++ b/creusot/tests/should_succeed/simple_trigger.coma @@ -0,0 +1,52 @@ + +module SimpleTrigger_Id_Impl + let%span ssimple_trigger0 = "../simple_trigger.rs" 7 11 7 17 + + let%span ssimple_trigger1 = "../simple_trigger.rs" 9 0 9 34 + + let%span ssimple_trigger2 = "../simple_trigger.rs" 8 10 8 11 + + use prelude.prelude.Int + + constant i : int + + function id [#"../simple_trigger.rs" 10 0 10 20] (i : int) : int + + goal vc_id : ([%#ssimple_trigger0] i >= 0) + -> (if i = 0 then + [%#ssimple_trigger1] i = 0 -> 0 = 0 + else + (([%#ssimple_trigger0] i - 1 >= 0) + /\ 0 <= ([%#ssimple_trigger2] i) /\ ([%#ssimple_trigger2] i - 1) < ([%#ssimple_trigger2] i)) + /\ (([%#ssimple_trigger1] i - 1 = 0 -> id (i - 1) = 0) -> ([%#ssimple_trigger1] i = 0 -> id (i - 1) + 1 = 0)) + ) +end +module SimpleTrigger_Test + let%span ssimple_trigger0 = "../simple_trigger.rs" 14 10 14 20 + + let%span span1 = "../simple_trigger.rs" 7 11 7 17 + + let%span span2 = "../simple_trigger.rs" 9 0 9 34 + + let%span span3 = "../simple_trigger.rs" 8 10 8 11 + + let%span span4 = "../simple_trigger.rs" 6 0 6 8 + + use prelude.prelude.Int + + function id'0 [#"../simple_trigger.rs" 10 0 10 20] (i : int) : int + + function id'0_lim (i : int) : int + + axiom id'0_def : forall i : int [id'0 i] . id'0 i = ([%#span4] if i = 0 then 0 else id'0_lim (i - 1) + 1) + + axiom id'0_def_lim : forall i : int [id'0 i] . id'0 i = id'0_lim i + + axiom id'0_lim_spec : forall i : int [id'0_lim i] . ([%#span1] i >= 0) -> ([%#span2] i = 0 -> id'0_lim i = 0) + + use prelude.prelude.Intrinsic + + let rec test (_1:()) (return' (ret:()))= (! bb0 [ bb0 = return' {_0} ] ) [ & _0 : () = any_l () ] + [ return' (result:())-> {[@expl:postcondition] [%#ssimple_trigger0] id'0 1 = 1} (! return' {result}) ] + +end diff --git a/creusot/tests/should_succeed/simple_trigger.rs b/creusot/tests/should_succeed/simple_trigger.rs new file mode 100644 index 0000000000..f824da3f9a --- /dev/null +++ b/creusot/tests/should_succeed/simple_trigger.rs @@ -0,0 +1,19 @@ +// CREUSOT_ARG=--simple-triggers=true +extern crate creusot_contracts; + +use creusot_contracts::*; + +#[logic] +#[requires(i >= 0)] +#[variant(i)] +#[ensures(i == 0 ==> result == 0)] +fn id(i: Int) -> Int { + if i == 0 { + 0 + } else { + id(i - 1) + 1 + } +} + +#[ensures(id(1) == 1)] +pub fn test() {} diff --git a/creusot/tests/should_succeed/simple_trigger/why3session.xml b/creusot/tests/should_succeed/simple_trigger/why3session.xml new file mode 100644 index 0000000000..d0bc0f0a71 --- /dev/null +++ b/creusot/tests/should_succeed/simple_trigger/why3session.xml @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/simple_trigger/why3shapes.gz b/creusot/tests/should_succeed/simple_trigger/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..4dc7e3de714e98b5e2c4b54f5a87cae8eb9acf3b GIT binary patch literal 220 zcmV<203-h&iwFP!00000|4mNI3c@fDyyq)&Q!9ntv`HJW1uv!kK(Df+Tdj3Yz9?? z?Geg=)t@;>hYiMB%+5k38nn(eqCJ~jq5>^slIC4!IM%>~>2hTOrI3iAbW4Ov8-+G& WsWXWW$vUl*TCgA3JQ=EF0RRBRA7`il literal 0 HcmV?d00001 From 014875dcee1b52037992129eef4893913971f39c Mon Sep 17 00:00:00 2001 From: dewert99 Date: Sat, 3 Aug 2024 10:20:39 -0700 Subject: [PATCH 3/3] Added simple_triggers test --- creusot/tests/should_succeed/simple_trigger.coma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/creusot/tests/should_succeed/simple_trigger.coma b/creusot/tests/should_succeed/simple_trigger.coma index a4438753d5..62bb408c46 100644 --- a/creusot/tests/should_succeed/simple_trigger.coma +++ b/creusot/tests/should_succeed/simple_trigger.coma @@ -22,7 +22,7 @@ module SimpleTrigger_Id_Impl ) end module SimpleTrigger_Test - let%span ssimple_trigger0 = "../simple_trigger.rs" 14 10 14 20 + let%span ssimple_trigger0 = "../simple_trigger.rs" 18 10 18 20 let%span span1 = "../simple_trigger.rs" 7 11 7 17