examples/multiprecision/ptralias.mlw

   1 module Alias
   2
   3   use mach.c.C
   4   use lemmas.Lemmas
   5   use int.Int
   6   use mach.int.Int32
   7   use import mach.int.UInt64GMP as Limb
   8   use types.Types
   9   use types.Int32Eq
  10   use types.UInt64Eq
  11   use array.Array
  12   use map.Map
  13
  14   type mem = abstract { zr:zone; zx:zone; zy:zone;
  15                         mr: int32; mx: int32; my: int32;
  16                         lr: int32; lx: int32; ly: int32;
  17                         mutable ok: bool }
  18
  19   predicate identical (p1 p2:ptr limb) =
  20     data p1 = data p2 /\ offset p1 = offset p2
  21     /\ min p1 = min p2 /\ max p1 = max p2 /\ zone p1 = zone p2
  22
  23
  24   val open_sep (r x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32) :
  25                (nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
  26     requires { valid r sx /\ valid x sx /\ valid y sy }
  27     requires { writable r }
  28     requires { 0 <= sy <= sx }
  29     ensures { writable nr }
  30     ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
  31     ensures { valid nr sx /\ valid nx sx /\ valid ny sy }
  32     ensures { 0 <= offset nr /\ offset nr + sx <= offset nx
  33               /\ offset nx + sx <= offset ny }
  34     ensures { m.zr = r.zone /\ m.zx = x.zone /\ m.zy = y.zone }
  35     ensures { m.mr = old r.max /\ m.mx = old x.max /\ m.my = old y.max }
  36     ensures { m.lr = sx /\ m.lx = sx /\ m.ly = sy }
  37     ensures { m.ok }
  38     ensures { map_eq_sub_shift (pelts nr) (pelts r) (offset nr) (offset r) sx }
  39     ensures { map_eq_sub_shift (pelts nx) (pelts x) (offset nx) (offset x) sx }
  40     ensures { map_eq_sub_shift (pelts ny) (pelts y) (offset ny) (offset y) sy }
  41     ensures { pelts r = old pelts r /\ pelts x = old pelts x
  42               /\ pelts y = old pelts y }
  43     ensures { plength r = old plength r /\ plength x = old plength x
  44               /\ plength y = old plength y }
  45     ensures { min r = old min r /\ min x = old min x /\ min y = old min y }
  46     ensures { data nr = data nx = data ny }
  47     writes  { r, x, y }
  48     alias { nr.data with nx.data }
  49     alias { nr.data with ny.data }
  50     alias { nx.data with ny.data }
  51
  52   val close_sep (r x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32)
  53                 (nr nx ny:ptr limb) (ghost m:mem) : unit
  54     alias { nr.data with nx.data }
  55     alias { nr.data with ny.data }
  56     alias { nx.data with ny.data }
  57     requires { m.ok }
  58     requires { 0 <= sy <= sx }
  59     requires { m.zr = r.zone /\ m.zx = x.zone /\ m.zy = y.zone }
  60     requires { m.lr = sx /\ m.lx = sx /\ m.ly = sy }
  61     requires { 0 <= offset nr /\ offset nr + sx <= offset nx
  62                /\ offset nx + sx <= offset ny }
  63     requires { writable r /\ writable nr }
  64     ensures { r.max = m.mr /\ x.max = m.mx /\ y.max = m.my }
  65     ensures { map_eq_sub_shift (old pelts nr) (pelts r)
  66                                (offset nr) (offset r) sx }
  67     ensures { map_eq_sub_shift (old pelts nx) (pelts x)
  68                                (offset nx) (offset x) sx }
  69     ensures { map_eq_sub_shift (old pelts ny) (pelts y)
  70                                (offset ny) (offset y) sy }
  71     ensures { forall j. j < offset r \/ offset r + sx <= j
  72               -> (pelts r)[j] = old (pelts r)[j] }
  73     ensures { forall j. j < offset x \/ offset x + sx <= j
  74               -> (pelts x)[j] = old (pelts x)[j] }
  75     ensures { forall j. j < offset y \/ offset y + sy <= j
  76               -> (pelts y)[j] = old (pelts y)[j] }
  77     ensures { plength r = old plength r /\ plength x = old plength x
  78               /\ plength y = old plength y }
  79     ensures { min r = old min r /\ min x = old min x /\ min y = old min y }
  80     writes { nr, nx, ny, nr.data, nx.data, ny.data,
  81              r.data, r.max, x.data, x.max, y.data, y.max, m.ok }
  82
  83   val open_rx (x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32) :
  84                (nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
  85     requires { valid x sx /\ valid y sy }
  86     requires { 0 <= sy <= sx }
  87     requires { writable x }
  88     ensures { writable nr }
  89     ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
  90     ensures { valid nx sx /\ valid ny sy }
  91     ensures { identical nr nx }
  92     ensures { 0 <= offset nx /\ offset nx + sx <= offset ny
  93               \/ 0 <= offset ny /\ offset ny + sy <= offset nx }
  94     ensures { m.zx = x.zone /\ m.zy = y.zone }
  95     ensures { m.mx = old x.max /\ m.my = old y.max }
  96     ensures { m.lx = sx /\ m.ly = sy }
  97     ensures { m.ok }
  98     ensures { map_eq_sub_shift (pelts nx) (pelts x) (offset nx) (offset x) sx }
  99     ensures { map_eq_sub_shift (pelts ny) (pelts y) (offset ny) (offset y) sy }
 100     ensures { pelts x = old pelts x /\ pelts y = old pelts y }
 101     ensures { plength x = old plength x /\ plength y = old plength y }
 102     ensures { min x = old min x /\ min y = old min y }
 103     ensures { data nr = data nx = data ny }
 104     writes  { x, y }
 105     alias { nr.data with nx.data }
 106     alias { nr.data with ny.data }
 107     alias { nx.data with ny.data }
 108
 109   val close_rx (x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32)
 110                 (nr nx ny:ptr limb) (ghost m:mem) : unit
 111     alias { nr.data with nx.data }
 112     alias { nr.data with ny.data }
 113     alias { nx.data with ny.data }
 114     requires { writable x /\ writable nr }
 115     requires { m.ok }
 116     requires { 0 <= sy <= sx }
 117     requires { identical nr nx }
 118     requires { 0 <= offset nx /\ offset nx + sx <= offset ny
 119                \/ 0 <= offset ny /\ offset ny + sy <= offset nx  }
 120     requires { m.zx = x.zone /\ m.zy = y.zone }
 121     requires { m.lx = sx /\ m.ly = sy }
 122     ensures { x.max = m.mx /\ y.max = m.my }
 123     ensures { map_eq_sub_shift (old pelts nx) (pelts x)
 124                                (offset nx) (offset x) sx }
 125     ensures { map_eq_sub_shift (old pelts ny) (pelts y)
 126                                (offset ny) (offset y) sy }
 127     ensures { forall j. j < offset x \/ offset x + sx <= j
 128               -> (pelts x)[j] = old (pelts x)[j] }
 129     ensures { forall j. j < offset y \/ offset y + sy <= j
 130               -> (pelts y)[j] = old (pelts y)[j] }
 131     ensures { plength x = old plength x /\ plength y = old plength y }
 132     ensures { min x = old min x /\ min y = old min y }
 133     writes { nr, nx, ny, nr.data, nx.data, ny.data,
 134              x.data, x.max, y.data, y.max, m.ok }
 135
 136   val open_shift_sep (r x:ptr limb) (ghost sz:int32) :
 137                      (nr:ptr limb, nx:ptr limb, ghost m:mem)
 138     requires { valid r sz /\ valid x sz }
 139     requires { 0 <= sz }
 140     requires { writable r }
 141     ensures  { writable nr }
 142     ensures  { value nx sz = old value x sz }
 143     ensures  { valid nr sz /\ valid nx sz }
 144     ensures  { 0 <= offset nx /\ offset nx + sz <= offset nr }
 145     ensures  { m.zr = zone r /\ m.zx = zone x }
 146     ensures  { m.mr = old r.max /\ m.mx = old x.max }
 147     ensures  { m.lr = m.lx = sz }
 148     ensures  { m.ok }
 149     ensures  { map_eq_sub_shift (pelts nx) (pelts x) (offset nx) (offset x) sz }
 150     ensures  { map_eq_sub_shift (pelts nr) (pelts r) (offset nr) (offset r) sz }
 151     ensures  { pelts r = old pelts r /\ pelts x = old pelts x }
 152     ensures  { plength r = old plength r /\ plength x = old plength x }
 153     ensures  { min r = old min r /\ min x = old min x }
 154     ensures  { data nr = data nx }
 155     writes   { r, x }
 156     alias    { nr.data with nx.data }
 157
 158   val close_shift_sep (r x:ptr limb) (ghost sz:int32) (nr nx:ptr limb) (ghost m:mem)
 159                       : unit
 160     alias    { nr.data with nx.data }
 161     requires { writable r /\ writable nr }
 162     requires { m.ok }
 163     requires { 0 <= sz }
 164     requires { 0 <= offset nx /\ offset nx + sz <= offset nr }
 165     requires { m.zx = x.zone /\ m.zr = r.zone }
 166     requires { m.lx = m.lr = sz }
 167     ensures  { x.max = m.mx /\ r.max = m.mr }
 168     ensures  { map_eq_sub_shift (old pelts nx) (pelts x)
 169                                 (offset nx) (offset x) sz }
 170     ensures  { map_eq_sub_shift (old pelts nr) (pelts r)
 171                                 (offset nr) (offset r) sz }
 172     ensures  { forall j. j < offset x \/ offset x + sz <= j
 173                 -> (pelts x)[j] = old (pelts x)[j] }
 174     ensures  { forall j. j < offset r \/ offset r + sz <= j
 175                 -> (pelts r)[j] = old (pelts r)[j] }
 176     ensures  { plength x = old plength x /\ plength r = old plength r }
 177     ensures  { min r = old min r /\ min x = old min x }
 178     writes   { nr, nx, nr.data, nx.data, x.data, x.max, r.data, r.max, m.ok }
 179
 180 (*
 181   let double_open (r x y: ptr limb)
 182     requires { valid r 0 /\ valid x 0 /\ valid y 0 }
 183   =
 184     let nr, nx, ny, m = open_sep r x 0 y 0 in
 185     let nr, nx, ny, m = open_sep r x 0 y 0 in
 186         (* invalid precondition valid _ 0 *)
 187     close_sep r x 0 y 0 nr nx ny m
 188
 189   let double_free (r x y: ptr limb)
 190     requires { valid r 0 /\ valid x 0 /\ valid y 0 }
 191   =
 192     let nr, nx, ny, m = open_sep r x 0 y 0 in
 193     close_sep r x 0 y 0 nr nx ny m;
 194     close_sep r x 0 y 0 nr nx ny m (* invalid precondition m.ok *)
 195
 196   let use_after_open (r x y: ptr limb)
 197     requires { valid x 1 }
 198   =
 199     let x' = incr x 0 in
 200     let nr, nx, ny, m = open_sep r x 0 y 0 in (* forbids x'*)
 201     let a = C.get x' in
 202     close_sep r x 0 y 0 nr nx ny m
 203 *)
 204
 205 end