examples/multiprecision/mpz_realloc2.mlw

   1 module Zrealloc2
   2
   3 use int.Int
   4 use int.Power
   5 use int.EuclideanDivision
   6 use map.Map
   7 use mach.int.Int32GMP
   8 use mach.c.C
   9 use lemmas.Lemmas
  10 use util.Util
  11 use compare.Compare
  12 use mach.int.UInt64GMP
  13 use int.Abs
  14 use mpz.Z
  15 use mpz.Zutil
  16
  17
  18 function alloc_of_bits (bits: int) : int
  19 = if bits <= 0 then 1 else div (bits + 63) 64
  20
  21 let partial wmpz_realloc2 (x:mpz_ptr) (bits:uint64) : unit
  22   requires { mpz.readers[x] = 0 }
  23   requires { div (bits - 1) 64 < max_int32 }
  24   requires { 1 <= mpz.alloc[x] }
  25   ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  26   ensures  { mpz.readers[x] = 0 }
  27   ensures  { mpz.alloc[x] = alloc_of_bits bits }
  28   ensures  { if alloc_of_bits bits >= old mpz.abs_size[x]
  29              then mpz.abs_size[x] = old mpz.abs_size[x]
  30                   /\ mpz.abs_value_of[x] = old mpz.abs_value_of[x]
  31              else mpz.abs_size[x] = 0 }
  32 =
  33   let ghost obits = bits in
  34   let bits = bits - (if bits <> 0 then 1 else 0) in
  35   let new_alloc = UInt64GMP.to_int32 (1 + (bits / 64)) in
  36   assert { new_alloc = alloc_of_bits obits };
  37   let p = get_write_ptr x in
  38   assert { forall y. y <> x -> mpz_unchanged y mpz (old mpz) };
  39   let ghost op = { p } in
  40   let ghost os = abs_size_of x in
  41   let q = realloc p new_alloc in
  42   c_assert (is_not_null q);
  43   if Int32.(>) (abs_size_of x) new_alloc
  44   then begin
  45     set_size_0 x; (* data has shrunk, reset x to 0 *)
  46   end
  47   else begin
  48     value_sub_frame (pelts q) (pelts op) 0 (p2i os);
  49   end;
  50   set_alloc x new_alloc;
  51   set_ptr x q;
  52   release_writer x q
  53
  54
  55 end