mlw_interp.ml 39 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
MARCHE Claude's avatar
MARCHE Claude committed
5
6
7
8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
MARCHE Claude's avatar
MARCHE Claude committed
10
(********************************************************************)
11

12
open Format
13
14
open Term

15

16
17
18
let debug = Debug.register_info_flag "trace_exec"
  ~desc:"trace execution of code given by --exec or --eval"

19
20
21
(* environment *)

open Mlw_ty
22
23
open Mlw_ty.T
open Mlw_expr
24

25
module Nummap = Map.Make(BigInt)
26

27
type value =
28
  | Vapp of lsymbol * value list
29
  | Vnum of BigInt.t
30
31
32
33
  | Vbool of bool
  | Vvoid
  | Vreg of region
(*
34
  | Varray of Big_int.big_int * value * value Nummap.t
35
              (* length, default, elements *)
36
*)
37
  | Vmap of value * value Nummap.t
38
39
40
41
42
43
44
45
46
              (* default, elements *)
  | Vbin of binop * value * value
  | Veq of value * value
  | Vnot of value
  | Vif of value * term * term
  | Vquant of quant * term_quant
  | Veps of term_bound
  | Vcase of value * term_branch list

47
48
let array_cons_ls = ref ps_equ

49
50
51
let rec print_value fmt v =
  match v with
  | Vnum n ->
52
53
54
55
    if BigInt.ge n BigInt.zero then
      fprintf fmt "%s" (BigInt.to_string n)
    else
      fprintf fmt "(%s)" (BigInt.to_string n)
56
57
  | Vbool b ->
    fprintf fmt "%b" b
58
59
60
  | Vvoid ->
    fprintf fmt "()"
  | Vreg reg -> Mlw_pretty.print_reg fmt reg
61
62
63
64
  | Vmap(def,m) ->
    fprintf fmt "@[[def=%a" print_value def;
    Nummap.iter
      (fun i v ->
65
        fprintf fmt ",@ %s -> %a" (BigInt.to_string i) print_value v)
66
67
68
69
      m;
    fprintf fmt "]@]"
  | Vapp(ls,[Vnum len;Vmap(def,m)]) when ls_equal ls !array_cons_ls ->
    fprintf fmt "@[[";
70
71
    let i = ref BigInt.zero in
    while BigInt.lt !i len do
72
73
74
      let v =
        try Nummap.find !i m
        with Not_found -> def
75
      in
76
      if BigInt.gt !i BigInt.zero
77
78
      then fprintf fmt ",@ ";
      fprintf fmt "%a" print_value v;
79
      i := BigInt.succ !i
80
81
    done;
    fprintf fmt "]@]"
MARCHE Claude's avatar
MARCHE Claude committed
82
83
84
  | Vapp(ls,vl) when is_fs_tuple ls ->
    fprintf fmt "@[(%a)@]"
      (Pp.print_list Pp.comma print_value) vl
85
86
  | Vapp(ls,[]) ->
    fprintf fmt "@[%a@]" Pretty.print_ls ls
87
  | Vapp(ls,vl) ->
88
89
    fprintf fmt "@[(%a %a)@]"
      Pretty.print_ls ls (Pp.print_list Pp.space print_value) vl
90
  | Vbin(op,v1,v2) ->
91
    fprintf fmt "@[(%a %a@ %a)@]"
92
      print_value v1 (Pretty.print_binop ~asym:false) op print_value v2
93
  | Veq(v1,v2) ->
94
95
96
97
    fprintf fmt "@[(%a =@ %a)@]" print_value v1 print_value v2
  | Vnot v ->
    fprintf fmt "@[(not@ %a)@]" print_value v
  | Vif(v,t1,t2) ->
98
    fprintf fmt "@[(if %a@ then %a@ else %a)@]"
99
100
101
102
103
104
      print_value v Pretty.print_term t1 Pretty.print_term t2
  | Vquant(q,tq) ->
    Pretty.print_term fmt (t_quant q tq)
  | Veps(tb) ->
    Pretty.print_term fmt (t_eps tb)
  | Vcase(v,_) ->
105
106
    fprintf fmt "@[match %a@ with ... end@]"
      print_value v
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

let v_eq v1 v2 = Veq(v1,v2)

let v_and v1 v2 =
  match (v1,v2) with
    | Vbool b1, Vbool b2 -> Vbool (b1 && b2)
    | _ -> Vbin(Tand,v1,v2)

let v_or v1 v2 =
  match (v1,v2) with
    | Vbool b1, Vbool b2 -> Vbool (b1 || b2)
    | _ -> Vbin(Tor,v1,v2)

let v_implies v1 v2 =
  match (v1,v2) with
    | Vbool b1, Vbool b2 -> Vbool (not b1 || b2)
    | _ -> Vbin(Timplies,v1,v2)

let v_iff v1 v2 =
  match (v1,v2) with
    | Vbool b1, Vbool b2 -> Vbool (b1 == b2)
    | _ -> Vbin(Tiff,v1,v2)

let v_not v =
  match v with
    | Vbool b -> Vbool (not b)
    | _ -> Vnot(v)

let v_if v t1 t2 = Vif(v,t1,t2)

137
138
139
type env = {
  mknown : Mlw_decl.known_map;
  tknown : Decl.known_map;
140
  funenv : Mlw_expr.fun_defn Mps.t;
141
  regenv : region Mreg.t;
142
  vsenv : value Mvs.t;
143
144
}

