Skip to content
Snippets Groups Projects
Commit c5017302 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] test tactic modmask

parent 31cc4550
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 528 additions and 0 deletions
src/plugins/wp/tests/wp_tip/modmask.i 0 → 100644
+ 18
− 0
View file @ c5017302
/* run.config
OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
*/
/* run.config_qualif
DONTRUN:
*/
/*@
check lemma and_modulo_us_255:
\forall unsigned short us ; (us & 0xFF) == us % 0x100 ;
*/
/*@
check lemma and_modulo_u:
\forall unsigned us, integer shift;
0 <= shift < (sizeof(us) * 8) ==> (us & ((1 << shift) - 1)) == us % (1 << shift);
*/
src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle 0 → 100644
+ 79
− 0
View file @ c5017302
# frama-c -wp [...]
[kernel] Parsing modmask.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp:script:allgoals]
Lemma and_modulo_u:
Prove: let x_0 = (lsl 1 shift_0) in
(0<=shift_0) -> (shift_0<=31) -> (is_uint32 us_0)
-> ((us_0 mod x_0)=(land us_0 (x_0-1)))
------------------------------------------------------------
[wp:script:allgoals]
Lemma and_modulo_us_255:
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-0 (generated):
Let x = lsl(1, shift_0).
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: (0 <= us_0) /\ (0 < x) /\ (exists i : Z. (lsl(1, i) = x) /\ (0 <= i)).
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-1 (generated):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_us_255 subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
Assume { Have: is_uint16(us_0). }
Prove: 0 <= us_0.
------------------------------------------------------------
[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
[wp:script:allgoals]
typed_check_lemma_and_modulo_us_255 subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: 0 <= us_0.
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-3 (generated):
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: 0 < lsl(1, shift_0).
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-4 (generated):
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
------------------------------------------------------------
[wp] [Script] Goal typed_check_lemma_and_modulo_u : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
[wp] Updated session with 2 new valid scripts.
src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json 0 → 100644
+ 162
− 0
View file @ c5017302
[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
"params": { "Wp.modmask.revert": false },
"select": { "select": "inside-goal", "occur": 0,
"target": "us_0 mod (lsl 1 shift_0)",
"pattern": "%$uslsl1$shift" },
"children": { "Mask Guard": [ { "header": "Split", "tactic": "Wp.split",
"params": {},
"select": { "select": "clause-goal",
"target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
"pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
"children": { "Goal 1/3": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-step",
"at": 2,
"kind": "have",
"target": "(is_uint32 us_0)",
"pattern": "is_uint32$us" },
"children":
{ "Unfold 'is_uint32'":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 2/3": [ { "header": "Range",
"tactic": "Wp.range",
"params":
{ "inf": 0,
"sup": 31 },
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "shift_0",
"pattern": "$shift" },
"children":
{ "Lower 0":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 0":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 1":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 2":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 3":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 4":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 5":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 6":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 7":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 8":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 9":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 10":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 11":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 12":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 13":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 14":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 15":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 16":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 17":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 18":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 19":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 20":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 21":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 22":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 23":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 24":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 25":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 26":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 27":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 28":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 29":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 30":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 31":
[ { "prover": "qed",
"verdict": "valid" } ],
"Upper 31":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "header": "Instance",
"tactic": "Wp.instance",
"params":
{ "P1":
{ "select": "inside-goal",
"occur": 0,
"target": "shift_0",
"pattern": "$shift" },
"P2": null,
"P3": null,
"P4": null,
"P5": null,
"P6": null,
"P7": null,
"P8": null,
"P9": null,
"P10": null },
"select":
{ "select": "clause-goal",
"target": "exists i_0:int. ((lsl 1 i_0)=(lsl 1 shift_0)) /\\ (0<=i_0)",
"pattern": "\\Elsl011$shift" },
"children":
{ "Witness":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ],
"Mask": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json 0 → 100644
+ 14
− 0
View file @ c5017302
[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
"params": { "Wp.modmask.revert": false },
"select": { "select": "inside-goal", "occur": 0,
"target": "us_0 mod 256", "pattern": "%$us256" },
"children": { "Mask Guard": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "(is_uint16 us_0)",
"pattern": "is_uint16$us" },
"children": { "Unfold 'is_uint16'":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Mask": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle 0 → 100644
+ 79
− 0
View file @ c5017302
# frama-c -wp [...]
[kernel] Parsing modmask.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp:script:allgoals]
Lemma and_modulo_u:
Prove: let x_0 = (lsl 1 shift_0) in
(0<=shift_0) -> (shift_0<=31) -> (is_uint32 us_0)
-> ((us_0 mod x_0)=(land us_0 (x_0-1)))
------------------------------------------------------------
[wp:script:allgoals]
Lemma and_modulo_us_255:
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-0 (generated):
Let x = lsl(1, shift_0).
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: (0 <= us_0) /\ (0 < x) /\ (exists i : Z. (lsl(1, i) = x) /\ (0 <= i)).
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-1 (generated):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_us_255 subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
Assume { Have: is_uint16(us_0). }
Prove: 0 <= us_0.
------------------------------------------------------------
[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
[wp:script:allgoals]
typed_check_lemma_and_modulo_us_255 subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: 0 <= us_0.
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-3 (generated):
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: 0 < lsl(1, shift_0).
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-4 (generated):
Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
------------------------------------------------------------
[wp] [Script] Goal typed_check_lemma_and_modulo_u : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
[wp] Updated session with 2 new valid scripts.
src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json 0 → 100644
+ 162
− 0
View file @ c5017302
[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
"params": { "Wp.modmask.revert": false },
"select": { "select": "inside-goal", "occur": 0,
"target": "(land us_0 ((lsl 1 shift_0)-1))",
"pattern": "land$us+-1lsl1$shift" },
"children": { "Mod Guard": [ { "header": "Split", "tactic": "Wp.split",
"params": {},
"select": { "select": "clause-goal",
"target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
"pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
"children": { "Goal 1/3": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-step",
"at": 2,
"kind": "have",
"target": "(is_uint32 us_0)",
"pattern": "is_uint32$us" },
"children":
{ "Unfold 'is_uint32'":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 2/3": [ { "header": "Range",
"tactic": "Wp.range",
"params":
{ "inf": 0,
"sup": 31 },
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "shift_0",
"pattern": "$shift" },
"children":
{ "Lower 0":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 0":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 1":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 2":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 3":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 4":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 5":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 6":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 7":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 8":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 9":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 10":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 11":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 12":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 13":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 14":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 15":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 16":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 17":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 18":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 19":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 20":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 21":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 22":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 23":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 24":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 25":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 26":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 27":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 28":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 29":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 30":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 31":
[ { "prover": "qed",
"verdict": "valid" } ],
"Upper 31":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "header": "Instance",
"tactic": "Wp.instance",
"params":
{ "P1":
{ "select": "inside-goal",
"occur": 0,
"target": "shift_0",
"pattern": "$shift" },
"P2": null,
"P3": null,
"P4": null,
"P5": null,
"P6": null,
"P7": null,
"P8": null,
"P9": null,
"P10": null },
"select":
{ "select": "clause-goal",
"target": "exists i_0:int. ((lsl 1 i_0)=(lsl 1 shift_0)) /\\ (0<=i_0)",
"pattern": "\\Elsl011$shift" },
"children":
{ "Witness":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ],
"Mod": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json 0 → 100644
+ 14
− 0
View file @ c5017302
[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
"params": { "Wp.modmask.revert": false },
"select": { "select": "inside-goal", "occur": 0,
"target": "(land 255 us_0)", "pattern": "land255$us" },
"children": { "Mod Guard": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "(is_uint16 us_0)",
"pattern": "is_uint16$us" },
"children": { "Unfold 'is_uint16'":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Mod": [ { "prover": "qed", "verdict": "valid" } ] } } ]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment