test_extraction.mlw 7.15 KB
Newer Older
1 2 3 4

(* test of the OCaml extraction
   run "make test-ocaml-extraction" from the top directory *)

Mário Pereira's avatar
Mário Pereira committed
5 6
(* TODO : add a test for match .. with .. exception expressions *)

7 8
module TestExtraction

9 10
  use int.Int
  use int.ComputerDivision
11 12 13
  let f (x: int) : int = x+1
  let test_int () = f 31 + (div 33 3 + 2 - 4) - -1

14
  use mach.int.Int63
15
  let f63 (x: int63) : int63 = x + 1
16
  let test_int63 () =
17
    to_int (f63 31 + (33 / 3 + 2 - 4) - (-1))
18

19 20 21
  use int.Int
  use ref.Ref
  use ref.Refint
22 23 24 25 26 27 28 29

  let test_ref () : int =
    let r = ref 0 in
    incr r;
    r := !r * 43;
    decr r;
    !r

30
  use array.Array
31 32

  let test_array () =
33
    let a = Array.make 43 (0:int63) in
34 35 36
    for i = 1 to 42 do a[i] <- a[i-1] + 1 done;
    a[42]

37
  use mach.array.Array63
38 39

  let test_array63 () : int =
40
    let a = Array63.make 43 0 in
41
    for i = 1 to 42 do a[Int63.of_int i] <- a[Int63.of_int (i - 1)] + 1 done;
42
    a[42]
43

44 45 46
  use seq.Seq
  use int.Int
  use mach.int.Int
47

48 49 50 51
  (* FIXME: this function is never used.
            Use it somewhere and supply a driver? *)
  (* val test_val (x: int) : int *)
  (*   ensures { result > x } *)
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 83 84 85 86 87 88 89 90 91

  let function f_function (y: int) (x: int) : int
    requires { x >= 0 }
    ensures  { result >= 0 }
  = x

  let g (ghost z: int) (x: int) : int
    requires { x > 0 }
    ensures  { result > 0 }
  = let y = x in
    y

  type t 'a 'b 'c 'd

  type list 'a = Nil | Cons 'a (list 'a)

  type btree 'a = E | N (btree 'a) 'a (btree 'a)

  type ntree 'a = Empty | Node 'a (list 'a)

  type list_int = list int

  type cursor 'a = {
    collection : list 'a;
    index      : int;
    mutable index2     : int;
    ghost mutable v : seq 'a;
  }

  type r 'a = {
    aa: 'a;
    ghost i: int;
  }

  (* let create_cursor (l: list int) (i i2: int) : cursor int = *)
  (*   { collection = l; index = i; index2 = i2; v = empty } *)

  let create_r (x: int) (y: int) : r int =
    { aa = x; i = y }

92
  use ref.Ref
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137

  let update (c: cursor int) : int
  = c.index

  exception Empty (list int, int)
  exception Out_of_bounds int

  (* exception are unary constructors *)