145
146
147
148
type state = value Mreg.t

let bind_vs v (t:value) env =
  { env with vsenv = Mvs.add v t env.vsenv }
149
150
151
152
153
154

let multibind_vs l tl env =
  try
    List.fold_right2 bind_vs l tl env
  with Invalid_argument _ -> assert false

155
let bind_pvs pv t env =
156
  { env with vsenv = Mvs.add pv.pv_vs t env.vsenv }
157
158
159
160
161
162
163

let multibind_pvs l tl env =
  try
    List.fold_right2 bind_pvs l tl env
  with Invalid_argument _ -> assert false


164
165
166
167
168
169
170
171
172
let p_regvar fmt (reg,t) =
  fprintf fmt "@[<hov 2><%a> -> %a@]"
    Mlw_pretty.print_reg reg Mlw_pretty.print_reg t

let print_regenv fmt s =
  let l = Mreg.bindings s in
  fprintf fmt "@[<v 0>%a@]" (Pp.print_list Pp.semi p_regvar) l


173
let get_reg env r =
174
  let rec aux n r =
175
    if n > 1000 then
176
177
178
179
180
181
182
183
184
      begin
        eprintf "@[<hov 2>looping region association ??? regenv =@ %a@]@."
          print_regenv env.regenv;
        assert false
      end;
    match Mreg.find_opt r env.regenv with
    | None -> r
    | Some r' -> aux (succ n) r'
  in aux 0 r
185

186
187
188
189
190


(* store *)


MARCHE Claude's avatar
MARCHE Claude committed
191
let p_reg fmt (reg,t) =
MARCHE Claude's avatar
MARCHE Claude committed
192
  fprintf fmt "@[<hov 2><%a> -> %a@]"
193
    Mlw_pretty.print_reg reg print_value t
MARCHE Claude's avatar
MARCHE Claude committed
194
195
196
197

let print_state fmt s =
  let l = Mreg.bindings s in
  fprintf fmt "@[<v 0>%a@]" (Pp.print_list Pp.semi p_reg) l
198

199
let p_vsvar fmt (vs,t) =
200
  fprintf fmt "@[<hov 2>%a -> %a@]"
201
202
203
204
205
    Pretty.print_vs vs print_value t

let print_vsenv fmt s =
  let l = Mvs.bindings s in
  fprintf fmt "@[<v 0>%a@]" (Pp.print_list Pp.semi p_vsvar) l
206
207
208

(* evaluation of terms *)

209
210
exception NoMatch
exception Undetermined
211
exception CannotCompute
212

213
let rec matching env (t:value) p =
214
215
216
217
218
219
220
221
222
223
  match p.pat_node with
  | Pwild -> env
  | Pvar v -> bind_vs v t env
  | Por(p1,p2) ->
    begin
      try matching env t p1
      with NoMatch -> matching env t p2
    end
  | Pas(p,v) -> matching (bind_vs v t env) t p
  | Papp(ls1,pl) ->
224
225
    match t with
      | Vapp(ls2,tl) ->
226
227
228
229
230
231
232
        if ls_equal ls1 ls2 then
          List.fold_left2 matching env tl pl
        else
          if ls2.ls_constr > 0 then raise NoMatch
          else raise Undetermined
      | _ -> raise Undetermined

233
234
235


(* builtin symbols *)
236
237
238

let builtins = Hls.create 17

239
240
241
let ls_minus = ref ps_equ (* temporary *)

exception NotNum
242

243
244
245
246
247
248
249
250
let big_int_of_const c =
  match c with
    | Number.ConstInt i -> Number.compute_int i
    | _ -> raise NotNum

let big_int_of_value v =
  match v with
    | Vnum i -> i
251
    | _ -> raise NotNum
252
253
254
255
256
257

let eval_true _ls _l = Vbool true

let eval_false _ls _l = Vbool false

let eval_int_op op ls l =
258
  match l with
259
  | [Vnum i1;Vnum i2] ->
260
    begin
261
      try Vnum (op i1 i2)
262
      with NotNum | Division_by_zero ->
263
        Vapp(ls,l)
264
    end
265
  | _ -> Vapp(ls,l)
266

267
let eval_int_uop op ls l =
268
  match l with
269
  | [Vnum i1] ->
270
    begin
271
      try Vnum (op i1)
272
      with NotNum ->
273
        Vapp(ls,l)
274
    end
275
  | _ -> Vapp(ls,l)
276

277
let eval_int_rel op ls l =
278
  match l with
279
  | [Vnum i1;Vnum i2] ->
280
    begin
281
      try Vbool (op i1 i2)
282
      with NotNum ->
283
        Vapp(ls,l)
284
    end
285
286
  | _ -> Vapp(ls,l)

287

288
289
290
291
292
let must_be_true b =
  if b then true else raise Undetermined

let rec value_equality v1 v2 =
  match (v1,v2) with
293
    | Vnum i1, Vnum i2 -> BigInt.eq i1 i2
294
295
296
297
    | Vbool b1, Vbool b2 -> b1 == b2
    | Vapp(ls1,vl1), Vapp(ls2,vl2) ->
      must_be_true (ls_equal ls1 ls2 && List.for_all2 value_equality vl1 vl2)
    | Vbin(o1,v11,v12),Vbin(o2,v21,v22) ->
