mlw_interp.ml 39.3 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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
let array_cons_ls = ref ps_equ
48
49
let ls_true = ref ps_equ
let ls_false = ref ps_equ
50

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

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)

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

147
148
149
150
type state = value Mreg.t

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

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

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

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


166
167
168
169
170
171
172
173
174
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


175
let get_reg env r =
176
  let rec aux n r =
177
    if n > 1000 then
178
179
180
181
182
183
184
185
186
      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
187

188
189
190
191
192


(* store *)


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

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

201
let p_vsvar fmt (vs,t) =
202
  fprintf fmt "@[<hov 2>%a -> %a@]"
203
204
205
206
207
    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
208
209
210

(* evaluation of terms *)

211
212
exception NoMatch
exception Undetermined
213
exception CannotCompute
214

215
let rec matching env (t:value) p =
216
217
218
219
220
221
222
223
224
225
  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) ->
226
227
    match t with
      | Vapp(ls2,tl) ->
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
233
234
235
      | Vbool b ->
         let l = if b then !ls_true else !ls_false in
         if ls_equal ls1 l then env else raise NoMatch
236
237
      | _ -> raise Undetermined

238
239
240


(* builtin symbols *)
241
242
243

let builtins = Hls.create 17

244
245
246
let ls_minus = ref ps_equ (* temporary *)

exception NotNum
247

248
249
250
251
252
253
254
255
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
256
    | _ -> raise NotNum
257
258
259
260
261
262

let eval_true _ls _l = Vbool true

let eval_false _ls _l = Vbool false

let eval_int_op op ls l =
263
  match l with
264
  | [Vnum i1;Vnum i2] ->
265
    begin
266
      try Vnum (op i1 i2)
267
      with NotNum | Division_by_zero ->
268
        Vapp(ls,l)
269
    end
270
  | _ -> Vapp(ls,l)
271

272
let eval_int_uop op ls l =
273
  match l with
274
  | [Vnum i1] ->
275
    begin
276
      try Vnum (op i1)
277
      with NotNum ->
278
        Vapp(ls,l)
279
    end
280
  | _ -> Vapp(ls,l)
281

282
let eval_int_rel op ls l =
283
  match l with
284
  | [Vnum i1;Vnum i2] ->
285
    begin
286
      try Vbool (op i1 i2)
287
      with NotNum ->
288
        Vapp(ls,l)
289
    end
290
291
  | _ -> Vapp(ls,l)

292

293
294
295
296
297
let must_be_true b =
  if b then true else raise Undetermined

let rec value_equality v1 v2 =
  match (v1,v2) with
298
    | Vnum i1, Vnum i2 -> BigInt.eq i1 i2
299
300
301
302
    | 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) ->
303
       must_be_true (o1 == o2 &&
304
305
306
                       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)
307
    | Vnot v1, Vnot v2 ->
308
309
310
311
312
313
314
315
316
317
318
319
320
      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
321
(*
322
  eprintf "[interp] eval_equ ? @.";
MARCHE Claude's avatar
MARCHE Claude committed
323
324
*)
  let res =
325
326
  match l with
  | [t1;t2] ->
327
    begin
328
329
      try Vbool(value_equality t1 t2)
      with Undetermined -> v_eq t1 t2
330
    end
331
  | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
332
333
334
335
336
337
  in
(*
  Format.eprintf "[interp] eval_equ: OK@.";
*)
  res

338
let eval_now ls l = Vapp(ls,l)
339

340
341
(* functions on map.Map *)

342
343
344
let ts_map = ref Ty.ts_int

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

346
347
348
349
let ls_map_const = ref ps_equ
let ls_map_get = ref ps_equ
let ls_map_set = ref ps_equ

350
let eval_map_const ls l =
351
  match l with
352
    | [d] -> Vmap(d,Nummap.empty)
353
    | _ -> Vapp(ls,l)
354

355
let eval_map_get ls_get l =
356
  match l with
357
  | [m;x] ->
358
      (* eprintf "Looking for get:"; *)
359
360
361
362
363
364
365
366
    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
367
            end
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
          | _ -> 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
