esterel.mlw 2.44 KB
Newer Older
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


(** {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 {
36
    forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl
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
  }


  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