Skip to content
GitLab
Commit bde133d5 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added uint_eq ghost function; use to prove that integer representations can be... 

added uint_eq ghost function; use to prove that integer representations can be used to prove byte-for-byte equalities (if necessary at some point)
parent 1430466e
Hide whitespace changes
Inline Side-by-side
avrmodel.mlw
View file @ bde133d5
......@@ -581,6 +581,21 @@ let rec ghost uint_bound (reg: address_space) (lo w: int): unit
assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
end
let rec ghost uint_eq (w: int) (m1 m2: address_space) (ofs: int)
requires { w >= 0 }
requires { B.sum (m1,ofs) 0 w = B.sum (m2,ofs) 0 w }
ensures { eq w m1 m2 ofs }
variant { w }
= if w > 0 then begin
uint_recursion m1 ofs w;
assert { B.sum (m1,ofs) 0 w = m1[ofs] + 256*B.sum (m1,ofs+1) 0 (w-1) };
uint_recursion m2 ofs w;
assert { B.sum (m1,ofs) 0 w = m2[ofs] + 256*B.sum (m2,ofs+1) 0 (w-1) };
assert { m1[ofs] = mod (B.sum (m1,ofs) 0 w) 256 = mod (B.sum (m2,ofs) 0 w) 256 = m2[ofs] };
uint_eq (w-1) m1 m2 (ofs+1);
assert { eq (w-1) m1 m2 (ofs+1) };
end
end
module Shadow
......
avrmodel/why3session.xml
View file @ bde133d5
......@@ -6,9 +6,9 @@
<prover id="2" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="0" memlimit="1000"/>
<file name="../avrmodel.mlw">
<theory name="AVRint" sum="b263d2793d6b4d719244c500d148f089">
<theory name="AVRint" sum="514a40cb0665f64f0dce0e88744d4d50">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
......@@ -195,14 +195,14 @@
<goal name="WP_parameter adiw.3" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter adiw.3.1" expl="postcondition">
<proof prover="5"><result status="valid" time="0.22"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter adiw.4" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter adiw.4.1" expl="postcondition">
<proof prover="5"><result status="valid" time="0.23"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
......@@ -217,19 +217,19 @@
<proof prover="4" steplimit="0"><result status="valid" time="0.06" steps="71"/></proof>
</goal>
<goal name="WP_parameter sbiw.3" expl="postcondition">
<proof prover="5"><result status="valid" time="0.15"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter sbiw.4" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter sbiw.4.1" expl="postcondition">
<proof prover="5"><result status="valid" time="0.26"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sbiw.5" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter sbiw.5.1" expl="postcondition">
<proof prover="5"><result status="valid" time="0.26"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
......@@ -297,13 +297,13 @@
<proof prover="0"><result status="valid" time="1.56"/></proof>
</goal>
<goal name="bitset_correct2" expl="">
<proof prover="5"><result status="valid" time="0.30"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="bitset_equiv_def" expl="">
<proof prover="0"><result status="valid" time="1.42"/></proof>
</goal>
<goal name="bitsetx_equiv_def" expl="">
<proof prover="5"><result status="valid" time="0.22"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter bld" expl="VC for bld">
<proof prover="4"><result status="valid" time="0.87" steps="786"/></proof>
......@@ -324,7 +324,7 @@
<proof prover="4" steplimit="-1"><result status="valid" time="0.14" steps="73"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.4" expl="postcondition">
<proof prover="5"><result status="valid" time="2.66"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="2.66"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.5" expl="postcondition">
<proof prover="0"><result status="valid" time="0.30"/></proof>
......@@ -337,7 +337,7 @@
<proof prover="4" steplimit="-1"><result status="valid" time="0.10" steps="73"/></proof>
</goal>
<goal name="WP_parameter uint_bound.2" expl="assertion">
<proof prover="5"><result status="valid" time="2.40"/></proof>
<proof prover="5" steplimit="1"><result status="valid" time="2.40"/></proof>
</goal>
<goal name="WP_parameter uint_bound.3" expl="variant decrease">
<proof prover="4" steplimit="-1"><result status="valid" time="0.06" steps="75"/></proof>
......@@ -349,13 +349,60 @@
<proof prover="4" steplimit="0"><result status="valid" time="0.08" steps="82"/></proof>
</goal>
<goal name="WP_parameter uint_bound.6" expl="postcondition">
<proof prover="5" steplimit="0"><result status="valid" time="0.34"/></proof>
<proof prover="5"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter uint_bound.7" expl="postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="0.21"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter uint_eq" expl="VC for uint_eq">
<transf name="split_goal_wp">
<goal name="WP_parameter uint_eq.1" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter uint_eq.2" expl="assertion">
<proof prover="5" memlimit="2000"><result status="valid" time="4.02"/></proof>
</goal>
<goal name="WP_parameter uint_eq.3" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter uint_eq.4" expl="assertion">
<proof prover="5" memlimit="2000"><result status="valid" time="4.38"/></proof>
</goal>
<goal name="WP_parameter uint_eq.5" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter uint_eq.5.1" expl="VC for uint_eq">
<proof prover="0" timelimit="30" steplimit="0" memlimit="2000"><result status="valid" time="12.87"/></proof>
</goal>
<goal name="WP_parameter uint_eq.5.2" expl="VC for uint_eq">
<proof prover="5" memlimit="2000"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter uint_eq.5.3" expl="VC for uint_eq">
<proof prover="0" steplimit="0" memlimit="2000"><result status="valid" time="11.25"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter uint_eq.6" expl="variant decrease">
<proof prover="5" memlimit="2000"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter uint_eq.7" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter uint_eq.8" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter uint_eq.9" expl="assertion">
<proof prover="5" memlimit="2000"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter uint_eq.10" expl="postcondition">
<proof prover="5" memlimit="2000"><result status="valid" time="5.44"/></proof>
</goal>
<goal name="WP_parameter uint_eq.11" expl="postcondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Shadow" sum="b68cde8d7dc402517d59c758cb43fec2">
<goal name="WP_parameter modify_r0" expl="VC for modify_r0">
......
avrmodel/why3shapes.gz
View file @ bde133d5
No preview for this file type
Supports Markdown
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