384

385
let eval_map_set ls_set l =
386
  match l with
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
  | [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 ->
404
            Vapp(ls_set,[m;x;v])
405
406
407
408
409
        end
      | _ ->
        Vapp(ls_set,[m;x;v])
    in compress m
  | _ -> assert false
410
411
412

(* all builtin functions *)

413
let built_in_theories =
414
  [ ["bool"],"Bool", [],
415
416
    [ "True", Some ls_true, eval_true ;
      "False", Some ls_false, eval_false ;
417
418
    ] ;
    ["int"],"Int", [],
419
420
421
422
423
424
425
426
    [ "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;
427
    ] ;
428
    ["int"],"MinMax", [],
429
430
    [ "min", None, eval_int_op BigInt.min;
      "max", None, eval_int_op BigInt.max;
431
    ] ;
432
    ["int"],"ComputerDivision", [],
433
434
    [ "div", None, eval_int_op BigInt.computer_div;
      "mod", None, eval_int_op BigInt.computer_mod;
435
    ] ;
436
    ["int"],"EuclideanDivision", [],
437
438
    [ "div", None, eval_int_op BigInt.euclidean_div;
      "mod", None, eval_int_op BigInt.euclidean_mod;
439
    ] ;
440
    ["map"],"Map", ["map", builtin_map_type],
MARCHE Claude's avatar
MARCHE Claude committed
441
    [ "get", Some ls_map_get, eval_map_get;
442
      "set", Some ls_map_set, eval_map_set;
443
    ] ;
MARCHE Claude's avatar
MARCHE Claude committed
444
445
    ["map"],"Const", [],
    [ "const", Some ls_map_const, eval_map_const ] ;
446
447
  ]

448
let add_builtin_th env (l,n,t,d) =
449
450
451
452
453
454
455
456
457
458
459
460
461
462
  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
463
464
465

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

469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
(* 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

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

535
536
537
538
539
540
541
542
543
544
545
546
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
547

548
549
550
551
552
let rec remove_prefix l r =
  match l,r with
  | _,[] -> l
  | [],_ -> assert false
  | r1::l,r2::r -> assert (r1 == r2); remove_prefix l r
553
554
555
556

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

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 *)
578
579
580
581
582
583
584
           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)
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
        | 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

601

602
603
604
605
606
let to_program_value env s ty v =
  match ty with
  | VTarrow _ -> s,v
  | VTvalue ity ->
    if ity_immutable ity then s,v else
607
608
      let _regs,s,v = to_program_value env s ity v in
      s,v
609
610
611
612
613
614

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
615
    Vnum (BigInt.of_int n)
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
  | 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 *)

641
type result =
642
643
  | Normal of value
  | Excep of xsymbol * value
644
645
646
647
648
649
650
651
652
653
654
  | 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

655
let exec_array_make env s vty args =
656
  match args with
657
    | [Vnum n;def] ->
658
      let m = Vmap(def,Nummap.empty) in
659
660
661
      let v = Vapp(!array_cons_ls,[Vnum n;m]) in
      let s',v' = to_program_value env s vty v in
      Normal v',s'
662
663
    | _ ->
      raise CannotCompute
664

665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
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

680
let exec_array_get _env s _vty args =
MARCHE Claude's avatar
MARCHE Claude committed
681
  match args with
682
    | [t;Vnum i] ->
MARCHE Claude's avatar
MARCHE Claude committed
683
      begin
684
685
        match t with
          | Vapp(ls,[_len;m]) when ls_equal ls !array_cons_ls ->
686
687
688
689
690
691
692
693
694
695
696
            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
697
              | _ -> raise CannotCompute
698
699
700
701
702
703
704
705
(*
                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
706
          | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
707
      end
708
    | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
709

710
let exec_array_length _env s _vty args =
MARCHE Claude's avatar
MARCHE Claude committed
711
712
713
  match args with
    | [t] ->
      begin
714
715
        match t with
          | Vapp(ls,[len;_m]) when ls_equal ls !array_cons_ls ->
MARCHE Claude's avatar
MARCHE Claude committed
716
            Normal len,s
717
          | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
718
      end
719
    | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
720

721
let exec_array_set _env s _vty args =
MARCHE Claude's avatar
MARCHE Claude committed
722
723
724
  match args with
    | [t;i;v] ->
      begin
725
726
        match t with
          | Vapp(ls,[_len;m]) when ls_equal ls !array_cons_ls ->
727
728
729
730
731
732
733
734
735
736
737
738
739
            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
740
741
742
743
744
745
746
747
748
749
            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
750
751
            eprintf "[interp] t[%a] <- %a (state = %a)@."
              print_value i print_value v print_state s';
752
            Normal Vvoid,s'
753
*)
754
              | _ -> raise CannotCompute
755
            end
756
          | _ -> raise CannotCompute
MARCHE Claude's avatar
MARCHE Claude committed
757
758
759
      end
    | _ -> assert false

760
let built_in_modules =
761
  [
762
   ["array"],"Array",
763
    ["array", builtin_array_type],
MARCHE Claude's avatar
MARCHE Claude committed
764
765
    ["make", None, exec_array_make ;
     "mixfix []", None, exec_array_get ;
MARCHE Claude's avatar
MARCHE Claude committed
766
767
     "length", None, exec_array_length ;
     "mixfix []<-", None, exec_array_set ;
768
     "copy", None, exec_array_copy ;
MARCHE Claude's avatar
MARCHE Claude committed
769
    ] ;
770
771
  ]

772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
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
789
790
791
792

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

793
let get_vs env vs =
794
  try
795
    let t = Mvs.find vs env.vsenv in t
796
797
  with Not_found ->
    eprintf "logic variable %s not found in env@." vs.vs_name.Ident.id_string;
798
    assert false
799

800
801
let get_pvs env pvs =
  let t =
802
803
804
805
806
    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;
807
    assert false
808
  in
809
  t
810

811
812
813
let rec to_logic_value env s v =
  let eval_rec t = to_logic_value env s t in
  match v with
814
  | Vreg r -> Mreg.find (get_reg env r) s
815
  | Vnum _ | Vbool _ | Vvoid | Vmap _ -> v
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
  | 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 =
845
  let eval_rec t = eval_term env s t in
846
847
  match t.t_node with
  | Tvar x ->
848
    begin
849
850
851
      try
        to_logic_value env s (get_vs env x)
      with Not_found -> assert false
852
853
    end
  | Tbinop(Tand,t1,t2) ->
854
    v_and (eval_rec t1) (eval_rec t2)
855
  | Tbinop(Tor,t1,t2) ->
856
    v_or (eval_rec t1) (eval_rec t2)
857
  | Tbinop(Timplies,t1,t2) ->
858
    v_implies (eval_rec t1) (eval_rec t2)
859
  | Tbinop(Tiff,t1,t2) ->
860
861
    v_iff (eval_rec t1) (eval_rec t2)
  | Tnot t1 -> v_not (eval_rec t1)
862
  | Tapp(ls,tl) ->
863
    eval_app env s ls (List.map eval_rec tl)
864
  | Tif(t1,t2,t3) ->
865
    let u = eval_rec t1 in
866
867
868
869
    begin match u with
    | Vbool true -> eval_term env s t2
    | Vbool false -> eval_term env s t3
    | _ -> v_if u t2 t3
870
    end
871
  | Tlet(t1,tb) ->
872
    let u = eval_rec t1 in
873
    let v,t2 = t_open_bound tb in
874
    eval_term (bind_vs v u env) s t2
875
  | Tcase(t1,tbl) ->
876
(*
877
    eprintf "found a match ... with ...@.";
878
*)
879
    let u = eval_rec t1 in
880
881
882
    eval_match env s u tbl
  | Tquant(q,t) -> Vquant(q,t)
  | Teps t -> Veps t
883
  | Tconst n -> Vnum (big_int_of_const n)
884
885
  | Ttrue -> Vbool true
  | Tfalse -> Vbool false
MARCHE Claude's avatar
MARCHE Claude committed
886
887
888
889
890





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

