stdlib/microc.mlw

   1
   2 (** Support library for the Micro-C format. *)
   3
   4 module MicroC
   5
   6   use int.Int
   7   use ref.Ref
   8   use array.Array
   9
  10   function length (a: array 'a) : int =
  11     Array.length a
  12
  13   function ([]) (a: array 'a) (i: int) : 'a =
  14     Array.([]) a i
  15
  16   function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a =
  17     Array.([<-]) a i v
  18
  19   let ([]) (a: array 'a) (i: int) : 'a
  20     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  21     ensures  { result = a[i] }
  22   = Array.([]) a i
  23
  24   let ([]<-) (a: array 'a) (i: int) (v: 'a) : unit
  25     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  26     ensures  { a = Array.([<-]) (old a) i v }
  27   = Array.([]<-) a i v
  28
  29   use map.Occ
  30
  31   function occurrence (v: 'a) (a: array 'a) : int =
  32     Occ.occ v a.Array.elts 0 a.Array.length
  33
  34   use export int.ComputerDivision
  35
  36   val (/) (x y: int) : int
  37     requires { [@expl:check division by zero] y <> 0 }
  38     ensures  { result = div x y }
  39
  40   val (/=) (ref x: int) (y: int) : unit writes {x}
  41     requires { [@expl:check division by zero] y <> 0 }
  42     ensures  { x = div (old x) y }
  43
  44   val (%) (x y: int) : int
  45     requires { y <> 0 }
  46     ensures  { result = mod x y }
  47
  48   (* operators ++ -- on integers *)
  49   let __postinc (ref r: int) : int
  50     ensures { r = old r + 1 }
  51     ensures { result = old r }
  52   = let v = r in r <- r + 1; v
  53
  54   let __postdec (ref r: int) : int
  55     ensures { r = old r - 1 }
  56     ensures { result = old r }
  57   = let v = r in r <- r - 1; v
  58
  59   let __preinc (ref r: int) : int
  60     ensures { result = r = old r + 1 }
  61   = r <- r + 1; r
  62
  63   let __predec (ref r: int) : int
  64     ensures { result = r = old r - 1 }
  65   = r <- r - 1; r
  66
  67   (* operators ++ -- on array elements *)
  68   let __arrpostinc (a: array int) (i: int) : int
  69     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  70     ensures  { a = (old a)[i <- (old a)[i] + 1] }
  71     ensures  { result = old a[i] }
  72   = let v = a[i] in a[i] <- v + 1; v
  73
  74   let __arrpostdec (a: array int) (i: int) : int
  75     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  76     ensures  { a = (old a)[i <- (old a)[i] - 1] }
  77     ensures  { result = old a[i] }
  78   = let v = a[i] in a[i] <- v - 1; v
  79
  80   let __arrpreinc (a: array int) (i: int) : int
  81     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  82     ensures  { a = (old a)[i <- (old a)[i] + 1] }
  83     ensures  { result = a[i] }
  84   = a[i] <- a[i] + 1; a[i]
  85
  86   let __arrpredec (a: array int) (i: int) : int
  87     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  88     ensures  { a = (old a)[i <- (old a)[i] - 1] }
  89     ensures  { result = a[i] }
  90   = a[i] <- a[i] - 1; a[i]
  91
  92   (* operators += -= on array elements *)
  93   let __array_add (a: array int) (i: int) (x: int) : unit
  94     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
  95     ensures  { a = (old a)[i <- (old a)[i] + x] }
  96   = a[i] <- a[i] + x
  97
  98   let __array_sub (a: array int) (i: int) (x: int) : unit
  99     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
 100     ensures  { a = (old a)[i <- (old a)[i] - x] }
 101   = a[i] <- a[i] - x
 102
 103   let __array_mul (a: array int) (i: int) (x: int) : unit
 104     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
 105     ensures  { a = (old a)[i <- (old a)[i] * x] }
 106   = a[i] <- a[i] * x
 107
 108   let __array_div (a: array int) (i: int) (x: int) : unit
 109     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
 110     requires { [@expl:check division by zero] x <> 0 }
 111     ensures  { a = (old a)[i <- div (old a)[i] x] }
 112   = a[i] <- a[i] / x
 113
 114   (* to initialize stack-allocated variables *)
 115
 116   val any_int () : int
 117
 118   val alloc_array (n: int) : array int
 119     requires { n >= 0 }
 120     ensures  { length result = n }
 121
 122   (* C library *)
 123
 124   val rand () : int
 125     ensures  { 0 <= result }
 126
 127   val scanf (ref r: int) : unit
 128     writes { r }
 129
 130   exception Break
 131
 132   exception Return int
 133
 134 end