Commit c66385d7 authored by MARCHE Claude's avatar MARCHE Claude

[Interp] fixed support for nested mutable fields

parent 4848a20e
...@@ -143,9 +143,8 @@ execute examples/conjugate.mlw Test.bench ...@@ -143,9 +143,8 @@ execute examples/conjugate.mlw Test.bench
# examples/knuth_prime_numbers.mlw --exec PrimeNumbers.bench # examples/knuth_prime_numbers.mlw --exec PrimeNumbers.bench
execute examples/vstte10_max_sum.mlw TestCase.test_case execute examples/vstte10_max_sum.mlw TestCase.test_case
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
# fails: assert failure on (regions = []) in Mlw_interp.to_program_value execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
# -> needs support for nested mutable fields execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
# examples/verifythis_fm2012_LRS.mlw --exec SuffixArray_test.bench
# fails: needs support for Array.copy # fails: needs support for Array.copy
# examples/verifythis_PrefixSumRec.mlw --exec PrefixSumRec.bench # examples/verifythis_PrefixSumRec.mlw --exec PrefixSumRec.bench
execute examples/vstte10_queens.mlw NQueens.test8 execute examples/vstte10_queens.mlw NQueens.test8
......
...@@ -285,9 +285,33 @@ let sort (a:array int) (data : array int) ...@@ -285,9 +285,33 @@ let sort (a:array int) (data : array int)
assert { !j > 0 -> le a data[!j-1] data[!j] } assert { !j > 0 -> le a data[!j-1] data[!j] }
done done
end end
module SuffixSort_test
use import int.Int
use import array.Array
use LCP
use SuffixSort
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let arr = Array.make 4 0 in
(* [7,8,8,6] *)
arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
let suf = Array.make 4 0 in
for i = 0 to 3 do suf[i] <- i done;
SuffixSort.sort arr suf;
(* should be [3,0,2,1] *)
if suf[0] <> 3 then raise BenchFailure;
if suf[1] <> 0 then raise BenchFailure;
if suf[2] <> 2 then raise BenchFailure;
if suf[3] <> 1 then raise BenchFailure
end
...@@ -389,12 +413,13 @@ let test () = ...@@ -389,12 +413,13 @@ let test () =
let bench () raises { BenchFailure -> true } = let bench () raises { BenchFailure -> true } =
let arr = Array.make 4 0 in let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5; (* [7,8,8,6] *)
arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
let sa = create arr in let sa = create arr in
if sa.suffixes[0] <> 0 then raise BenchFailure; if sa.suffixes[0] <> 3 then raise BenchFailure;
if sa.suffixes[1] <> 1 then raise BenchFailure; if sa.suffixes[1] <> 0 then raise BenchFailure;
if sa.suffixes[2] <> 2 then raise BenchFailure; if sa.suffixes[2] <> 2 then raise BenchFailure;
if sa.suffixes[3] <> 3 then raise BenchFailure if sa.suffixes[3] <> 1 then raise BenchFailure
end end
......
...@@ -481,6 +481,47 @@ let get_builtins env = ...@@ -481,6 +481,47 @@ let get_builtins env =
<r2> -> Vnum 2 <r2> -> Vnum 2
*) *)
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
let to_program_value env s ty v = let to_program_value env s ty v =
match ty,v with match ty,v with
| VTarrow _, _ -> s,v | VTarrow _, _ -> s,v
...@@ -494,42 +535,14 @@ let to_program_value env s ty v = ...@@ -494,42 +535,14 @@ let to_program_value env s ty v =
List.map (get_reg env) rl List.map (get_reg env) rl
| _ -> assert false | _ -> assert false
in in
try let s,regions,v = to_program_value_rec env regions s ity ls vl in
let csl = Mlw_decl.inst_constructors env.tknown env.mknown ity in match regions with
let rec find_cs csl = | [] -> s,v
match csl with | _ ->
| [] -> assert false eprintf "@[<hov 2>error while converting logic value (%a:%a) to a program value:@ regions should be empty, not@ [%a]@]@."
| (cs,fdl)::rem -> print_value v Mlw_pretty.print_vty ty
if ls_equal cs ls then (Pp.print_list Pp.comma Mlw_pretty.print_reg) regions;
(* we found the fields of that constructor *) assert false
begin
let (s,regions,vl) =
List.fold_left2
(fun (s,regions,vl) fd v ->
match fd.fd_mut,regions with
| None,_ -> (s,regions,v::vl)
| 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
begin match regions with
| [] -> ()
| _ ->
eprintf "@[<hov 2>error while converting logic value (%a:%a) to a program value:@ regions should be empty, not@ [%a]@]@."
print_value v Mlw_pretty.print_vty ty
(Pp.print_list Pp.comma Mlw_pretty.print_reg) regions;
assert false
end;
s,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
end end
| VTvalue ity, _ -> | VTvalue ity, _ ->
assert (ity_immutable ity); assert (ity_immutable ity);
...@@ -837,9 +850,6 @@ and eval_match env s u tbl = ...@@ -837,9 +850,6 @@ and eval_match env s u tbl =
Vcase(u,tbl) Vcase(u,tbl)
and eval_app env s ls tl = and eval_app env s ls tl =
(*
if ls.ls_constr > 0 then eval_constr env s ls tl else
*)
try try
let f = Hls.find builtins ls in let f = Hls.find builtins ls in
f ls tl f ls tl
...@@ -857,12 +867,14 @@ and eval_app env s ls tl = ...@@ -857,12 +867,14 @@ and eval_app env s ls tl =
| Decl.Dparam _ | Decl.Dind _ -> | Decl.Dparam _ | Decl.Dind _ ->
Vapp(ls,tl) Vapp(ls,tl)
| Decl.Ddata dl -> | Decl.Ddata dl ->
(* projection *) (* constructor or projection *)
match tl with match tl with
| [ Vapp(ls1,tl1) ] -> | [ Vapp(ls1,tl1) ] ->
(* if ls is a projection and ls1 is a constructor,
we should compute that projection *)
let rec iter dl = let rec iter dl =
match dl with match dl with
| [] -> assert false | [] -> Vapp(ls,tl)
| (_,csl) :: rem -> | (_,csl) :: rem ->
let rec iter2 csl = let rec iter2 csl =
match csl with match csl with
...@@ -1180,7 +1192,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state = ...@@ -1180,7 +1192,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
| Eabstr _ | Eabstr _
| Eabsurd -> | Eabsurd ->
eprintf "@[[Exec] unsupported expression: @[%a@]@]@." eprintf "@[[Exec] unsupported expression: @[%a@]@]@."
Mlw_pretty.print_expr e; (if Debug.test_flag debug then p_expr else Mlw_pretty.print_expr) e;
Irred e, s Irred e, s
and exec_match env t s ebl = and exec_match env t s ebl =
...@@ -1265,45 +1277,13 @@ let eval_global_expr env mkm tkm _writes e = ...@@ -1265,45 +1277,13 @@ let eval_global_expr env mkm tkm _writes e =
vsenv = Mvs.empty; vsenv = Mvs.empty;
} }
in in
let constr_of_ity renv ity =
(*
if ity_immutable ity then default_fixme (* FIXME ! *),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,default_fixme (* FIXME ! *) ::vl)
| Some _r, reg::regions ->
(* found a mutable field *)
let renv' = Mreg.add reg default_fixme (* FIXME ! *) renv in
(renv',regions,Vreg reg :: vl)
| Some _, [] -> assert false)
(renv,regions,[]) fdl
in
Vapp(cs,vl),renv
| _ ->
default_fixme,renv (* FIXME ! *)
*)
let v = any_value_of_type env (ty_of_ity ity) in
to_program_value env renv (VTvalue ity) v
in
let add_glob _ d ((venv,renv) as acc) = let add_glob _ d ((venv,renv) as acc) =
match d.Mlw_decl.pd_node with match d.Mlw_decl.pd_node with
| Mlw_decl.PDval (Mlw_expr.LetV pvs) | Mlw_decl.PDval (Mlw_expr.LetV pvs)
when not (pv_equal pvs Mlw_wp.pv_old) -> when not (pv_equal pvs Mlw_wp.pv_old) ->
let ity = pvs.pv_ity in let ity = pvs.pv_ity in
let renv,v = constr_of_ity renv ity in let v = any_value_of_type env (ty_of_ity ity) in
let renv,v = to_program_value env renv (VTvalue ity) v in
(Mvs.add pvs.pv_vs v venv,renv) (Mvs.add pvs.pv_vs v venv,renv)
| _ -> acc | _ -> acc
in in
......
...@@ -182,6 +182,31 @@ module Ref ...@@ -182,6 +182,31 @@ module Ref
end end
module Pair
use import ref.Ref
type t = { left : ref int ; middle : int; right : ref int }
let a () = { left = ref 13 ; middle = 5; right = ref 42 }
let b () =
let x = a () in
x.left := 57;
x.right := 98;
x
type u = { u1 : t ; u2 : t }
let c () =
let x = { left = ref 1; middle = 2; right = ref 3} in
let y = { left = ref 4; middle = 5; right = ref 6} in
let u = { u1 = x ; u2 = y } in
u.u2.left := 7;
u
end
module Array module Array
use import int.Int use import int.Int
......
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