907
and eval_app env s ls tl =
908
909
  try
    let f = Hls.find builtins ls in
910
    f ls tl
911
  with Not_found ->
912
913
914
915
916
917
918
919
920
    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
921
        eval_term env' s t
922
      | Decl.Dparam _ | Decl.Dind _ ->
923
        Vapp(ls,tl)
924
      | Decl.Ddata dl ->
925
        (* constructor or projection *)
926
        match tl with
927
        | [ Vapp(ls1,tl1) ] ->
928
929
          (* if ls is a projection and ls1 is a constructor,
             we should compute that projection *)
930
931
          let rec iter dl =
            match dl with
932
            | [] -> Vapp(ls,tl)
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
            | (_,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
950
                      | _ -> Vapp(ls,tl)
951
952
953
954
                    in iter3 prs tl1
                  else iter2 rem2
              in iter2 csl
          in iter dl
955
        | _ -> Vapp(ls,tl)
956
957
958
    with Not_found ->
      Format.eprintf "[Exec] definition of logic symbol %s not found@."
        ls.ls_name.Ident.id_string;
959
      Vapp(ls,tl)
960

961
962
963
964
965
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
966

967
let eval_global_term env km t =
968
  get_builtins env;
969
970
971
  let env =
    { mknown = Ident.Mid.empty;
      tknown = km;
972
      funenv = Mps.empty;
973
      regenv = Mreg.empty;
974
975
976
      vsenv = Mvs.empty;
    }
  in
977
  eval_term env Mreg.empty t
978
979


980
(* explicit printing of expr *)
981

982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
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
1003

1004
1005
and p_expr fmt e =
  match e.e_node with
1006
1007
1008
1009
    | Elogic t ->
      fprintf fmt "@[Elogic{type=%a}(%a)@]"
        Mlw_pretty.print_vty e.e_vty
        Pretty.print_term t
1010
1011
    | Evalue pvs -> fprintf fmt "@[Evalue(%a)@]" p_pvs pvs
    | Earrow ps -> fprintf fmt "@[Earrow(%a)@]" p_ps ps
1012
    | Eapp (e1, pvs, _) ->
1013
      fprintf fmt "@[Eapp(%a,@ %a,@ <spec>)@]" p_expr e1 p_pvs pvs
1014
    | Elet(ldefn,e1) ->
1015
1016
1017
1018
      fprintf fmt "@[Elet(%a,@ %a)@]" p_let ldefn p_expr e1
    | Erec (_, _) -> fprintf fmt "@[Erec(_,@ _,@ _)@]"
    | Eif (_, _, _) -> fprintf fmt "@[Eif(_,@ _,@ _)@]"
    | Ecase (_, _) -> fprintf fmt "@[Ecase(_,@ _)@]"
1019
    | Eassign (pls, e1, reg, pvs) ->
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
      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@]"

1032

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

1046
1047
1048
1049
1050
let print_result env s fmt r =
  print_logic_result fmt (to_logic_result env s r)

(*
let print_result env s fmt r =
1051
1052
1053
1054
1055
1056
1057
1058
  let env = {
    mknown = mkm;
    tknown = tkm;
    regenv = Mreg.empty;
    vsenv = Mvs.empty;
  }
  in
  print_result_aux env s fmt r
1059
*)
1060

1061

1062

1063
1064
(* evaluation of WhyML expressions *)

1065
1066
1067
1068
1069
let find_definition env ps =
  try
    Some (Mps.find ps env.funenv)
  with
      Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
1070
        Mlw_decl.find_definition env.mknown ps
1071
1072
1073


(* evaluate expressions *)
MARCHE Claude's avatar
MARCHE Claude committed
1074
let rec eval_expr env (s:state) (e : expr) : result * state =
1075
  match e.e_node with
1076
  | Elogic t ->
1077
1078
1079
1080
(*
    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;
*)
1081
    let v = eval_term env s t in
1082
    let s',v' = to_program_value env s e.e_vty v in
1083
(*
1084
1085
    eprintf "@[<hov 2>[interp]after@ @[%a@]: state=@ %a@]@."
      p_expr e print_state s';
1086
*)