298
       must_be_true (o1 == o2 &&
299
300
301
                       value_equality v11 v21 && value_equality v12 v22)
    | Veq(v11,v12),Veq(v21,v22) ->
      must_be_true (value_equality v11 v21 && value_equality v12 v22)
302
    | Vnot v1, Vnot v2 ->
303
304
305
306
307
308
309
310
311
312
313
314
315
      must_be_true (value_equality v1 v2)
    | Vif(v1,t11,t12),Vif(v2,t21,t22) ->
      must_be_true (value_equality v1 v2 &&
                      t_equal t11 t21 && t_equal t12 t22)
    | Vquant(q1,t1),Vquant(q2,t2) ->
      must_be_true (q1 = q2 && t1 == t2)
    | Veps t1, Veps t2 ->
      must_be_true (t1 == t2)
    | Vcase(v1,b1),Vcase(v2,b2) ->
      must_be_true(value_equality v1 v2 && b1 == b2)
    | _ -> raise Undetermined

let eval_equ _ls l =
MARCHE Claude's avatar
MARCHE Claude committed
316
(*
317
  eprintf "[interp] eval_equ ? @.";
MARCHE Claude's avatar
MARCHE Claude committed
318
319
*)
  let res =
320
321
  match l with
  | [t1;t2] ->
322
    begin
323
324
      try Vbool(value_equality t1 t2)
      with Undetermined -> v_eq t1 t2
325
    end
326
  | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
327
328
329
330
331
332
  in
(*
  Format.eprintf "[interp] eval_equ: OK@.";
*)
  res

333
let eval_now ls l = Vapp(ls,l)
334

335
336
(* functions on map.Map *)

337
338
339
let ts_map = ref Ty.ts_int

let builtin_map_type ts = ts_map := ts
MARCHE Claude's avatar
MARCHE Claude committed
340

341
342
343
344
let ls_map_const = ref ps_equ
let ls_map_get = ref ps_equ
let ls_map_set = ref ps_equ

345
let eval_map_const ls l =
346
  match l with
347
    | [d] -> Vmap(d,Nummap.empty)
348
    | _ -> Vapp(ls,l)
349

350
let eval_map_get ls_get l =
351
  match l with
352
  | [m;x] ->
353
      (* eprintf "Looking for get:"; *)
354
355
356
357
358
359
360
361
    let rec find m =
      match m with
      | Vmap(def,m) ->
        begin
          match x with
          | Vnum i ->
            begin try Nummap.find i m
              with Not_found -> def
