Commit a541f3ca authored by MARCHE Claude's avatar MARCHE Claude

New example: Berry's challenge from Esterel compiler

parent 9f77a2ab
(** {1 Challenge about the Esterel Compiler}
This is a challenge given by Gérard Berry, extracted from
Esterel compiler.
1. Each instruction returns an integer code between [1] and
[N]. Parallel execution returns the maximum of codes of its
branches.
2. Return codes are implemented as bitvectors.
3. During static analysis, each instruction [P] may return a set of
codes [C(P)] instead of one code only. Hence [P||Q] must return
[{max(p,q) | p in C(p), q in C(q)], to be computed on bitvectors.
4. A method given by Georges Gonthier is to write the result under the
form [{ x in P U Q | x >= max (min(P), min(Q) }] that can be
encoded as bitvector operation [(P|Q)&(P|-P)&(Q|-Q)].
*)
module Esterel
use import int.Int
use import int.MinMax
use import set.Fsetint
use import bv.BV64
type s = {
bv : BV64.t; (* a 64-bit bitvector *)
ghost mdl: set int; (* its interpretation as a set *)
}
invariant {
forall i: int. (0 <= i < size /\ nth self.bv i) <-> mem i self.mdl
}
let union (a b: s) : s (* operator [a|b] *)
ensures { result.mdl = union b.mdl a.mdl }
= { bv = bw_or a.bv b.bv;
mdl = union b.mdl a.mdl }
let intersection (a b : s) : s (* operator [a&b] *)
ensures { result.mdl = inter a.mdl b.mdl }
= { bv = bw_and a.bv b.bv;
mdl = inter a.mdl b.mdl }
let aboveMin (a : s) : s (* operator [a|-a] *)
requires { not is_empty a.mdl }
ensures { result.mdl = interval (min_elt a.mdl) size }
= let ghost p = min_elt a.mdl in
let ghost p_bv = of_int p in
assert { eq_sub_bv a.bv zeros zeros p_bv };
let res = bw_or a.bv (neg a.bv) in
assert { eq_sub_bv res zeros zeros p_bv };
assert { eq_sub_bv res ones p_bv (sub size_bv p_bv) };
{ bv = res;
mdl = interval p size }
let maxUnion (a b : s) : s (* operator [(a|b)&(a|-a)&(b|-b)] *)
requires { not is_empty a.mdl /\ not is_empty b.mdl }
ensures { forall x. mem x result.mdl <->
(mem x (union a.mdl b.mdl) /\
x >= max (min_elt a.mdl) (min_elt b.mdl)) }
ensures { forall x. mem x result.mdl <->
exists y z. mem y a.mdl /\ mem z b.mdl /\ x = max y z }
= let res =
intersection (union a b) (intersection (aboveMin a) (aboveMin b))
in
assert {
forall x. mem x res.mdl ->
let (y,z) =
if mem x a.mdl then (x,min_elt b.mdl) else (min_elt a.mdl,x)
in
mem y a.mdl /\ mem z b.mdl /\ x = max y z };
res
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="4000" memlimit="-1"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="4000" memlimit="-1"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="4000" memlimit="-1"/>
<file name="../esterel.mlw" expanded="true">
<theory name="Esterel" sum="a43de3ed68b03982f261f5072b3943c0" expanded="true">
<goal name="WP_parameter union" expl="VC for union" expanded="true">
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.20" steps="219"/></proof>
</goal>
<goal name="WP_parameter intersection" expl="VC for intersection" expanded="true">
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.18" steps="186"/></proof>
</goal>
<goal name="WP_parameter aboveMin" expl="VC for aboveMin" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter aboveMin.1" expl="1. assertion">
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.28" steps="206"/></proof>
</goal>
<goal name="WP_parameter aboveMin.2" expl="2. assertion">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.22"/></proof>
<proof prover="2" steplimit="-1" memlimit="4000"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="WP_parameter aboveMin.3" expl="3. assertion">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.60"/></proof>
</goal>
<goal name="WP_parameter aboveMin.4" expl="4. type invariant">
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.45" steps="326"/></proof>
</goal>
<goal name="WP_parameter aboveMin.5" expl="5. postcondition">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.03"/></proof>
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.02" steps="68"/></proof>
<proof prover="2" steplimit="-1" memlimit="4000"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter maxUnion" expl="VC for maxUnion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter maxUnion.1" expl="1. precondition">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.05"/></proof>
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.01" steps="70"/></proof>
<proof prover="2" steplimit="-1" memlimit="4000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxUnion.2" expl="2. precondition">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.05"/></proof>
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.02" steps="71"/></proof>
<proof prover="2" steplimit="-1" memlimit="4000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter maxUnion.3" expl="3. assertion">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.25"/></proof>
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.30" steps="379"/></proof>
<proof prover="2" steplimit="-1" memlimit="4000"><result status="valid" time="0.63"/></proof>
</goal>
<goal name="WP_parameter maxUnion.4" expl="4. postcondition">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.26"/></proof>
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="2.21" steps="1518"/></proof>
</goal>
<goal name="WP_parameter maxUnion.5" expl="5. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter maxUnion.5.1" expl="1. postcondition">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter maxUnion.5.2" expl="2. postcondition">
<proof prover="0" steplimit="-1" memlimit="4000"><result status="valid" time="0.31"/></proof>
<proof prover="1" steplimit="-1" memlimit="4000"><result status="valid" time="0.43" steps="412"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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