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

slight optimization

parent f370892c
Hide whitespace changes
Inline Side-by-side
avrmodel.mlw
View file @ 0ed6b403
......@@ -99,13 +99,7 @@ let add (dst src: register): unit
let r2 = (Map.get reg.data src) in
reg.data <- Map.set reg.data dst (mod sum 256);
let res = (Map.get reg.data dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- True
else
cf.value <- False
cf.value <- (r1 >= 128 && r2 >= 128 || r1 >= 128 && res < 128 || r2 >= 128 && res < 128)
let adc (dst src: register): unit
writes { cf }
......@@ -321,11 +315,7 @@ let add_ (dst src: register): unit
let rr = BV8.of_int (Map.get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- Map.set reg.data dst (BV8.to_uint rd');
if BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7
then
cf.value <- True
else
cf.value <- False
cf.value <- (BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7)
let inc_ (dst: register): unit
writes { reg }
......@@ -585,14 +575,7 @@ let add (dst src: register): unit
let r2 = (Map.get reg.data src) in
reg.data <- Map.set reg.data dst (mod sum 256);
let res = (Map.get reg.data dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- True
else
cf.value <- False
cf.value <- (r1 >= 128 && r2 >= 128 || r1 >= 128 && res < 128 || r2 >= 128 && res < 128)
let adc (dst src: register): unit
writes { cf }
......@@ -851,11 +834,7 @@ let add_ (dst src: register): unit
let rr = BV8.of_int (Map.get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- Map.set reg.data dst (BV8.to_uint rd');
if BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7
then
cf.value <- True
else
cf.value <- False
cf.value <- (BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7)
let add__ (dst src: register): unit
writes { reg, cf }
......@@ -871,7 +850,6 @@ let add__ (dst src: register): unit
else
cf.value <- False
let eor (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- BV8.to_uint (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
......@@ -1269,21 +1247,6 @@ let add_ (dst src: register): unit
else
cf.value <- 0
let add__ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let rd = BV8.of_int (get reg.data dst) in
let rr = BV8.of_int (get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- set reg.data dst (BV8.to_uint rd');
if BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7
then
cf.value <- 1
else
cf.value <- 0
let eor (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- BV8.to_uint (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
......
avrmodel/why3session.xml
View file @ 0ed6b403
......@@ -7,11 +7,11 @@
<prover id="2" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.1" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.5.0" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<file name="../avrmodel.mlw">
<theory name="AVRint" sum="995df742fcafccf2c6d106b1c8f28fe8">
<theory name="AVRint" sum="69ce702afe588152e81039482aba1cda">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="3"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
......@@ -35,7 +35,7 @@
</transf>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="3"><result status="valid" time="0.93" steps="223"/></proof>
<proof prover="3"><result status="valid" time="0.48" steps="178"/></proof>
</goal>
<goal name="WP_parameter adc" expl="VC for adc">
<proof prover="3"><result status="valid" time="0.44" steps="146"/></proof>
......@@ -130,22 +130,13 @@
<goal name="WP_parameter add_" expl="VC for add_">
<transf name="split_goal_wp">
<goal name="WP_parameter add_.1" expl="1. type invariant">
<proof prover="3"><result status="valid" time="0.08" steps="76"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="77"/></proof>
</goal>
<goal name="WP_parameter add_.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter add_.3" expl="3. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="58.02"/></proof>
</goal>
<goal name="WP_parameter add_.4" expl="4. type invariant">
<proof prover="3"><result status="valid" time="0.04" steps="76"/></proof>
</goal>
<goal name="WP_parameter add_.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter add_.6" expl="6. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="23.68"/></proof>
<proof prover="2" timelimit="60"><result status="valid" time="47.27"/></proof>
</goal>
</transf>
</goal>
......@@ -232,7 +223,7 @@
<proof prover="3" steplimit="-1"><result status="valid" time="2.91" steps="1009"/></proof>
</goal>
</theory>
<theory name="AVRint_limit" sum="d95ac809230c2c0794c6ea94f8b9ac9d">
<theory name="AVRint_limit" sum="f23992e42dcdd5b3a23543796cb90e80">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="3"><result status="valid" time="0.06" steps="69"/></proof>
</goal>
......@@ -246,7 +237,7 @@
<proof prover="3"><result status="valid" time="4.38" steps="150"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="3"><result status="valid" time="1.16" steps="223"/></proof>
<proof prover="3"><result status="valid" time="0.72" steps="178"/></proof>
</goal>
<goal name="WP_parameter adc" expl="VC for adc">
<proof prover="3"><result status="valid" time="0.58" steps="146"/></proof>
......@@ -336,7 +327,7 @@
<proof prover="3"><result status="valid" time="0.04" steps="67"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.4" expl="4. postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="0.27"/></proof>
<proof prover="5"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.07"/></proof>
......@@ -488,22 +479,13 @@
<goal name="WP_parameter add_" expl="VC for add_">
<transf name="split_goal_wp">
<goal name="WP_parameter add_.1" expl="1. type invariant">
<proof prover="3"><result status="valid" time="0.05" steps="76"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="WP_parameter add_.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter add_.3" expl="3. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="37.07"/></proof>
</goal>
<goal name="WP_parameter add_.4" expl="4. type invariant">
<proof prover="3"><result status="valid" time="0.06" steps="76"/></proof>
</goal>
<goal name="WP_parameter add_.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter add_.6" expl="6. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="42.15"/></proof>
<proof prover="2" timelimit="60"><result status="valid" time="42.04"/></proof>
</goal>
</transf>
</goal>
......@@ -511,23 +493,21 @@
<transf name="split_goal_wp">
<goal name="WP_parameter add__.1" expl="1. type invariant">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="76"/></proof>
</goal>
<goal name="WP_parameter add__.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter add__.3" expl="3. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="37.82"/></proof>
<proof prover="2" timelimit="60"><result status="valid" time="43.23"/></proof>
</goal>
<goal name="WP_parameter add__.4" expl="4. type invariant">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="76"/></proof>
<proof prover="1" steplimit="-1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter add__.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="1" steplimit="-1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter add__.6" expl="6. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="42.08"/></proof>
<proof prover="2" timelimit="60" steplimit="-1"><result status="valid" time="28.54"/></proof>
</goal>
</transf>
</goal>
......@@ -544,7 +524,7 @@
<proof prover="2"><result status="valid" time="0.89"/></proof>
</goal>
</theory>
<theory name="AVRint_alt" sum="61ff95a7ac4f2e016c224271648cf457">
<theory name="AVRint_alt" sum="c7d25b805b28d1ca69a32b949ddb1b16">
<goal name="WP_parameter mov" expl="VC for mov">
<proof prover="3"><result status="valid" time="0.03" steps="69"/></proof>
</goal>
......@@ -743,7 +723,7 @@
<proof prover="3"><result status="valid" time="0.02" steps="75"/></proof>
</goal>
<goal name="WP_parameter uint_shift.6" expl="6. assertion">
<proof prover="5" steplimit="1"><result status="valid" time="1.49"/></proof>
<proof prover="5"><result status="valid" time="1.49"/></proof>
</goal>
<goal name="WP_parameter uint_shift.7" expl="7. assertion">
<proof prover="3"><result status="valid" time="0.02" steps="82"/></proof>
......@@ -825,34 +805,6 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter add__" expl="VC for add__">
<transf name="split_goal_wp">
<goal name="WP_parameter add__.1" expl="1. type invariant">
<proof prover="3"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter add__.2" expl="2. type invariant">
<proof prover="3"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
<goal name="WP_parameter add__.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter add__.4" expl="4. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="37.95"/></proof>
</goal>
<goal name="WP_parameter add__.5" expl="5. type invariant">
<proof prover="3"><result status="valid" time="0.04" steps="71"/></proof>
</goal>
<goal name="WP_parameter add__.6" expl="6. type invariant">
<proof prover="3"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
<goal name="WP_parameter add__.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter add__.8" expl="8. postcondition">
<proof prover="2" timelimit="60"><result status="valid" time="23.38"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter eor" expl="VC for eor">
<proof prover="3"><result status="valid" time="0.04" steps="71"/></proof>
</goal>
......
avrmodel/why3shapes.gz
View file @ 0ed6b403
No preview for this file type
avrmodel2.mlw
View file @ 0ed6b403
......@@ -89,6 +89,7 @@ let add (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst in
let r1 = (Map.get reg.data dst) in
let r2 = (Map.get reg.data src) in
......@@ -418,11 +419,7 @@ let add_ (dst src: register): unit
let rr = BV8.of_int (Map.get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- Map.set reg.data dst (BV8.to_uint rd');
if BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7
then
cf.value <- True
else
cf.value <- False
cf.value <- (BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7)
let inc_ (dst: register): unit
writes { reg }
......
avrmodel2/why3session.xml
View file @ 0ed6b403
......@@ -8,7 +8,7 @@
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<file name="../avrmodel2.mlw">
<theory name="AVRint" sum="d5d935323eedfa7b127a8246499e1827">
<theory name="AVRint" sum="83ef08b223e4ffddcb377513715bebbb">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="3"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
......@@ -225,7 +225,7 @@
<goal name="WP_parameter add_" expl="VC for add_">
<transf name="split_goal_wp">
<goal name="WP_parameter add_.1" expl="1. type invariant">
<proof prover="3"><result status="valid" time="0.14" steps="76"/></proof>
<proof prover="3"><result status="valid" time="0.14" steps="77"/></proof>
</goal>
<goal name="WP_parameter add_.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.24"/></proof>
......@@ -233,15 +233,6 @@
<goal name="WP_parameter add_.3" expl="3. postcondition">
<proof prover="2" timelimit="130"><result status="valid" time="47.35"/></proof>
</goal>
<goal name="WP_parameter add_.4" expl="4. type invariant">
<proof prover="3"><result status="valid" time="0.13" steps="76"/></proof>
</goal>
<goal name="WP_parameter add_.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter add_.6" expl="6. postcondition">
<proof prover="2" timelimit="130" steplimit="-1"><result status="valid" time="16.46"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter inc_" expl="VC for inc_">
......
avrmodel2/why3shapes.gz
View file @ 0ed6b403
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