(*
  let raise1 () =
    raises { Empty -> true }
    raise (Empty (Nil, 0))
  let raise2 () =
    raises { Empty -> true }
    let p = (Nil, 0) in
    raise (Empty p)
*)

  let rec length (l: list 'a) : int
    variant  { l }
  = match l with
    | Nil -> 0
    | Cons _ r -> 1 + length r
    end

  let t (x:int) : int
    requires { false }
  = absurd

  let a () : unit
  = assert { true }

  let singleton (x: int) (l: list int) : list int =
    let x = Nil in x

(* FIXME constructors in Why3 can be partially applied
         => an eta-expansion is needed
         be careful with side-effects
         "let c = Cons e in" should be translated to
         "let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml

   Mário: I think A-normal form takes care of the side-effects problem
*)
  let constructor1 () =
    let x = Cons in
138
    x (42:int63)
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165

  let foofoo (x: int) : int =
    let ghost y = x + 1 in
    x

  let test (x: int) : int =
    let y =
      let z = x in
      (ghost z) + 1
    in 42

  type list_ghost = Nil2 | Cons2 int list_ghost (ghost int)

  let add_list_ghost (x: int) (l: list_ghost) : list_ghost =
    match l with
    | Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 (1+2)
    | Cons2 _ _ n -> Cons2 x l (n+1)
    end

  let ggg () : int = 42

  let call (x:int) : int =
    ggg () + 42

  (* functions with ghost arguments *)

  let test_filter_ghost_args (x: int) (ghost y: int) =
166
    (1:int) / 0
167 168 169 170 171

  let test_call (x: int) : int =
    test_filter_ghost_args x 0 + 1

  let constant test_partial : int =
172
    let partial_ex = test_filter_ghost_args 3 in
173 174
    42

175 176 177 178 179 180 181 182 183
  let constant test_partial2 : int =
    let r = ref 0 in
    let f (x: int) (ghost y) = r := !r + 21 in
    let g = f 17 in
    g (0:int); g (1:int); !r

  let test_zero_args () : int =
    test_partial2 + 0

184 185 186 187 188 189 190 191 192
  let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int =
    x + z

  let test_filter_ghost_args3 (ghost y: int) : int =
    1 / 0

  let many_args (a b c d e f g h i j k l m: int) : int = 42

  let foo (x: int) : int =
193
    let _ = (42:int63) in (* FIXME? print _ in OCaml *)
194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
    x

  let test_fun (x: int) : int -> int =
    fun (y: int) -> x + y

  let test_local (x: int) : int =
    let fact (x: int) (y: int): int = x + y in
    fact x 42

  let test_lets (x: int) : int =
    let y = x in
    let z = y + 1 in
    let yxz = y * x * z in
    let xzy = x + z + y in
    let res = yxz - xzy in
    res

211
  let test_partial3 (x: int) : int =
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
    let sum : int -> int -> int = fun x y -> x + y in
    let incr_a (a: int) = sum a in
    incr_a x x

  let constr_partial (x: int) : list int =
    let x = Cons 42 in
    x Nil

  let filter_record (c: cursor 'a) : int =
    match c with
    | { collection = l; index = i; index2 = i2; v = v} -> i
    end

  (** for loops *)

  let for_loop1 () =
228
    let r = ref (0: int63) in
229 230 231
    for i = 0 to 10 do r := !r + i done;
    !r

232 233
  (** optional and named arguments *)

234
  use option.Option
235

236
  let opt_f (x [@ocaml:named]: int) (y [@ocaml:named]) = x+y
237
  let constant opt_a = opt_f 40 2
238
  let opt_g (x [@ocaml:optional]) (y [@ocaml:named]: int) =
239 240 241 242
     match x with None -> y | Some x -> x + y end
  let constant opt_c = opt_g (Some 40) 2

  (* FIXME: partial application with named arguments not yet supported *)
243
  let constant opt_b = fun y -> opt_g y 42
244 245 246
  let opt_h () = fun y -> opt_f 40 y
  let opt_i () = opt_h () 2

247 248
  (** test the execution of the extracted code *)

249
  use ocaml.Pervasives
250 251

  let test1 () raises { AssertFailure } =
252
    ocaml_assert ((1:int) + 1 = 2)
253 254 255 256 257 258 259 260 261 262 263 264 265

  (** parallel assignement *)

  type record1 = { mutable field: int }

  let test_parallel_assign () raises { AssertFailure } =
    let a = { field = 0 } in
    let b = { field = 1 } in
    (a.field, b.field) <- (b.field, a.field);
    ocaml_assert (a.field = 1)

  (** machine arithmetic *)

266
  use mach.int.Int63
267 268 269 270 271

  let get_min_int63 (x: int63) : int
  = min_int63

  let test2 () raises { AssertFailure }
272
  = ocaml_assert ((1:int63) + 1 = 2)
273

Mário Pereira's avatar
Mário Pereira committed
274 275
  (* testing proxy-variables inlining mechanism inside a lambda *)
  let test3 () raises { AssertFailure }
276
  = let i = ref (42:int63) in
Mário Pereira's avatar
Mário Pereira committed
277
    let c = Cons !i in
278
    i := 0;
Mário Pereira's avatar
Mário Pereira committed
279
    let c = c Nil in
280
    ocaml_assert (match c with Cons x _ -> x = 42 | _ -> true end)
Mário Pereira's avatar
Mário Pereira committed
281 282 283 284

  (* testing proxy-variables inlining with conflicting effects *)
  let test4 () raises { AssertFailure }
  = let f (x y: int63) raises { AssertFailure }
285
    = ocaml_assert (y = 42);
Mário Pereira's avatar
Mário Pereira committed
286
      x + y in
287 288 289 290
    let i = ref 42 in
    let res = f (i := 0; !i) !i in
    ocaml_assert (!i = 0);
    ocaml_assert (res = 42)
Mário Pereira's avatar
Mário Pereira committed
291

292 293 294
  let main () raises { AssertFailure } =
    test1 ();
    test2 ();
Mário Pereira's avatar
Mário Pereira committed
295 296
    test3 ();
    test4 ();
297
    test_parallel_assign ()
298

299 300 301 302 303 304 305 306 307 308 309 310 311
  (* scopes *)

  type ty = A | B | C

  scope S
    type ty = A | B | C
    (* locally hides toplevel function foo: int -> int *)
    let foo (x: bool) : bool = x
    let test_foo () = foo true
  end

  let test_foo () = foo 42

312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327
  (* range types *)

  type small_range = <range 1 10>

  let test_small_range () =
    for x = 1: small_range to 3 do
      ()
    done

  type big_range = <range 1 0x4000_0000>

  let test_big_range () =
    for x = 1: big_range to 3 do
      ()
    done

328 329 330 331
end

(*
Local Variables:
332
compile-command: "make -C .. test-ocaml-extraction"
333 334
End:
*)