362
            end
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
          | _ -> assert false
        end
      | Vapp(ls,[m';y;v]) when ls_equal ls !ls_map_set ->
        begin try
                if value_equality x y then
                  ((* Format.eprintf "ok!@.";*) v)
                else
                  ((* Format.eprintf "recur...@.";*) find m' )
          with Undetermined ->
              (* Format.eprintf "failed.@."; *)
            Vapp(ls_get,[m;x])
        end
      | Vapp(ls,[def]) when ls_equal ls !ls_map_const -> def
      | _ -> Vapp(ls_get,[m;x])
    in find m
  | _ -> assert false
379

380
let eval_map_set ls_set l =
381
  match l with
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
  | [m;x;v] ->
    let rec compress m =
      match m with
      | Vmap(def,m) ->
        begin
          match x with
          | Vnum i -> Vmap(def,Nummap.add i v m)
          | _ -> assert false
        end
      | Vapp(ls,[m';y;v']) when ls_equal ls !ls_map_set ->
        begin try
                if value_equality x y then
                  Vapp(ls_set,[m';x;v])
                else
                  let c = compress m' in
                  Vapp(ls_set,[c;y;v'])
          with Undetermined ->
399
            Vapp(ls_set,[m;x;v])
400
401
402
403
404
        end
      | _ ->
        Vapp(ls_set,[m;x;v])
    in compress m
  | _ -> assert false
405
406
407

(* all builtin functions *)

408
let built_in_theories =
409
  [ ["bool"],"Bool", [],
410
411
    [ "True", None, eval_true ;
      "False", None, eval_false ;
412
413
    ] ;
    ["int"],"Int", [],
414
415
416
417
418
419
420
421
    [ "infix +", None, eval_int_op BigInt.add;
      "infix -", None, eval_int_op BigInt.sub;
      "infix *", None, eval_int_op BigInt.mul;
      "prefix -", Some ls_minus, eval_int_uop BigInt.minus;
      "infix <", None, eval_int_rel BigInt.lt;
      "infix <=", None, eval_int_rel BigInt.le;
      "infix >", None, eval_int_rel BigInt.gt;
      "infix >=", None, eval_int_rel BigInt.ge;
422
    ] ;
423
    ["int"],"MinMax", [],
424
425
    [ "min", None, eval_int_op BigInt.min;
      "max", None, eval_int_op BigInt.max;
426
    ] ;
427
    ["int"],"ComputerDivision", [],
428
429
    [ "div", None, eval_int_op BigInt.computer_div;
      "mod", None, eval_int_op BigInt.computer_mod;
430
    ] ;
431
    ["int"],"EuclideanDivision", [],
432
433
    [ "div", None, eval_int_op BigInt.euclidean_div;
      "mod", None, eval_int_op BigInt.euclidean_mod;
434
    ] ;
435
    ["map"],"Map", ["map", builtin_map_type],
436
437
438
    [ "const", Some ls_map_const, eval_map_const;
      "get", Some ls_map_get, eval_map_get;
      "set", Some ls_map_set, eval_map_set;
439
    ] ;
440
441
  ]

442
let add_builtin_th env (l,n,t,d) =
443
444
445
446
447
448
449
450
451
452
453
454
455
456
  let th = Env.read_theory env l n in
  List.iter
    (fun (id,r) ->
      let ts = Theory.ns_find_ts th.Theory.th_export [id] in
      r ts)
    t;
  List.iter
    (fun (id,r,f) ->
      let ls = Theory.ns_find_ls th.Theory.th_export [id] in
      Hls.add builtins ls f;
      match r with
        | None -> ()
        | Some r -> r := ls)
    d
457
458
459

let get_builtins env =
  Hls.add builtins ps_equ eval_equ;
MARCHE Claude's avatar
MARCHE Claude committed
460
  Hls.add builtins Mlw_wp.fs_now eval_now;
461
462
  List.iter (add_builtin_th env) built_in_theories

463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
(* promotes logic value v of program type ty into a program value,
   e.g if

     type t = { mutable a : int; c: int ; mutable b : int }

   then

     to_value (mk_t 1 43 2 : t <r1,r2>) =
        Vapp(mk_t,[Vreg r1,Vnum 43, Vreg r2])

   with new regions in s

     <r1> -> Vnum 1
     <r2> -> Vnum 2

*)
479

480
(*
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
let rec to_program_value_rec env regions s ity ls vl =
  try
    let csl = Mlw_decl.inst_constructors env.tknown env.mknown ity in
    let rec find_cs csl =
      match csl with
      | [] -> assert false (* FIXME ? *)
      | (cs,fdl)::rem ->
        if ls_equal cs ls then
              (* we found the fields of that constructor *)
          begin
            let (s,regions,vl) =
              List.fold_left2
                (fun (s,regions,vl) fd v ->
                  match fd.fd_mut,regions with
                  | None,_ -> (* non mutable field, but
                                 some subfield may be mutable *)
                    begin
                      match v with
                      | Vapp(ls1,vl1) ->
                        let s, regions, v =
                          to_program_value_rec env regions s fd.fd_ity ls1 vl1
                        in
                        (s,regions,v::vl)
                      | _ -> (s,regions,v::vl)
                    end
                  | Some _r, reg::regions ->
                        (* found a mutable field *)
                    let s' = Mreg.add reg v s in
                    (s',regions,Vreg reg :: vl)
                  | Some _, [] -> assert false)
                (s,regions,[]) fdl vl
            in
            s,regions,Vapp(ls,List.rev vl)
          end
        else find_cs rem
    in find_cs csl
  with Not_found ->
        (* absurd, it would be a pure type *)
    assert false

MARCHE Claude's avatar
MARCHE Claude committed
521
522
523
let rec get_regions acc ity =
  match ity.ity_node with
  | Ityvar _ -> assert false
524
  | Ityapp(its,tl,rl) ->
MARCHE Claude's avatar
MARCHE Claude committed
525
526
     List.map (get_reg env) rl
  | Itypur(ts,tl) ->
527
    *)
MARCHE Claude's avatar
MARCHE Claude committed
528

529
530
531
532
533
534
535
536
537
538
539
540
let find_fields env ity ls =
  try
    let csl = Mlw_decl.inst_constructors env.tknown env.mknown ity in
    let rec find_cs csl =
      match csl with
      | [] -> assert false (* FIXME ? *)
      | (cs,fdl)::rem ->
        if ls_equal cs ls then fdl else find_cs rem
    in find_cs csl
  with Not_found ->
    (* absurd, [ity] would be a pure type *)
    assert false
MARCHE Claude's avatar
MARCHE Claude committed
541

542
543
544
545
546
let rec remove_prefix l r =
  match l,r with
  | _,[] -> l
  | [],_ -> assert false
  | r1::l,r2::r -> assert (r1 == r2); remove_prefix l r
547
548
549
550

let rec to_program_value env s ity v =
  match v with
  | Vapp(ls,vl) ->
551
    if ity_immutable ity then [],s,v else
552
      begin
553
554
        let fdl = find_fields env ity ls in
        let targs,regions =
555
          match ity.ity_node with
556
          | Ityapp(_,tl,rl) -> tl, List.map (get_reg env) rl
MARCHE Claude's avatar
MARCHE Claude committed
557
          | Ityvar _ -> assert false
558
          | Itypur(_,tl) -> tl, []
559
        in
560
561
        let s,v = to_program_value_list env s targs fdl regions ls vl in
        regions, s, v
562
      end
563
  | _ -> assert (ity_immutable ity); [], s,v
564
565
566
567
568
569
570
571

and to_program_value_list env s _tl fdl regions ls vl =
  let (s,regions,vl) =
    List.fold_left2
      (fun (s,regions,vl) fd v ->
        match fd.fd_mut,regions with
        | None,_ -> (* non mutable field, but
                       some subfield may be mutable *)
572
573
574
575
576
577
578
           let regs, s, v = to_program_value env s fd.fd_ity v in
           let rem_regs =
             match regions with
             | [] -> []
             | _ -> remove_prefix regions regs
           in
           (s,rem_regs,v::vl)
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
        | Some _r, reg::regions ->
          (* found a mutable field *)
          let s' = Mreg.add reg v s in
          (s',regions,Vreg reg :: vl)
        | Some _, [] -> assert false)
      (s,regions,[]) fdl vl
  in
  match regions with
  | [] -> s, Vapp(ls,List.rev vl)
  | _ ->
    eprintf "@[<hov 2>error while converting logic value (%a) \
              to a program value:@ regions should be empty, not@ [%a]@]@."
      print_value (Vapp(ls,vl))
      (Pp.print_list Pp.comma Mlw_pretty.print_reg) regions;
    assert false

595

596
597
598
599
600
let to_program_value env s ty v =
  match ty with
  | VTarrow _ -> s,v
  | VTvalue ity ->
    if ity_immutable ity then s,v else
601
602
      let _regs,s,v = to_program_value env s ity v in
      s,v
603
604
605
606
607
608

let rec any_value_of_type env ty =
  match ty.Ty.ty_node with
  | Ty.Tyvar _ -> assert false
  | Ty.Tyapp(ts,_) when Ty.ts_equal ts Ty.ts_int ->
    let n = Random.int 199 - 99 in
609
    Vnum (BigInt.of_int n)
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
  | Ty.Tyapp(ts,_) when Ty.ts_equal ts Ty.ts_real ->
    Vvoid (* FIXME *)
  | Ty.Tyapp(ts,_) when Ty.ts_equal ts Ty.ts_bool ->
    Vbool(Random.bool ())
  | Ty.Tyapp(ts,_tyl) when Ty.is_ts_tuple ts ->
    Vvoid (* FIXME *)
  | Ty.Tyapp(ts,tyargs) ->
    try
      let csl = Decl.find_constructors env.tknown ts in
      match csl with
      | [] -> Vvoid (* FIXME *)
      | [cs,_] ->
        let ts_args = ts.Ty.ts_args in
        let subst = List.fold_left2
          (fun acc v t -> Ty.Mtv.add v t acc) Ty.Mtv.empty ts_args tyargs
        in
        let tyl = List.map (Ty.ty_inst subst) cs.ls_args in
        let vl = List.map (any_value_of_type env) tyl in
        Vapp(cs,vl)
      | (cs,_)::_rem -> (* FIXME *)
        let tyl = cs.ls_args in
        let vl = List.map (any_value_of_type env) tyl in
        Vapp(cs,vl)
    with Not_found -> Vvoid (* FIXME *)

635
type result =
636
637
  | Normal of value
  | Excep of xsymbol * value
638
639
640
641
642
643
644
645
646
647
648
  | Irred of expr
  | Fun of psymbol * pvsymbol list * int

let builtin_progs = Hps.create 17

let builtin_array_type kn its =
  let csl = Mlw_decl.find_constructors kn its in
  match csl with
    | [(pls,_)] -> array_cons_ls := pls.pl_ls
    | _ ->  assert false

649
let exec_array_make env s vty args =
650
  match args with
651
    | [Vnum n;def] ->
652
      let m = Vmap(def,Nummap.empty) in
653
654
655
      let v = Vapp(!array_cons_ls,[Vnum n;m]) in
      let s',v' = to_program_value env s vty v in
      Normal v',s'
656
657
    | _ ->
      raise CannotCompute
658

659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
let exec_array_copy env s vty args =
  match args with
    | [Vapp(ls,[len;m])] when ls_equal ls !array_cons_ls ->
      begin
        match m with
          | Vreg r ->
            let m = Mreg.find r s in
            let v = Vapp(!array_cons_ls,[len;m]) in
            let s',v' = to_program_value env s vty v in
            Normal v',s'
          | _ -> raise CannotCompute
      end
    | _ ->
      raise CannotCompute

674
let exec_array_get _env s _vty args =
MARCHE Claude's avatar
MARCHE Claude committed
675
  match args with
676
    | [t;Vnum i] ->
MARCHE Claude's avatar
MARCHE Claude committed
677
      begin
678
679
        match t with
          | Vapp(ls,[_len;m]) when ls_equal ls !array_cons_ls ->
680
681
682
683
684
685
686
687
688
689
690
            begin
              match m with
              | Vreg r ->
                let m = Mreg.find r s in
                let t = eval_map_get !ls_map_get [m;Vnum i] in
(*
                eprintf
                  "[interp] exec_array_get (on reg %a)@ state =@ %a@ t[%a] -> %a@."
                  Mlw_pretty.print_reg r print_state s print_value (Vnum i) print_value t;
*)
                Normal t,s
691
              | _ -> raise CannotCompute
692
693
694
695
696
697
698
699
(*
                let t = eval_map_get !ls_map_get [m;Vnum i] in
                eprintf
                  "[interp] exec_array_get (on map %a)@ state =@ %a@ t[%a] -> %a@."
                  print_value m print_state s print_value (Vnum i) print_value t;
                Normal t,s
*)
            end
700
          | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
701
      end
702
    | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
703

704
let exec_array_length _env s _vty args =
MARCHE Claude's avatar
MARCHE Claude committed
705
706
707
  match args with
    | [t] ->
      begin
708
709
        match t with
          | Vapp(ls,[len;_m]) when ls_equal ls !array_cons_ls ->
MARCHE Claude's avatar
MARCHE Claude committed
710
            Normal len,s
711
          | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
712
      end
713
    | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
714

715
let exec_array_set _env s _vty args =
MARCHE Claude's avatar
MARCHE Claude committed
716
717
718
  match args with
    | [t;i;v] ->
      begin
719
720
        match t with
          | Vapp(ls,[_len;m]) when ls_equal ls !array_cons_ls ->
721
722
723
724
725
726
727
728
729
730
731
732
733
            begin
              match m with
              | Vreg r ->
                let m = Mreg.find r s in
(*
                eprintf
                  "[interp] exec_array_set (on reg %a)@ state =@ %a@ t[%a] -> %a@."
                  Mlw_pretty.print_reg r print_state s print_value i print_value t;
*)
                let t = eval_map_set !ls_map_set [m;i;v] in
                let s' =  Mreg.add r t s in
                Normal Vvoid,s'
(*
MARCHE Claude's avatar
MARCHE Claude committed
734
735
736
737
738
739
740
741
742
743
            let effs = spec.c_effect.eff_writes in
            let reg =
              if Sreg.cardinal effs = 1 then Sreg.choose effs
              else assert false
            in
            let reg =
              try Mreg.find reg env.regenv
              with Not_found -> reg
            in
            let s' = Mreg.add reg t s in
744
745
            eprintf "[interp] t[%a] <- %a (state = %a)@."
              print_value i print_value v print_state s';
746
            Normal Vvoid,s'
747
*)
748
              | _ -> raise CannotCompute
749
            end
750
          | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
751
752
753
      end
    | _ -> assert false

754
let built_in_modules =
755
  [
756
   ["array"],"Array",
757
    ["array", builtin_array_type],
MARCHE Claude's avatar
MARCHE Claude committed
758
759
    ["make", None, exec_array_make ;
     "mixfix []", None, exec_array_get ;
MARCHE Claude's avatar
MARCHE Claude committed
760
761
     "length", None, exec_array_length ;
     "mixfix []<-", None, exec_array_set ;
762
     "copy", None, exec_array_copy ;
MARCHE Claude's avatar
MARCHE Claude committed
763
    ] ;
764
765
  ]

766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
let add_builtin_mo env (l,n,t,d) =
  let mo = Mlw_module.read_module env l n in
  let exp = mo.Mlw_module.mod_export in
  let kn = mo.Mlw_module.mod_known in
  List.iter
    (fun (id,r) ->
      let its = Mlw_module.ns_find_its exp [id] in
      r kn its)
    t;
  List.iter
    (fun (id,r,f) ->
      let ps = Mlw_module.ns_find_ps exp [id] in
      Hps.add builtin_progs ps f;
      match r with
        | None -> ()
        | Some r -> r := ps)
    d
783
784
785
786

let get_builtin_progs lib =
  List.iter (add_builtin_mo lib) built_in_modules

787
let get_vs env vs =
788
  try
789
    let t = Mvs.find vs env.vsenv in t
790
791
  with Not_found ->
    eprintf "logic variable %s not found in env@." vs.vs_name.Ident.id_string;
792
    assert false
793

794
795
let get_pvs env pvs =
  let t =
796
797
798
799
800
    try
      Mvs.find pvs.pv_vs env.vsenv
  with Not_found ->
    eprintf "program variable %s not found in env@."
      pvs.pv_vs.vs_name.Ident.id_string;
801
    assert false
802
  in
803
  t
804

805
806
807
let rec to_logic_value env s v =
  let eval_rec t = to_logic_value env s t in
  match v with
808
  | Vreg r -> Mreg.find (get_reg env r) s
809
  | Vnum _ | Vbool _ | Vvoid | Vmap _ -> v
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
  | Vbin(Tand,t1,t2) ->
    v_and (eval_rec t1) (eval_rec t2)
  | Vbin(Tor,t1,t2) ->
    v_or (eval_rec t1) (eval_rec t2)
  | Vbin(Timplies,t1,t2) ->
    v_implies (eval_rec t1) (eval_rec t2)
  | Vbin(Tiff,t1,t2) ->
    v_iff (eval_rec t1) (eval_rec t2)
  | Vnot t1 -> v_not (eval_rec t1)
  | Vapp(ls,tl) ->
    eval_app env s ls (List.map eval_rec tl)
  | Veq (v1, v2) -> eval_equ ps_equ [v1;v2]
  | Vif(t1,t2,t3) ->
    let u = eval_rec t1 in
    begin match u with
    | Vbool true -> eval_term env s t2
    | Vbool false -> eval_term env s t3
    | _ -> v_if u t2 t3
    end
  | Vcase(t1,tbl) ->
(*
    eprintf "found a match ... with ...@.";
*)
    let u = eval_rec t1 in
    eval_match env s u tbl
  | Vquant(q,t) -> Vquant(q,t)
  | Veps t -> Veps t

and eval_term env s t =
839
  let eval_rec t = eval_term env s t in
840
841
  match t.t_node with
  | Tvar x ->
842
    begin
843
844
845
      try
        to_logic_value env s (get_vs env x)
      with Not_found -> assert false
846
847
    end
  | Tbinop(Tand,t1,t2) ->
848
    v_and (eval_rec t1) (eval_rec t2)
849
  | Tbinop(Tor,t1,t2) ->
850
    v_or (eval_rec t1) (eval_rec t2)
851
  | Tbinop(Timplies,t1,t2) ->
852
    v_implies (eval_rec t1) (eval_rec t2)
853
  | Tbinop(Tiff,t1,t2) ->
854
855
    v_iff (eval_rec t1) (eval_rec t2)
  | Tnot t1 -> v_not (eval_rec t1)
856
  | Tapp(ls,tl) ->
857
    eval_app env s ls (List.map eval_rec tl)
858
  | Tif(t1,t2,t3) ->
859
    let u = eval_rec t1 in
860
861
862
863
    begin match u with
    | Vbool true -> eval_term env s t2
    | Vbool false -> eval_term env s t3
    | _ -> v_if u t2 t3
864
    end
865
  | Tlet(t1,tb) ->
866
    let u = eval_rec t1 in
867
    let v,t2 = t_open_bound tb in
868
    eval_term (bind_vs v u env) s t2
869
  | Tcase(t1,tbl) ->
870
(*
871
    eprintf "found a match ... with ...@.";
872
*)
873
    let u = eval_rec t1 in
874
875
876
    eval_match env s u tbl
  | Tquant(q,t) -> Vquant(q,t)
  | Teps t -> Veps t
877
  | Tconst n -> Vnum (big_int_of_const n)
878
879
  | Ttrue -> Vbool true
  | Tfalse -> Vbool false
MARCHE Claude's avatar
MARCHE Claude committed
880
881
882
883
884





885
and eval_match env s u tbl =
886
887
888
  let rec iter tbl =
    match tbl with
    | [] ->
889
      eprintf "[Exec] fatal error: pattern matching not exhaustive in evaluation.@.";
890
      assert false
891
892
893
894
    | b::rem ->
      let p,t = t_open_branch b in
      try
        let env' = matching env u p in
895
        eval_term env' s t
896
897
      with NoMatch -> iter rem
  in
898
  try iter tbl with Undetermined ->
899
    Vcase(u,tbl)
900

901
and eval_app env s ls tl =
902
903
  try
    let f = Hls.find builtins ls in
904
    f ls tl
905
  with Not_found ->
906
907
908
909
910
911
912
913
914
    try
      let d = Ident.Mid.find ls.ls_name env.tknown in
      match d.Decl.d_node with
      | Decl.Dtype _ | Decl.Dprop _ -> assert false
      | Decl.Dlogic dl ->
        (* regular definition *)
        let d = List.assq ls dl in
        let l,t = Decl.open_ls_defn d in
        let env' = multibind_vs l tl env in
915
        eval_term env' s t
916
      | Decl.Dparam _ | Decl.Dind _ ->
917
        Vapp(ls,tl)
918
      | Decl.Ddata dl ->
919
        (* constructor or projection *)
920
        match tl with
921
        | [ Vapp(ls1,tl1) ] ->
922
923
          (* if ls is a projection and ls1 is a constructor,
             we should compute that projection *)
924
925
          let rec iter dl =
            match dl with
926
            | [] -> Vapp(ls,tl)
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
            | (_,csl) :: rem ->
              let rec iter2 csl =
                match csl with
                | [] -> iter rem
                | (cs,prs) :: rem2 ->
                  if ls_equal cs ls1
                  then
                    (* we found the right constructor *)
                    let rec iter3 prs tl1 =
                      match prs,tl1 with
                      | (Some pr)::prs, t::tl1 ->
                        if ls_equal ls pr
                        then (* projection found! *) t
                        else
                          iter3 prs tl1
                      | None::prs, _::tl1 ->
                        iter3 prs tl1
944
                      | _ -> Vapp(ls,tl)
945
946
947
948
                    in iter3 prs tl1
                  else iter2 rem2
              in iter2 csl
          in iter dl
949
        | _ -> Vapp(ls,tl)
950
951
952
    with Not_found ->
      Format.eprintf "[Exec] definition of logic symbol %s not found@."
        ls.ls_name.Ident.id_string;
953
      Vapp(ls,tl)
954

955
956
957
958
959
let to_logic_result env st res =
  match res with
    | Normal v -> Normal(to_logic_value env st v)
    | Excep(e,v) -> Excep(e,to_logic_value env st v)
    | Irred _ | Fun _ -> res
960

961
let eval_global_term env km t =
962
  get_builtins env;
963
964
965
  let env =
    { mknown = Ident.Mid.empty;
      tknown = km;
966
      funenv = Mps.empty;
967
      regenv = Mreg.empty;
968
969
970
      vsenv = Mvs.empty;
    }
  in
971
  eval_term env Mreg.empty t
972
973


974
(* explicit printing of expr *)
975

976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
let p_pvs fmt pvs =
  fprintf fmt "@[{ pv_vs =@ %a;@ pv_ity =@ %a;@ pv_ghost =@ %B }@]"
    Pretty.print_vs pvs.pv_vs Mlw_pretty.print_ity pvs.pv_ity
    pvs.pv_ghost

let p_ps fmt ps =
  fprintf fmt "@[{ ps_name =@ %s;@ ... }@]"
    ps.ps_name.Ident.id_string

let p_pls fmt pls =
  fprintf fmt "@[{ pl_ls =@ %s;@ ... }@]"
    pls.pl_ls.ls_name.Ident.id_string

let p_letsym fmt lsym =
  match lsym with
    | LetV pvs -> fprintf fmt "@[LetV(%a)@]" p_pvs pvs
    | LetA _ -> fprintf fmt "@[LetA(_)@]"

let rec p_let fmt ld =
  fprintf fmt "@[{ let_sym =@ %a;@ let_expr =@ %a }@]"
    p_letsym ld.let_sym p_expr ld.let_expr
997

998
999
and p_expr fmt e =
  match e.e_node with
1000
1001
1002
1003
    | Elogic t ->
      fprintf fmt "@[Elogic{type=%a}(%a)@]"
        Mlw_pretty.print_vty e.e_vty
        Pretty.print_term t
1004
1005
    | Evalue pvs -> fprintf fmt "@[Evalue(%a)@]" p_pvs pvs
    | Earrow ps -> fprintf fmt "@[Earrow(%a)@]" p_ps ps
1006
    | Eapp (e1, pvs, _) ->
1007
      fprintf fmt "@[Eapp(%a,@ %a,@ <spec>)@]" p_expr e1 p_pvs pvs
1008
    | Elet(ldefn,e1) ->
1009
1010
1011
1012
      fprintf fmt "@[Elet(%a,@ %a)@]" p_let ldefn p_expr e1
    | Erec (_, _) -> fprintf fmt "@[Erec(_,@ _,@ _)@]"
    | Eif (_, _, _) -> fprintf fmt "@[Eif(_,@ _,@ _)@]"
    | Ecase (_, _) -> fprintf fmt "@[Ecase(_,@ _)@]"
1013
    | Eassign (pls, e1, reg, pvs) ->
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
      fprintf fmt "@[Eassign(%a,@ %a,@ %a,@ %a)@]"
        p_pls pls p_expr e1 Mlw_pretty.print_reg reg p_pvs pvs
    | Eghost _ -> fprintf fmt "@[Eghost(_)@]"
    | Eany _ -> fprintf fmt "@[Eany(_)@]"
    | Eloop (_, _, _) -> fprintf fmt "@[Eloop(_,@ _,@ _)@]"
    | Efor (_, _, _, _) -> fprintf fmt "@[Efor(_,@ _,@ _,@ _)@]"
    | Eraise (_, _) -> fprintf fmt "@[Eraise(_,@ _)@]"
    | Etry (_, _) -> fprintf fmt "@[Etry(_,@ _)@]"
    | Eabstr (_, _) -> fprintf fmt "@[Eabstr(_,@ _)@]"
    | Eassert (_, _) -> fprintf fmt "@[Eassert(_,@ _)@]"
    | Eabsurd -> fprintf fmt "@[Eabsurd@]"

1026

1027
let print_logic_result fmt r =
1028
  match r with
1029
    | Normal v ->
1030
      fprintf fmt "@[%a@]" print_value v
1031
    | Excep(x,v) ->
1032
      fprintf fmt "@[exception %s(@[%a@])@]"
1033
        x.xs_name.Ident.id_string print_value v
1034
    | Irred e ->
1035
      fprintf fmt "@[Cannot execute expression@ @[%a@]@]"
1036
        Mlw_pretty.print_expr (* p_expr *) e
1037
    | Fun _ ->
1038
      fprintf fmt "@[Result is a function@]"
1039

1040
1041
1042
1043
1044
let print_result env s fmt r =
  print_logic_result fmt (to_logic_result env s r)

(*
let print_result env s fmt r =
1045
1046
1047
1048
1049
1050
1051
1052
  let env = {
    mknown = mkm;
    tknown = tkm;
    regenv = Mreg.empty;
    vsenv = Mvs.empty;
  }
  in
  print_result_aux env s fmt r
1053
*)
1054

1055

1056

1057
1058
(* evaluation of WhyML expressions *)

1059
1060
1061
1062
1063
let find_definition env ps =
  try
    Some (Mps.find ps env.funenv)
  with
      Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
1064
        Mlw_decl.find_definition env.mknown ps
1065
1066
1067


(* evaluate expressions *)
MARCHE Claude's avatar
MARCHE Claude committed
1068
let rec eval_expr env (s:state) (e : expr) : result * state =
1069
  match e.e_node with
1070
  | Elogic t ->
1071
1072
1073
1074
(*
    eprintf "@[<hov 2>[interp]before@ @[%a@]:@ vsenv =@ %a@ regenv=@ %a@ state=@ %a@]@."
      p_expr e print_vsenv env.vsenv print_regenv env.regenv print_state s;
*)
1075
    let v = eval_term env s t in
1076
    let s',v' = to_program_value env s e.e_vty v in
1077
(*
1078
1079
    eprintf "@[<hov 2>[interp]after@ @[%a@]: state=@ %a@]@."
      p_expr e print_state s';
1080
*)
1081
    Normal v', s'
1082
  | Evalue pvs ->
MARCHE Claude's avatar
MARCHE Claude committed
1083
    begin
1084
      try
1085
        let t = get_pvs env pvs in (Normal t),s
1086
      with Not_found -> assert false (* Irred e, s *)
MARCHE Claude's avatar
MARCHE Claude committed
1087
    end
1088
  | Elet(ld,e1) ->