Commit 6a986d78 authored by MARCHE Claude's avatar MARCHE Claude

[interp] support for globals starts to work

parent 11a46591
......@@ -222,10 +222,11 @@ install_no_local:: clean_old_install
mkdir -p $(DATADIR)/why3/vim
mkdir -p $(DATADIR)/why3/lang
mkdir -p $(DATADIR)/why3/theories
mkdir -p $(DATADIR)/why3/modules
mkdir -p $(DATADIR)/why3/modules/mach
mkdir -p $(DATADIR)/why3/drivers
cp -f theories/*.why $(DATADIR)/why3/theories
cp -f modules/*.mlw $(DATADIR)/why3/modules
cp -f modules/mach/*.mlw $(DATADIR)/why3/modules/mach
cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
cp -f share/provers-detection-data.conf $(DATADIR)/why3/
cp -f share/images/icons.rc $(DATADIR)/why3/images
......
......@@ -1213,23 +1213,70 @@ and exec_app env s ps args (*spec*) ity_result =
raise Exit
let eval_global_expr env mkm tkm writes e =
let eval_global_expr env mkm tkm _writes e =
(*
eprintf "@[<hov 2>[interp] eval_global_expr:@ %a@]@."
p_expr e;
*)
get_builtins env;
get_builtin_progs (Mlw_main.library_of_env env);
(*
let init_state =
Sreg.fold
(fun r acc -> Mreg.add r Vvoid acc)
writes Mreg.empty
in
*)
let constr_of_ity renv ity =
if ity_immutable ity then Vvoid,renv else
let regions =
match ity.ity_node with
| Ityapp(_,_,rl) -> rl
| _ ->
eprintf "type = %a@." Mlw_pretty.print_ity ity;
assert false
in
let csl = Mlw_decl.inst_constructors tkm mkm ity in
match csl with
| [] -> assert false
| [ cs,fdl ] ->
let (renv,_regions,vl) =
List.fold_left
(fun (renv,regions,vl) fd ->
match fd.fd_mut,regions with
| None,_ -> (renv,regions,Vvoid::vl)
| Some _r, reg::regions ->
(* found a mutable field *)
let renv' = Mreg.add reg Vvoid renv in
(renv',regions,Vreg reg :: vl)
| Some _, [] -> assert false)
(renv,regions,[]) fdl
in
Vapp(cs,vl),renv
| _ ->
Vvoid,renv (* FIXME ! *)
in
let add_glob _ d ((venv,renv) as acc) =
match d.Mlw_decl.pd_node with
| Mlw_decl.PDval (Mlw_expr.LetV pvs) ->
let ity = pvs.pv_ity in
let v,renv = constr_of_ity renv ity in
(Mvs.add pvs.pv_vs v venv,renv)
(*
Sreg.fold
(fun r acc -> Mreg.add r Vvoid acc)
ity.ity_vars.vars_reg renv)
*)
| _ -> acc
in
let init_env,init_state =
Ident.Mid.fold add_glob mkm (Mvs.empty,Mreg.empty)
in
let env = {
mknown = mkm;
tknown = tkm;
regenv = Mreg.empty;
vsenv = Mvs.empty;
vsenv = init_env;
}
in
eval_expr env init_state e
......
......@@ -92,6 +92,7 @@ module Mut
let x = { i = 0 } in
let s = { i = 0 } in
while x.i <= 10 do
variant { 10 - x.i }
s.i <- s.i + x.i;
x.i <- x.i + 1
done;
......@@ -103,6 +104,7 @@ module Mut
let y = { i = 8 } in
let sum = { i = 0 } in
while x.i <= m do
variant { m - x.i }
let tmp = x.i in
x.i <- y.i;
y.i <- 4 * y.i + tmp;
......@@ -118,7 +120,7 @@ module Mut
val x : refint
let j () = x.i <- 42 (*; x.i *)
let j () = x.i <- 42; x.i
end
......@@ -138,6 +140,7 @@ module Ref
let y = ref 8 in
let sum = ref 0 in
while !x <= m do
variant { m - !x }
let tmp = !x in
x := !y;
y := 4 * !y + tmp;
......@@ -157,7 +160,9 @@ module Ref
done;
42
let rec h n : int =
let rec h n : int
variant { n }
=
let x = ref 0 in
x := !x + 1;
if n = 0 then 0 else h (n-1) + !x
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment