esterel.mlw 2.45 KB
 MARCHE Claude committed Mar 15, 2016 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 `````` (** {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``````