Commit 71f138c5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Bitvector: equality in programs

parent ab22e2ca
......@@ -16,7 +16,7 @@ theory bv.BV_Gen
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
syntax predicate (==) "(= %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
......
......@@ -18,7 +18,7 @@ theory bv.BV_Gen
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
syntax predicate (==) "(= %1 %2)"
(* Warning: we should NOT remove all the axioms using "allprops" *)
......
......@@ -29,7 +29,7 @@ module Test_proofinuse
type bitvec64 = BV64.t
let mask ( x : t ) =
ensures{ BV8.eq result (BV8.of_int 1) }
ensures{ result = BV8.of_int 1 }
(* ensures{ not ( BV8.eq result (BV8.of_int 1) ) } *)
let res = C8_32.toSmall(
bw_and
......
......@@ -3,37 +3,37 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="01976ddc6bd80d04acbe32f98fd3ce49">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
<theory name="Test_proofinuse" sum="158d6e24bf07e0b38048188cb356e855">
<goal name="VC shift_is_div" expl="VC for shift_is_div">
<transf name="split_goal_wp">
<goal name="WP_parameter shift_is_div.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<goal name="VC shift_is_div.1" expl="1. assertion">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.48" steps="136"/></proof>
<goal name="VC shift_is_div.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.37" steps="147"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<goal name="VC shift_is_div.3" expl="3. assertion">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="1.22" steps="203"/></proof>
<goal name="VC shift_is_div.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.50" steps="177"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter mask" expl="VC for mask">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC mask" expl="VC for mask">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter testVariant" expl="VC for testVariant">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC testVariant" expl="VC for testVariant">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ttt">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="a0944cec62c66f9386bc79e4c44a0f16">
<theory name="Hackers_delight" sum="66d0bda7ff93bb79f32092fd9a35a9fe">
<goal name="DM1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -92,69 +92,69 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="32d38cd9c48389171edd12feea17b382">
<goal name="WP_parameter dm1" expl="VC for dm1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<theory name="Hackers_delight_mod" sum="eb3ef503d17c919ce3d2ce5d7ebbd192">
<goal name="VC dm1" expl="VC for dm1">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter dm2" expl="VC for dm2">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC dm2" expl="VC for dm2">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter dm3" expl="VC for dm3">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC dm3" expl="VC for dm3">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter dm4" expl="VC for dm4">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<goal name="VC dm4" expl="VC for dm4">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter dm5" expl="VC for dm5">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC dm5" expl="VC for dm5">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter dm6" expl="VC for dm6">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="VC dm6" expl="VC for dm6">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter dm7" expl="VC for dm7">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC dm7" expl="VC for dm7">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter dm8" expl="VC for dm8">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<goal name="VC dm8" expl="VC for dm8">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter dmtest" expl="VC for dmtest">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC dmtest" expl="VC for dmtest">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter ie1" expl="VC for ie1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC ie1" expl="VC for ie1">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter ie2" expl="VC for ie2">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="VC ie2" expl="VC for ie2">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter ie3" expl="VC for ie3">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<goal name="VC ie3" expl="VC for ie3">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter ie4" expl="VC for ie4">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<goal name="VC ie4" expl="VC for ie4">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sr1" expl="VC for sr1">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="VC sr1" expl="VC for sr1">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter rs_left" expl="VC for rs_left">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC rs_left" expl="VC for rs_left">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter rs_right" expl="VC for rs_right">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC rs_right" expl="VC for rs_right">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter bp1" expl="VC for bp1">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<goal name="VC bp1" expl="VC for bp1">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter bp1&apos;" expl="VC for bp1&apos;">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC bp1&apos;" expl="VC for bp1&apos;">
<proof prover="1"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="WP_parameter bp2" expl="VC for bp2">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<goal name="VC bp2" expl="VC for bp2">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter bp3" expl="VC for bp3">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<goal name="VC bp3" expl="VC for bp3">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="3b53ccfb24b0e5076075a7389a6e49e5">
<theory name="Test_imperial_violet" sum="84c4bc98193118bbf8135e376ca1bb6c">
<goal name="bv32_bounds_bv">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -170,11 +170,42 @@
<goal name="bv32_bounds">
<proof prover="0"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="4"><result status="valid" time="0.16"/></proof>
<goal name="VC add" expl="VC for add">
<transf name="split_goal_wp">
<goal name="VC add.1" expl="1. array creation size">
<proof prover="1"><result status="valid" time="0.03" steps="69"/></proof>
</goal>
<goal name="VC add.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
<goal name="VC add.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
<goal name="VC add.4" expl="4. loop invariant init">
<proof prover="1"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
<goal name="VC add.5" expl="5. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="72"/></proof>
</goal>
<goal name="VC add.6" expl="6. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="VC add.7" expl="7. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="VC add.8" expl="8. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="VC add.9" expl="9. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.18" steps="132"/></proof>
</goal>
<goal name="VC add.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="6b18dfa01a56b248764549f53590545a">
<theory name="Test_from_bitvector_example" sum="238cabfc0fd7ad4c671f1f60c618bf11">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -193,32 +224,32 @@
<goal name="Test6">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter lsr31" expl="VC for lsr31">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr31" expl="VC for lsr31">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr30" expl="VC for lsr30">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr30" expl="VC for lsr30">
<proof prover="2" timelimit="1" steplimit="-1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr29" expl="VC for lsr29">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr29" expl="VC for lsr29">
<proof prover="1"><result status="valid" time="0.07" steps="90"/></proof>
</goal>
<goal name="WP_parameter lsr28" expl="VC for lsr28">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr28" expl="VC for lsr28">
<proof prover="1"><result status="valid" time="0.07" steps="90"/></proof>
</goal>
<goal name="WP_parameter lsr27" expl="VC for lsr27">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr27" expl="VC for lsr27">
<proof prover="1"><result status="valid" time="0.07" steps="90"/></proof>
</goal>
<goal name="WP_parameter lsr26" expl="VC for lsr26">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<goal name="VC lsr26" expl="VC for lsr26">
<proof prover="1"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
<goal name="WP_parameter lsr20" expl="VC for lsr20">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr20" expl="VC for lsr20">
<proof prover="1"><result status="valid" time="0.04" steps="90"/></proof>
</goal>
<goal name="WP_parameter lsr13" expl="VC for lsr13">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr13" expl="VC for lsr13">
<proof prover="1"><result status="valid" time="0.04" steps="90"/></proof>
</goal>
<goal name="WP_parameter lsr8" expl="VC for lsr8">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC lsr8" expl="VC for lsr8">
<proof prover="1"><result status="valid" time="0.04" steps="90"/></proof>
</goal>
<goal name="to_int_0x00000001">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......
......@@ -312,13 +312,12 @@ module Bitwalker
requires {BV64.to_uint value < BV64.to_uint (maxvalue len)}
ensures {result = value}
=
assert { forall i:int. BV32.to_uint len <= i < 64 -> BV64.nth value i = False };
assert { forall i:int. BV32.to_uint len <= i < 64 ->
BV64.nth value i = False };
let poke_result = poke start len addr value in
assert {poke_result = 0};
assert { poke_result = 0 };
let peek_result = peek start len addr in
assert {BV64.eq peek_result value};
assert { BV64.(==) peek_result value };
peek_result
end
This diff is collapsed.
......@@ -168,7 +168,7 @@ theory BV_Check
eq_sub a b (to_uint i) (to_uint n)
<-> eq_sub_bv a b i n
goal Extensionality: forall x y : t [eq x y]. eq x y -> x = y
goal Extensionality: forall x y : t [x == y]. x == y -> x = y
end
......
......@@ -25,7 +25,6 @@ module BVCheck_Gen
function asr t int : t
function asr_bv t t : t
predicate eq t t
predicate ule t t
predicate ult t t
predicate uge t t
......@@ -79,64 +78,26 @@ module BVCheck_Gen
ensures { result = urem a b }
val eq_check (a b:t) : bool
ensures { match result with
| True -> to_uint a = to_uint b
| False -> to_uint a <> to_uint b
end }
ensures { match result with
| True -> eq a b
| False -> not (eq a b)
end }
ensures { result <-> a = b }
val ne_check (a b:t) : bool
ensures { match result with
| True -> to_uint a <> to_uint b
| False -> to_uint a = to_uint b
end }
ensures { match result with
| True -> not (eq a b)
| False -> eq a b
end }
ensures { result <-> a <> b }
val le_check (a b:t) : bool
ensures { match result with
| True -> to_uint a <= to_uint b
| False -> to_uint a > to_uint b
end }
ensures { match result with
| True -> ule a b
| False -> not (ule a b)
end }
ensures { result <-> to_uint a <= to_uint b }
ensures { result <-> ule a b }
val lt_check (a b:t) : bool
ensures { match result with
| True -> to_uint a < to_uint b
| False -> to_uint a >= to_uint b
end }
ensures { match result with
| True -> ult a b
| False -> not (ult a b)
end }
ensures { result <-> to_uint a < to_uint b }
ensures { result <-> ult a b }
val ge_check (a b:t) : bool
ensures { match result with
| True -> to_uint a >= to_uint b
| False -> to_uint a < to_uint b
end }
ensures { match result with
| True -> uge a b
| False -> not (uge a b)
end }
ensures { result <-> to_uint a >= to_uint b }
ensures { result <-> uge a b }
val gt_check (a b:t) : bool
ensures { match result with
| True -> to_uint a > to_uint b
| False -> to_uint a <= to_uint b
end }
ensures { match result with
| True -> ugt a b
| False -> not (ugt a b)
end }
ensures { result <-> to_uint a > to_uint b }
ensures { result <-> ugt a b }
end
......@@ -161,7 +122,6 @@ module BVCheck8
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
......@@ -189,7 +149,6 @@ module BVCheck16
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
......@@ -217,7 +176,6 @@ module BVCheck32
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
......@@ -245,7 +203,6 @@ module BVCheck64
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
......
......@@ -385,13 +385,13 @@ theory BV_Gen
eq_sub a b (to_uint i) (to_uint n)
<-> eq_sub_bv a b i n
predicate eq (v1 v2 : t) =
predicate (==) (v1 v2 : t) =
eq_sub v1 v2 0 size
axiom Extensionality: forall x y : t [eq x y]. eq x y -> x = y
axiom Extensionality: forall x y : t [x == y]. x == y -> x = y
val eq (v1 v2 : t) : bool
ensures { if result then v1 = v2 else v1 <> v2 }
ensures { result <-> v1 = v2 }
end
......
Markdown is supported
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