summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2016-04-18 15:41:12 +0100
committerKathy Gray2016-04-18 15:41:28 +0100
commite35f87c06f2bd3a96bc7df23fe541c96c28d3eab (patch)
tree8cf3eace1b0021b9a7b30f80173a8c38a95df21a /src
parenta732bfdfbacd9be9b06922c1403730aab267c0a7 (diff)
More fixes to interp with regards to warnings and debugging info
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem2344
-rw-r--r--src/lem_interp/interp_inter_imp.lem2
-rw-r--r--src/lem_interp/interp_interface.lem11
-rw-r--r--src/lem_interp/interp_lib.lem1
-rw-r--r--src/lem_interp/pretty_interp.ml75
5 files changed, 1249 insertions, 1184 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 908fe3f1..dc787b5b 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -94,10 +94,10 @@ let rec {ocaml} string_of_value v = match v with
match vals with
| [] -> default_format ()
| v::vs ->
- match v with
- | V_lit (L_aux L_zero _) -> to_bin()
- | V_lit (L_aux L_one _) -> to_bin()
- | _ -> default_format() end end
+ match v with
+ | V_lit (L_aux L_zero _) -> to_bin()
+ | V_lit (L_aux L_one _) -> to_bin()
+ | _ -> default_format() end end
| V_vector_sparse start stop inc vals default ->
"[" ^ (list_to_string (fun (i,v) -> (show i) ^ " = " ^ (string_of_value v)) "," vals) ^ "]:" ^
show start ^ "-" ^show stop ^ "(default of " ^ (string_of_value default) ^ ")"
@@ -154,21 +154,21 @@ let reg_start_pos reg =
match reg with
| Reg _ (Just(typ,_,_,_,_)) _ ->
let start_from_vec targs = match targs with
- | T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s
+ | T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s
| _ -> Assert_extra.failwith "vector type not well formed"
end in
let start_from_reg targs = match targs with
- | T_args [T_arg_typ (T_app "vector" targs)] -> start_from_vec targs
+ | T_args [T_arg_typ (T_app "vector" targs)] -> start_from_vec targs
| _ -> Assert_extra.failwith "register not of vector"
end in
let start_from_abbrev t = match t with
- | T_app "vector" targs -> start_from_vec targs
- | T_app "register" targs -> start_from_reg targs
+ | T_app "vector" targs -> start_from_vec targs
+ | T_app "register" targs -> start_from_reg targs
| _ -> Assert_extra.failwith "register abbrev not register or vector"
end in
match typ with
- | T_app "vector" targs -> start_from_vec targs
- | T_app "register" targs -> start_from_reg targs
+ | T_app "vector" targs -> start_from_vec targs
+ | T_app "register" targs -> start_from_reg targs
| T_abbrev _ t -> start_from_abbrev t
| _ -> Assert_extra.failwith "register type not vector, register, or abbrev"
end
@@ -179,7 +179,7 @@ let reg_size reg =
match reg with
| Reg _ (Just(typ,_,_,_,_)) _ ->
let end_from_vec targs = match targs with
- | T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s
+ | T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s
| _ -> Assert_extra.failwith "register vector type not well formed"
end in
let end_from_reg targs = match targs with
@@ -187,13 +187,13 @@ let reg_size reg =
| _ -> Assert_extra.failwith "register does not contain vector"
end in
let end_from_abbrev t = match t with
- | T_app "vector" targs -> end_from_vec targs
+ | T_app "vector" targs -> end_from_vec targs
| T_app "register" targs -> end_from_reg targs
| _ -> Assert_extra.failwith "register abbrev is neither vector nor register"
end in
match typ with
- | T_app "vector" targs -> end_from_vec targs
- | T_app "register" targs -> end_from_reg targs
+ | T_app "vector" targs -> end_from_vec targs
+ | T_app "register" targs -> end_from_reg targs
| T_abbrev _ t -> end_from_abbrev t
| _ -> Assert_extra.failwith "register type is none of vector, register, or abbrev"
end
@@ -286,13 +286,13 @@ let rec to_fdefs (Defs defs) =
| [] -> Map.empty
| def::defs ->
match def with
- | DEF_fundef f -> (match f with
- | FD_aux (FD_function _ _ _ fcls) _ ->
- match fcls with
- | [] -> to_fdefs (Defs defs)
- | (FCL_aux (FCL_Funcl name _ _) _)::_ ->
- Map.insert (get_id name) fcls (to_fdefs (Defs defs)) end end)
- | _ -> to_fdefs (Defs defs) end end
+ | DEF_fundef f -> (match f with
+ | FD_aux (FD_function _ _ _ fcls) _ ->
+ match fcls with
+ | [] -> to_fdefs (Defs defs)
+ | (FCL_aux (FCL_Funcl name _ _) _)::_ ->
+ Map.insert (get_id name) fcls (to_fdefs (Defs defs)) end end)
+ | _ -> to_fdefs (Defs defs) end end
val to_register_fields : defs tannot -> map string (map string index_range)
let rec to_register_fields (Defs defs) =
@@ -302,8 +302,8 @@ let rec to_register_fields (Defs defs) =
match def with
| DEF_type (TD_aux (TD_register id n1 n2 indexes) l') ->
Map.insert (get_id id)
- (List.foldr (fun (a,b) imap -> Map.insert (get_id b) a imap) Map.empty indexes)
- (to_register_fields (Defs defs))
+ (List.foldr (fun (a,b) imap -> Map.insert (get_id b) a imap) Map.empty indexes)
+ (to_register_fields (Defs defs))
| _ -> to_register_fields (Defs defs)
end
end
@@ -316,8 +316,8 @@ let rec to_registers dd (Defs defs) =
match def with
| DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) ->
let dir = match tannot with
- | Nothing -> dd
- | Just(t, _, _, _,_) -> dd (*TODO, lets pull the direction out properly*)
+ | Nothing -> dd
+ | Just(t, _, _, _,_) -> dd (*TODO, lets pull the direction out properly*)
end in
Map.insert (get_id id) (V_register(Reg id tannot dir)) (to_registers dd (Defs defs))
| DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) ->
@@ -332,11 +332,11 @@ let rec to_aliases (Defs defs) =
| [] -> Map.empty
| def::defs ->
match def with
- | DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) ->
- Map.insert (get_id id) aspec (to_aliases (Defs defs))
- | DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) ->
- Map.insert (get_id id) aspec (to_aliases (Defs defs))
- | _ -> to_aliases (Defs defs)
+ | DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) ->
+ Map.insert (get_id id) aspec (to_aliases (Defs defs))
+ | DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) ->
+ Map.insert (get_id id) aspec (to_aliases (Defs defs))
+ | _ -> to_aliases (Defs defs)
end
end
@@ -353,11 +353,11 @@ let rec to_data_constructors (Defs defs) =
match t with
| TD_variant id _ tq tid_list _ ->
(List.foldr
- (fun (Tu_aux t _) map ->
- match t with
- | (Tu_ty_id x y) -> Map.insert (get_id y) x map
- | Tu_id x -> Map.insert (get_id x) unit_t map end)
- (to_data_constructors (Defs defs))) tid_list
+ (fun (Tu_aux t _) map ->
+ match t with
+ | (Tu_ty_id x y) -> Map.insert (get_id y) x map
+ | Tu_id x -> Map.insert (get_id x) unit_t map end)
+ (to_data_constructors (Defs defs))) tid_list
| _ -> to_data_constructors (Defs defs) end
| _ -> to_data_constructors (Defs defs) end
end
@@ -422,37 +422,37 @@ let litV_to_vec (L_aux lit l) (dir: i_direction) =
let to_v b = V_lit (L_aux b l) in
let hexes = List.map to_v
(List.concat
- (List.map
- (fun s -> match s with
- | #'0' -> [L_zero;L_zero;L_zero;L_zero]
- | #'1' -> [L_zero;L_zero;L_zero;L_one ]
- | #'2' -> [L_zero;L_zero;L_one ;L_zero]
- | #'3' -> [L_zero;L_zero;L_one ;L_one ]
- | #'4' -> [L_zero;L_one ;L_zero;L_zero]
- | #'5' -> [L_zero;L_one ;L_zero;L_one ]
- | #'6' -> [L_zero;L_one ;L_one ;L_zero]
- | #'7' -> [L_zero;L_one ;L_one ;L_one ]
- | #'8' -> [L_one ;L_zero;L_zero;L_zero]
- | #'9' -> [L_one ;L_zero;L_zero;L_one ]
- | #'A' -> [L_one ;L_zero;L_one ;L_zero]
- | #'B' -> [L_one ;L_zero;L_one ;L_one ]
- | #'C' -> [L_one ;L_one ;L_zero;L_zero]
- | #'D' -> [L_one ;L_one ;L_zero;L_one ]
- | #'E' -> [L_one ;L_one ;L_one ;L_zero]
- | #'F' -> [L_one ;L_one ;L_one ;L_one ]
- | #'a' -> [L_one ;L_zero;L_one ;L_zero]
- | #'b' -> [L_one ;L_zero;L_one ;L_one ]
- | #'c' -> [L_one ;L_one ;L_zero;L_zero]
- | #'d' -> [L_one ;L_one ;L_zero;L_one ]
- | #'e' -> [L_one ;L_one ;L_one ;L_zero]
+ (List.map
+ (fun s -> match s with
+ | #'0' -> [L_zero;L_zero;L_zero;L_zero]
+ | #'1' -> [L_zero;L_zero;L_zero;L_one ]
+ | #'2' -> [L_zero;L_zero;L_one ;L_zero]
+ | #'3' -> [L_zero;L_zero;L_one ;L_one ]
+ | #'4' -> [L_zero;L_one ;L_zero;L_zero]
+ | #'5' -> [L_zero;L_one ;L_zero;L_one ]
+ | #'6' -> [L_zero;L_one ;L_one ;L_zero]
+ | #'7' -> [L_zero;L_one ;L_one ;L_one ]
+ | #'8' -> [L_one ;L_zero;L_zero;L_zero]
+ | #'9' -> [L_one ;L_zero;L_zero;L_one ]
+ | #'A' -> [L_one ;L_zero;L_one ;L_zero]
+ | #'B' -> [L_one ;L_zero;L_one ;L_one ]
+ | #'C' -> [L_one ;L_one ;L_zero;L_zero]
+ | #'D' -> [L_one ;L_one ;L_zero;L_one ]
+ | #'E' -> [L_one ;L_one ;L_one ;L_zero]
+ | #'F' -> [L_one ;L_one ;L_one ;L_one ]
+ | #'a' -> [L_one ;L_zero;L_one ;L_zero]
+ | #'b' -> [L_one ;L_zero;L_one ;L_one ]
+ | #'c' -> [L_one ;L_one ;L_zero;L_zero]
+ | #'d' -> [L_one ;L_one ;L_zero;L_one ]
+ | #'e' -> [L_one ;L_one ;L_one ;L_zero]
| #'f' -> [L_one ;L_one ;L_one ;L_one ]
| _ -> Assert_extra.failwith "Lexer did not restrict to valid hex" end)
- (String.toCharList s))) in
+ (String.toCharList s))) in
V_vector (if is_inc(dir) then 0 else ((List.length hexes) - 1)) dir hexes
| L_bin s ->
let bits = List.map
(fun s -> match s with
- | #'0' -> (V_lit (L_aux L_zero l))
+ | #'0' -> (V_lit (L_aux L_zero l))
| #'1' -> (V_lit (L_aux L_one l))
| _ -> Assert_extra.failwith "Lexer did not restrict to valid bin"
end) (String.toCharList s) in
@@ -552,15 +552,15 @@ let merge_lmems ((LMem owner1 c1 mem1 set1) as lmem1) ((LMem owner2 c2 mem2 set2
let diff_mem1 =
List.foldr
(fun i mem -> update_mem false mem i
- (match Map.lookup i mem2 with
- | Nothing -> V_unknown
- | Just v -> merge_values (in_mem lmem1 i) v end)) mem diff1 in
+ (match Map.lookup i mem2 with
+ | Nothing -> V_unknown
+ | Just v -> merge_values (in_mem lmem1 i) v end)) mem diff1 in
let diff_mem2 =
List.foldr
(fun i mem -> update_mem false mem i
- (match Map.lookup i mem1 with
- | Nothing -> V_unknown
- | Just v -> merge_values (in_mem lmem2 i) v end)) diff_mem1 diff2 in
+ (match Map.lookup i mem1 with
+ | Nothing -> V_unknown
+ | Just v -> merge_values (in_mem lmem2 i) v end)) diff_mem1 diff2 in
List.foldr
(fun i mem -> update_mem false mem i (merge_values (in_mem lmem1 i) (in_mem lmem2 i)))
diff_mem2 inters
@@ -583,8 +583,8 @@ let access_vector v n =
list_nth vs (if is_inc(dir) then (n - m) else (m - n))
| V_vector_sparse _ _ _ vs d ->
match (List.lookup n vs) with
- | Nothing -> d
- | Just v -> v end
+ | Nothing -> d
+ | Just v -> v end
| _ -> Assert_extra.failwith ("access_vector given unexpected " ^ string_of_value v)
end )
@@ -617,9 +617,9 @@ let slice_vector v n1 n2 =
else V_vector n1 dir (from_n_to_n (m - n1) (m - n2) vs)
| V_vector_sparse m n dir vs d ->
let (slice, still_sparse) =
- if is_inc(dir)
- then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
- else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
+ if is_inc(dir)
+ then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
+ else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
if still_sparse && is_inc(dir)
then V_vector_sparse n1 (n2 - n1) dir slice d
else if is_inc(dir) then V_vector 0 dir (List.map snd slice)
@@ -641,7 +641,7 @@ val fupdate_record : value -> value -> value
let fupdate_record base updates =
let fupdate_record_helper base updates =
(match (base,updates) with
- | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs (env_from_list us))
+ | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs (env_from_list us))
| _ ->
Assert_extra.failwith ("fupdate_record given unexpected " ^
string_of_value base ^ " and " ^ (string_of_value updates))
@@ -664,9 +664,9 @@ let fupdate_vec v n vexp =
retaint tainted
(match detaint v with
| V_vector m dir vals ->
- V_vector m dir (List.update vals (if is_inc(dir) then (n-m) else (m-n)) vexp)
+ V_vector m dir (List.update vals (if is_inc(dir) then (n-m) else (m-n)) vexp)
| V_vector_sparse m o dir vals d ->
- V_vector_sparse m o dir (fupdate_sparse (if is_inc(dir) then (>) else (<)) vals n vexp) d
+ V_vector_sparse m o dir (fupdate_sparse (if is_inc(dir) then (>) else (<)) vals n vexp) d
| _ -> Assert_extra.failwith ("fupdate_vec given unexpected " ^ string_of_value v)
end)
@@ -700,20 +700,20 @@ let fupdate_vector_slice vec replace start stop =
(match (vec,replace) with
| (V_vector m dir vals,V_vector _ dir' reps) ->
V_vector m dir
- (replace_is vals
- (if dir=dir' then reps else (List.reverse reps))
- 0 (if is_inc(dir) then (start-m) else (m-start)) (if is_inc(dir) then (stop-m) else (m-stop)))
+ (replace_is vals
+ (if dir=dir' then reps else (List.reverse reps))
+ 0 (if is_inc(dir) then (start-m) else (m-start)) (if is_inc(dir) then (stop-m) else (m-stop)))
| (V_vector m dir vals, V_unknown) ->
V_vector m dir
- (replace_is vals
- (List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown)
- 0 (if is_inc(dir) then (start-m) else (m-start)) (if is_inc(dir) then (stop-m) else (m-stop)))
+ (replace_is vals
+ (List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown)
+ 0 (if is_inc(dir) then (start-m) else (m-start)) (if is_inc(dir) then (stop-m) else (m-stop)))
| (V_vector_sparse m n dir vals d,V_vector _ _ reps) ->
let (_,repsi) = List.foldl (fun (i,rs) r -> ((if is_inc(dir) then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
(V_vector_sparse m n dir (replace_sparse (if is_inc(dir) then (<) else (>)) vals (List.reverse repsi)) d)
| (V_vector_sparse m n dir vals d, V_unknown) ->
let (_,repsi) = List.foldl (fun (i,rs) r -> ((if is_inc(dir) then i+1 else i-1), (i,r)::rs)) (start,[])
- (List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown) in
+ (List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown) in
(V_vector_sparse m n dir (replace_sparse (if is_inc(dir) then (<) else (>)) vals (List.reverse repsi)) d)
| (V_unknown,_) -> V_unknown
| _ -> Assert_extra.failwith ("fupdate vector slice given " ^ (string_of_value vec)
@@ -732,20 +732,26 @@ let update_vector_slice track vector value start stop mem =
| V_boxref n t -> update_mem track mem n v end)
mem vs' vals
| ((V_vector m dir vs),(V_vector_sparse n o _ vals d)) ->
- let (V_vector m' _ vs') = slice_vector vector start stop in
+ let (m',vs') = match slice_vector vector start stop with
+ | (V_vector m' _ vs') -> (m',vs')
+ | _ -> Assert_extra.failwith "slice_vector did not return vector" end in
let (_,mem) = foldr (fun vbox (i,mem) ->
match vbox with
- | V_boxref n t ->
- (if is_inc(dir) then i+1 else i-1,
- update_mem track mem n (match List.lookup i vals with
- | Nothing -> d
- | Just v -> v end))
+ | V_boxref n t ->
+ (if is_inc(dir) then i+1 else i-1,
+ update_mem track mem n (match List.lookup i vals with
+ | Nothing -> d
+ | Just v -> v end))
+ | _ -> Assert_extra.failwith "Internal error: update_vector_slice not of boxes"
end) (m,mem) vs' in
mem
| ((V_vector m _ vs),v) ->
- let (V_vector m' _ vs') = slice_vector vector start stop in
+ let (m',vs') = match slice_vector vector start stop with
+ | (V_vector m' _ vs') -> (m',vs')
+ | _ -> Assert_extra.failwith "slice vector didn't return vector" end in
List.foldr (fun vbox mem -> match vbox with
- | V_boxref n t -> update_mem track mem n v end)
+ | V_boxref n t -> update_mem track mem n v
+ | _ -> Assert_extra.failwith "update_vector_slice not of boxes" end)
mem vs'
| _ -> Assert_extra.failwith ("update_vector_slice given unexpected " ^ string_of_value vector
^ " and " ^ string_of_value value)
@@ -828,8 +834,8 @@ let rec update_stack_state stack ((LMem name c mem _) as lmem) =
| Top -> Top
| Hole_frame id oe t_level env (LMem _ _ _ s) Top ->
(match Map.lookup (0 : nat) mem with
- | Nothing -> Thunk_frame oe t_level (add_to_env (id,V_unknown) env) (LMem name c mem s) Top
- | Just v -> Thunk_frame oe t_level (add_to_env (id, v) env) (LMem name c (Map.delete (0 : nat) mem) s) Top end)
+ | Nothing -> Thunk_frame oe t_level (add_to_env (id,V_unknown) env) (LMem name c mem s) Top
+ | Just v -> Thunk_frame oe t_level (add_to_env (id, v) env) (LMem name c (Map.delete (0 : nat) mem) s) Top end)
| Thunk_frame e t_level env _ Top -> Thunk_frame e t_level env lmem Top
| Hole_frame id e t_level env mem s -> Hole_frame id e t_level env mem (update_stack_state s lmem)
| Thunk_frame e t_level env mem s -> Thunk_frame e t_level env mem (update_stack_state s lmem)
@@ -854,28 +860,28 @@ let rec combine_typs ts =
match (t,t') with
| (_,T_var _) -> t
| ((T_app "range" (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
- (T_app "range" (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
- let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
- let r = (larger + larger_r) - smaller in
- T_app "range" (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
+ (T_app "range" (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
+ let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
+ let r = (larger + larger_r) - smaller in
+ T_app "range" (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
| ((T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1);
- T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
- (T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2);
- T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
- let t = combine_typs [t1;t2] in
- match (o1,o2) with
- | (Ord_inc,Ord_inc) ->
- let larger_start = if b1 < b2 then b2 else b1 in
- let smaller_rise = if r1 < r2 then r1 else r2 in
- (T_app "vector" (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
- (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
- | (Ord_dec,Ord_dec) ->
- let smaller_start = if b1 < b2 then b1 else b2 in
- let smaller_fall = if r1 < r2 then r2 else r2 in
- (T_app "vector" (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
- (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
- | _ -> T_var "fresh"
- end
+ T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
+ (T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2);
+ T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
+ let t = combine_typs [t1;t2] in
+ match (o1,o2) with
+ | (Ord_inc,Ord_inc) ->
+ let larger_start = if b1 < b2 then b2 else b1 in
+ let smaller_rise = if r1 < r2 then r1 else r2 in
+ (T_app "vector" (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
+ (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+ | (Ord_dec,Ord_dec) ->
+ let smaller_start = if b1 < b2 then b1 else b2 in
+ let smaller_fall = if r1 < r2 then r2 else r2 in
+ (T_app "vector" (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
+ (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+ | _ -> T_var "fresh"
+ end
| _ -> t'
end
end
@@ -891,28 +897,30 @@ let rec val_typ v =
| V_boxref n t -> T_app "reg" (T_args [T_arg_typ t])
| V_lit (L_aux lit _) ->
match lit with
- | L_unit -> T_id "unit"
- | L_true -> T_id "bool"
- | L_false -> T_id "bool"
- | L_one -> T_id "bit"
- | L_zero -> T_id "bit"
- | L_string _ -> T_id "string"
- | L_num n -> T_app "range" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
- | L_undef -> T_var "fresh"
+ | L_unit -> T_id "unit"
+ | L_true -> T_id "bool"
+ | L_false -> T_id "bool"
+ | L_one -> T_id "bit"
+ | L_zero -> T_id "bit"
+ | L_string _ -> T_id "string"
+ | L_num n -> T_app "range" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
+ | L_undef -> T_var "fresh"
+ | L_hex _ -> Assert_extra.failwith "literal hex not removed"
+ | L_bin _ -> Assert_extra.failwith "literal bin not removed"
end
| V_tuple vals -> T_tup (List.map val_typ vals)
| V_vector n dir vals ->
let ts = List.map val_typ vals in
let t = combine_typs ts in
T_app "vector" (T_args [T_arg_nexp (Ne_const (integerFromNat n)); T_arg_nexp (Ne_const (list_length vals));
- T_arg_order (Ord_aux (if is_inc(dir) then Ord_inc else Ord_dec) Unknown);
- T_arg_typ t])
+ T_arg_order (Ord_aux (if is_inc(dir) then Ord_inc else Ord_dec) Unknown);
+ T_arg_typ t])
| V_vector_sparse n m dir vals d ->
let ts = List.map val_typ (d::(List.map snd vals)) in
let t = combine_typs ts in
T_app "vector" (T_args [T_arg_nexp (Ne_const (integerFromNat n)); T_arg_nexp (Ne_const (integerFromNat m));
- T_arg_order (Ord_aux (if is_inc(dir) then Ord_inc else Ord_dec) Unknown);
- T_arg_typ t])
+ T_arg_order (Ord_aux (if is_inc(dir) then Ord_inc else Ord_dec) Unknown);
+ T_arg_typ t])
| V_record t ivals -> t
| V_list vals ->
let ts = List.map val_typ vals in
@@ -922,6 +930,7 @@ let rec val_typ v =
| V_register reg -> reg_to_t reg
| V_track v _ -> val_typ v
| V_unknown -> T_var "fresh" (*consider carrying the type along*)
+ | V_register_alias _ _ -> T_var "fresh_alias"
end
(* When mode.track_values keeps tracking on registers by extending environment *)
@@ -954,27 +963,27 @@ let rec to_exp mode env v : (exp tannot * lenv) =
then (E_aux (E_vector es) annot, env')
else if is_inc(dir)
then (E_aux (E_vector_indexed
- (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,((integerFromNat n),e)::acc)) (n,[]) es)))
- (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
+ (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,((integerFromNat n),e)::acc)) (n,[]) es)))
+ (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
else if (n+1)= List.length vals
then (E_aux (E_vector es) annot, env')
else
(E_aux (E_vector_indexed
- (snd (List.foldr (fun e (n,acc) -> (n+1,((integerFromNat n),e)::acc)) (n-(List.length es),[]) es))
+ (snd (List.foldr (fun e (n,acc) -> (n+1,((integerFromNat n),e)::acc)) (n-(List.length es),[]) es))
(Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
| V_vector_sparse n m dir vals d ->
let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in
let ((d : (exp tannot)),env') = to_exp mode env' d in
(E_aux (E_vector_indexed
- ((if is_inc(dir) then List.reverse else (fun i -> i))
- (List.map (fun ((i,v), e) -> ((integerFromNat i), e)) (List.zip vals es)))
- (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env')
+ ((if is_inc(dir) then List.reverse else (fun i -> i))
+ (List.map (fun ((i,v), e) -> ((integerFromNat i), e)) (List.zip vals es)))
+ (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env')
| V_record t ivals ->
let (es,env') = mapf (List.map (fun (i,v) -> v) ivals) env in
(E_aux (E_record(FES_aux (FES_Fexps
- (List.map (fun ((id,value), e) -> (FE_aux (FE_Fexp id e) (Unknown,Nothing)))
+ (List.map (fun ((id,value), e) -> (FE_aux (FE_Fexp id e) (Unknown,Nothing)))
(List.zip ivals es)) false)
- (Unknown,Nothing))) annot, env')
+ (Unknown,Nothing))) annot, env')
| V_list(vals) -> let (es,env') = mapf vals env in (E_aux (E_list es) annot, env')
| V_ctor id t ckind vals ->
let annotation = mk_annot true (Just ckind) in
@@ -990,13 +999,15 @@ let rec to_exp mode env v : (exp tannot * lenv) =
then begin let (fid,env') = fresh_var env in
let env' = add_to_env (fid,vals) env' in
(E_aux
- (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))])
- annotation, env')
+ (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))])
+ annotation, env')
end
else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation, env')
| _ ->
let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation,env') end)
| V_register (Reg id tan dir) -> (E_aux (E_id id) annot, env)
+ | V_register _ -> Assert_extra.failwith "V_register contains subreg"
+ | V_register_alias _ _ -> (E_aux (E_id (id_of_string "dummy_register")) annot, env) (*If this persists, then alias spec must change*)
| V_track v' _ ->
if mode.track_values
then begin let (fid,env') = fresh_var env in
@@ -1030,9 +1041,9 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env =
let t = T_tup ts in
let tan = val_annot t in
(E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan))
- (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
- (E_aux e annot))
- annot, taint_env)
+ (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
+ (E_aux e annot))
+ annot, taint_env)
end
let fix_up_nondet typ branches annot =
@@ -1058,11 +1069,15 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
match p with
| P_lit(lit) ->
if is_lit_vector lit then
- let (V_vector n inc bits) = litV_to_vec lit default_dir in
+ let (n, inc, bits) = match litV_to_vec lit default_dir
+ with | V_vector n inc bits -> (n, inc, bits)
+ | _ -> Assert_extra.failwith "litV_to_vec failed" end in
match value with
| V_lit litv ->
if is_lit_vector litv then
- let (V_vector n' inc' bits') = litV_to_vec litv default_dir in
+ let (n', inc', bits') = match litV_to_vec litv default_dir with
+ | V_vector n' inc' bits' -> (n', inc', bits')
+ | _ -> Assert_extra.failwith "litV_to_vec failed" end in
if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, eenv)
else (false,false,eenv)
else (false,false,eenv)
@@ -1116,11 +1131,11 @@ else
| V_lit (L_aux (L_num i) _) ->
match tag with
| Tag_enum _ ->
- match Map.lookup (get_id (Id_aux id Unknown)) lets with
- | Just(V_ctor _ t (C_Enum j) _) ->
- if i = (integerFromNat j) then (true,false,eenv)
- else (false,false,eenv)
- | _ -> (false,false,eenv) end
+ match Map.lookup (get_id (Id_aux id Unknown)) lets with
+ | Just(V_ctor _ t (C_Enum j) _) ->
+ if i = (integerFromNat j) then (true,false,eenv)
+ else (false,false,eenv)
+ | _ -> (false,false,eenv) end
| _ -> (false,false,eenv) end
| V_unknown -> (true,true,eenv)
| _ -> (false,false,eenv) end
@@ -1145,26 +1160,26 @@ else
if ((List.length vals) = (List.length pats))
then foldr2
(fun pat value (matched_p,used_unknown,bounds) ->
- if matched_p then
- let (matched_p,used_unknown',new_bounds) = match_pattern t_level pat (taint_pat value) in
- (matched_p, (used_unknown||used_unknown'), (union_env new_bounds bounds))
- else (false,false,eenv))
+ if matched_p then
+ let (matched_p,used_unknown',new_bounds) = match_pattern t_level pat (taint_pat value) in
+ (matched_p, (used_unknown||used_unknown'), (union_env new_bounds bounds))
+ else (false,false,eenv))
(true,false,eenv) pats vals
else (false,false,eenv)
| V_vector_sparse n m dir vals d ->
if (m = (List.length pats))
then let (_,matched_p,used_unknown,bounds) =
- foldr
- (fun pat (i,matched_p,used_unknown,bounds) ->
- if matched_p
- then let (matched_p,used_unknown',new_bounds) =
- match_pattern t_level pat (match List.lookup i vals with
- | Nothing -> d
- | Just v -> (taint_pat v) end) in
- ((if is_inc(dir) then i+1 else i-1),
- matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
+ foldr
+ (fun pat (i,matched_p,used_unknown,bounds) ->
+ if matched_p
+ then let (matched_p,used_unknown',new_bounds) =
+ match_pattern t_level pat (match List.lookup i vals with
+ | Nothing -> d
+ | Just v -> (taint_pat v) end) in
+ ((if is_inc(dir) then i+1 else i-1),
+ matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
else (i,false,false,eenv)) (n,true,false,eenv) pats in
- (matched_p,used_unknown,bounds)
+ (matched_p,used_unknown,bounds)
else (false,false,eenv)
| V_unknown -> (true,true,eenv)
| _ -> (false,false,eenv)
@@ -1175,22 +1190,22 @@ else
let v_len = if is_inc(dir) then List.length vals + n else n - List.length vals in
List.foldr
(fun (i,pat) (matched_p,used_unknown,bounds) ->
- let i = natFromInteger i in
- if matched_p && i < v_len then
- let (matched_p,used_unknown',new_bounds) =
- match_pattern t_level pat (taint_pat (list_nth vals (if is_inc(dir) then i+n else i-n))) in
- (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
+ let i = natFromInteger i in
+ if matched_p && i < v_len then
+ let (matched_p,used_unknown',new_bounds) =
+ match_pattern t_level pat (taint_pat (list_nth vals (if is_inc(dir) then i+n else i-n))) in
+ (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
else (false,false,eenv))
(true,false,eenv) ipats
| V_vector_sparse n m dir vals d ->
List.foldr
(fun (i,pat) (matched_p,used_unknown,bounds) ->
- let i = natFromInteger i in
- if matched_p && i < m then
- let (matched_p,used_unknown',new_bounds) =
+ let i = natFromInteger i in
+ if matched_p && i < m then
+ let (matched_p,used_unknown',new_bounds) =
match_pattern t_level pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint_pat v) end) in
- (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
- else (false,false,eenv))
+ (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
+ else (false,false,eenv))
(true,false,eenv) ipats
| V_unknown -> (true,true,eenv)
| _ -> (false,false, eenv)
@@ -1201,8 +1216,8 @@ else
let (matched_p,used_unknown,bounds,remaining_vals) = vec_concat_match_top t_level pats vals dir in
(*List.foldl
(fun (matched_p,used_unknown,bounds,r_vals) (P_aux pat (l,Just(t,_,_,_))) ->
- let (matched_p,used_unknown',bounds',matcheds,r_vals) = vec_concat_match_plev t_level pat r_vals inc l t in
- (matched_p,(used_unknown || used_unknown'),(union_env bounds' bounds),r_vals)) (true,false,eenv,vals) pats in*)
+ let (matched_p,used_unknown',bounds',matcheds,r_vals) = vec_concat_match_plev t_level pat r_vals inc l t in
+ (matched_p,(used_unknown || used_unknown'),(union_env bounds' bounds),r_vals)) (true,false,eenv,vals) pats in*)
if matched_p && ([] = remaining_vals) then (matched_p,used_unknown,bounds) else (false,false,eenv)
| V_unknown -> (true,true,eenv)
| _ -> (false,false, eenv)
@@ -1213,9 +1228,9 @@ else
if ((List.length pats)= (List.length vals))
then foldr2
(fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
- let (matched_p,used_unknown',new_bounds) = match_pattern t_level pat (taint_pat v) in
- (matched_p,used_unknown ||used_unknown', (union_env new_bounds bounds))
- else (false,false,eenv))
+ let (matched_p,used_unknown',new_bounds) = match_pattern t_level pat (taint_pat v) in
+ (matched_p,used_unknown ||used_unknown', (union_env new_bounds bounds))
+ else (false,false,eenv))
(true,false,eenv) pats vals
else (false,false,eenv)
| V_unknown -> (true,true,eenv)
@@ -1227,9 +1242,9 @@ else
if ((List.length pats)= (List.length vals))
then foldr2
(fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
- let (matched_p,used_unknown',new_bounds) = match_pattern t_level pat (taint_pat v) in
- (matched_p,used_unknown|| used_unknown', (union_env new_bounds bounds))
- else (false,false,eenv))
+ let (matched_p,used_unknown',new_bounds) = match_pattern t_level pat (taint_pat v) in
+ (matched_p,used_unknown|| used_unknown', (union_env new_bounds bounds))
+ else (false,false,eenv))
(true,false,eenv) pats vals
else (false,false,eenv)
| V_unknown -> (true,true,eenv)
@@ -1245,72 +1260,75 @@ and vec_concat_match_top t_level pats r_vals dir : ((*matched_p*) bool * (*used_
| (P_aux p (l,Just(t,_,_,_,_)))::pats ->
let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match_plev t_level p r_vals dir l false t in
if matched_p then
- let (matched_p',used_unknown',bounds',r_vals) = vec_concat_match_top t_level pats r_vals dir in
- (matched_p',(used_unknown || used_unknown'),union_env bounds' bounds, r_vals)
+ let (matched_p',used_unknown',bounds',r_vals) = vec_concat_match_top t_level pats r_vals dir in
+ (matched_p',(used_unknown || used_unknown'),union_env bounds' bounds, r_vals)
else (false,false,eenv,r_vals)
+ | _ -> Assert_extra.failwith "Type annotation illformed"
end
and vec_concat_match_plev t_level pat r_vals dir l last_pat t =
match pat with
| P_lit (L_aux (L_bin bin_string) l') ->
- let bin_chars = toCharList bin_string in
- let binpats = List.map
+ let bin_chars = toCharList bin_string in
+ let binpats = List.map
(fun b -> P_aux (match b with
- | #'0' -> P_lit (L_aux L_zero l') | #'1' -> P_lit (L_aux L_one l')end) (l',Nothing)) bin_chars in
- vec_concat_match t_level binpats r_vals
+ | #'0' -> P_lit (L_aux L_zero l')
+ | #'1' -> P_lit (L_aux L_one l')
+ | _ -> Assert_extra.failwith "bin not 0 or 1" end) (l',Nothing)) bin_chars in
+ vec_concat_match t_level binpats r_vals
| P_vector pats -> vec_concat_match t_level pats r_vals
| P_id id ->
(match t with
| T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
- let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
- let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match t_level wilds r_vals in
- if matched_p
+ let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+ let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match t_level wilds r_vals in
+ if matched_p
then (matched_p, used_unknown,
(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds))
- bounds),
+ bounds),
matcheds,r_vals)
- else (false,false,eenv,[],[])
+ else (false,false,eenv,[],[])
| T_abbrev _ (T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_])) ->
- let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
- let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match t_level wilds r_vals in
- if matched_p
- then (matched_p, used_unknown,
+ let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+ let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match t_level wilds r_vals in
+ if matched_p
+ then (matched_p, used_unknown,
(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds))
- bounds),
+ bounds),
matcheds,r_vals)
- else (false,false,eenv,[],[])
- | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
- if last_pat
- then
- (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
- else (false,false,eenv,[],[]) (*TODO use some constraint bounds here*)
- | _ ->
- if last_pat
- then
- (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
- else (false,false,eenv,[],[]) end)
+ else (false,false,eenv,[],[])
+ | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
+ if last_pat
+ then
+ (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
+ else (false,false,eenv,[],[]) (*TODO use some constraint bounds here*)
+ | _ ->
+ if last_pat
+ then
+ (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
+ else (false,false,eenv,[],[]) end)
| P_wild -> (match t with
- | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
- let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
- vec_concat_match t_level wilds r_vals
- | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
- if last_pat
- then
- (true,false,eenv,r_vals,[])
- else (false,false,eenv,[],[]) (*TODO use some constraint bounds here*)
- | _ ->
- if last_pat
- then
- (true,false,eenv,r_vals,[])
- else (false,false,eenv,[],[]) end)
+ | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
+ let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+ vec_concat_match t_level wilds r_vals
+ | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
+ if last_pat
+ then
+ (true,false,eenv,r_vals,[])
+ else (false,false,eenv,[],[]) (*TODO use some constraint bounds here*)
+ | _ ->
+ if last_pat
+ then
+ (true,false,eenv,r_vals,[])
+ else (false,false,eenv,[],[]) end)
| P_as (P_aux pat (l',Just(t',_,_,_,_))) id ->
- let (matched_p, used_unknown, bounds,matcheds,r_vals) =
+ let (matched_p, used_unknown, bounds,matcheds,r_vals) =
vec_concat_match_plev t_level pat r_vals dir l last_pat t' in
- if matched_p
- then (matched_p, used_unknown,
+ if matched_p
+ then (matched_p, used_unknown,
(add_to_env (id,V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds) bounds),
matcheds,r_vals)
- else (false,false,eenv,[],[])
+ else (false,false,eenv,[],[])
| P_typ _ (P_aux p (l',Just(t',_,_,_,_))) -> vec_concat_match_plev t_level p r_vals dir l last_pat t
| _ -> (false,false,eenv,[],[]) end
(*TODO Need to support indexed here, skipping intermediate numbers but consumming r_vals, and as *)
@@ -1321,7 +1339,7 @@ and vec_concat_match t_level pats r_vals =
| pat::pats -> match r_vals with
| [] -> (false,false,eenv,[],[])
| r::r_vals ->
- let (matched_p,used_unknown,new_bounds) = match_pattern t_level pat r in
+ let (matched_p,used_unknown,new_bounds) = match_pattern t_level pat r in
if matched_p then
let (matched_p,used_unknown',bounds,matcheds,r_vals) = vec_concat_match t_level pats r_vals in
(matched_p, used_unknown||used_unknown',(union_env new_bounds bounds),r :: matcheds,r_vals)
@@ -1367,7 +1385,10 @@ let resolve_outcome to_match value_thunk action_thunk =
| (Error l s,lm,le) -> (Error l s,lm,le)
end
-let update_stack (Action act stack) fn = Action act (fn stack)
+let update_stack o fn = match o with
+ | Action act stack -> Action act (fn stack)
+ | _ -> o
+end
let debug_out fn value e tl lm le =
(Action (Step (get_exp_l e) fn value) (Thunk_frame e tl le lm Top),lm,le)
@@ -1389,523 +1410,528 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
(fun a -> update_stack a (add_to_top_frame
(fun e env ->
let (es,env') = to_exps mode env vals in
- let (e,env'') = build_e (es++(e::exps)) env' in
- (e,env''))))
+ let (e,env'') = build_e (es++(e::exps)) env' in
+ (e,env''))))
end
and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,effect,reffect) = match annot with
- | Nothing -> (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
+ | Nothing ->
+ (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef,efr) -> (t,tag,ncs,ef,efr) end in
match exp with
| E_lit lit ->
if is_lit_vector lit
then let is_inc = (match typ with
- | T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> IInc | _ -> IDec end) in
+ | T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> IInc | _ -> IDec end) in
(Value (litV_to_vec lit is_inc),l_mem,l_env)
else (Value (V_lit (match lit with
- | L_aux L_false loc -> L_aux L_zero loc
- | L_aux L_true loc -> L_aux L_one loc
- | _ -> lit end)), l_mem,l_env)
+ | L_aux L_false loc -> L_aux L_zero loc
+ | L_aux L_true loc -> L_aux L_one loc
+ | _ -> lit end)), l_mem,l_env)
+ | E_comment _ -> (Value unitv, l_mem,l_env)
+ | E_comment_struc _ -> (Value unitv, l_mem, l_env)
| E_cast ((Typ_aux typ _) as ctyp) exp ->
(*Cast is either a no-op, a signal to read a register, or a signal to change the start of a vector *)
resolve_outcome
- (interp_main mode t_level l_env l_mem exp)
- (fun v lm le ->
- (* Potentially use cast to change vector start position *)
- let conditional_update_vstart () =
- match typ with
- | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
- let i = natFromInteger i in
- match (detaint v) with
- | V_vector start dir vs ->
- if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
- | _ -> (Value v,lm,le) end
- | (Typ_var (Kid_aux (Var "length") _))->
- match (detaint v) with
- | V_vector start dir vs ->
- let i = (List.length vs) - 1 in
- if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
- | _ -> (Value v,lm,le) end
-
- | _ -> (Value v,lm,le) end in
+ (interp_main mode t_level l_env l_mem exp)
+ (fun v lm le ->
+ (* Potentially use cast to change vector start position *)
+ let conditional_update_vstart () =
+ match typ with
+ | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
+ let i = natFromInteger i in
+ match (detaint v) with
+ | V_vector start dir vs ->
+ if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
+ | _ -> (Value v,lm,le) end
+ | (Typ_var (Kid_aux (Var "length") _))->
+ match (detaint v) with
+ | V_vector start dir vs ->
+ let i = (List.length vs) - 1 in
+ if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
+ | _ -> (Value v,lm,le) end
+
+ | _ -> (Value v,lm,le) end in
(match (tag,detaint v) with
- (*Cast is telling us to read a register*)
- | (Tag_extern _, V_register regform) ->
- (Action (Read_reg regform Nothing) (mk_hole l (val_annot (reg_to_t regform)) t_level le lm), lm,le)
- (*Cast is changing vector start position, potentially*)
- | (_,v) -> conditional_update_vstart () end))
- (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env))))
+ (*Cast is telling us to read a register*)
+ | (Tag_extern _, V_register regform) ->
+ (Action (Read_reg regform Nothing) (mk_hole l (val_annot (reg_to_t regform)) t_level le lm), lm,le)
+ (*Cast is changing vector start position, potentially*)
+ | (_,v) -> conditional_update_vstart () end))
+ (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env))))
| E_id id ->
let name = get_id id in
match tag with
- | Tag_empty ->
- match in_lenv l_env id with
- | V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
- | value -> (Value value,l_mem,l_env) end
+ | Tag_empty ->
+ match in_lenv l_env id with
+ | V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
+ | value -> (Value value,l_mem,l_env) end
| Tag_global ->
- match in_env lets name with
- | Just(value) -> (Value value, l_mem,l_env)
- | Nothing ->
- (match in_env regs name with
- | Just(value) -> (Value value, l_mem,l_env)
- | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_global"),l_mem,l_env) end) end
+ match in_env lets name with
+ | Just(value) -> (Value value, l_mem,l_env)
+ | Nothing ->
+ (match in_env regs name with
+ | Just(value) -> (Value value, l_mem,l_env)
+ | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_global"),l_mem,l_env) end) end
| Tag_enum _ ->
match in_env lets name with
| Just(value) -> (Value value,l_mem,l_env)
- | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_enum "), l_mem,l_env)
- end
+ | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_enum "), l_mem,l_env)
+ end
| Tag_extern _ -> (* update with id here when it's never just "register" *)
- let regf = match in_lenv l_env id with (* Check for local treatment of a register as a value *)
- | V_register regform -> regform
- | _ ->
- match in_env regs name with (* Register isn't a local value, so pull from global environment *)
- | Just(V_register regform) -> regform
- | _ -> Reg id annot default_dir end end in
- (Action (Read_reg regf Nothing) (mk_hole l annot t_level l_env l_mem), l_mem, l_env)
+ let regf = match in_lenv l_env id with (* Check for local treatment of a register as a value *)
+ | V_register regform -> regform
+ | _ ->
+ match in_env regs name with (* Register isn't a local value, so pull from global environment *)
+ | Just(V_register regform) -> regform
+ | _ -> Reg id annot default_dir end end in
+ (Action (Read_reg regf Nothing) (mk_hole l annot t_level l_env l_mem), l_mem, l_env)
| Tag_alias ->
- match in_env aliases name with
- | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
- | _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
+ match in_env aliases name with
+ | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
+ | _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
| _ ->
- (Error l
- ("Internal error: tag " ^ (string_of_tag tag) ^ " expected empty,enum,alias,or extern for " ^ name),
- l_mem,l_env)
+ (Error l
+ ("Internal error: tag " ^ (string_of_tag tag) ^ " expected empty,enum,alias,or extern for " ^ name),
+ l_mem,l_env)
end
| E_if cond thn els ->
resolve_outcome
- (interp_main mode t_level l_env l_mem cond)
- (fun value_whole lm le ->
- let value = detaint value_whole in
- match (value,mode.eager_eval) with
- (*TODO remove booleans here when fully removed elsewhere *)
- | (V_lit(L_aux L_one _),true) -> interp_main mode t_level l_env lm thn
- | (V_lit(L_aux L_one _),false) -> debug_out Nothing Nothing thn t_level lm l_env
- | (V_vector _ _ [(V_lit(L_aux L_one _))],true) -> interp_main mode t_level l_env lm thn
- | (V_vector _ _ [(V_lit(L_aux L_one _))],false) -> debug_out Nothing Nothing thn t_level lm l_env
- | (V_unknown,_) ->
- let (branches,maybe_id) = fix_up_nondet typ [thn;els] (l,annot) in
- interp_main mode t_level l_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id))
+ (interp_main mode t_level l_env l_mem cond)
+ (fun value_whole lm le ->
+ let value = detaint value_whole in
+ match (value,mode.eager_eval) with
+ (*TODO remove booleans here when fully removed elsewhere *)
+ | (V_lit(L_aux L_one _),true) -> interp_main mode t_level l_env lm thn
+ | (V_lit(L_aux L_one _),false) -> debug_out Nothing Nothing thn t_level lm l_env
+ | (V_vector _ _ [(V_lit(L_aux L_one _))],true) -> interp_main mode t_level l_env lm thn
+ | (V_vector _ _ [(V_lit(L_aux L_one _))],false) -> debug_out Nothing Nothing thn t_level lm l_env
+ | (V_unknown,_) ->
+ let (branches,maybe_id) = fix_up_nondet typ [thn;els] (l,annot) in
+ interp_main mode t_level l_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id))
| (_,true) -> interp_main mode t_level l_env lm els
- | (_,false) -> debug_out Nothing Nothing els t_level lm l_env end)
+ | (_,false) -> debug_out Nothing Nothing els t_level lm l_env end)
(fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_if c thn els) (l,annot), env))))
| E_for id from to_ by ((Ord_aux o _) as order) exp ->
let is_inc = match o with | Ord_inc -> true | _ -> false end in
resolve_outcome
- (interp_main mode t_level l_env l_mem from)
+ (interp_main mode t_level l_env l_mem from)
(fun from_val_whole lm le ->
- let from_val = detaint from_val_whole in
+ let from_val = detaint from_val_whole in
let (from_e,env) = to_exp mode le from_val_whole in
match from_val with
| V_lit(L_aux(L_num from_num) fl) ->
resolve_outcome
- (interp_main mode t_level env lm to_)
+ (interp_main mode t_level env lm to_)
(fun to_val_whole lm le ->
- let to_val = detaint to_val_whole in
- let (to_e,env) = to_exp mode le to_val_whole in
+ let to_val = detaint to_val_whole in
+ let (to_e,env) = to_exp mode le to_val_whole in
match to_val with
| V_lit(L_aux (L_num to_num) tl) ->
resolve_outcome
(interp_main mode t_level env lm by)
(fun by_val_whole lm le ->
- let by_val = detaint by_val_whole in
- let (by_e,env) = to_exp mode le by_val_whole in
+ let by_val = detaint by_val_whole in
+ let (by_e,env) = to_exp mode le by_val_whole in
match by_val with
| V_lit (L_aux (L_num by_num) bl) ->
if ((is_inc && (from_num > to_num)) || (not(is_inc) && (from_num < to_num)))
then (Value(V_lit (L_aux L_unit l)),lm,le)
else
- let (ftyp,ttyp,btyp) = (val_typ from_val,val_typ to_val,val_typ by_val) in
- let augment_annot = (fl, val_annot (combine_typs [ftyp;ttyp])) in
- let diff = L_aux (L_num (if is_inc then from_num+by_num else from_num - by_num)) fl in
- let (augment_e,env) = match (from_val_whole,by_val_whole) with
- | (V_lit _, V_lit _) -> ((E_aux (E_lit diff) augment_annot), env)
- | (V_track _ rs, V_lit _) -> to_exp mode env (taint (V_lit diff) rs)
- | (V_lit _, V_track _ rs) -> to_exp mode env (taint (V_lit diff) rs)
- | (V_track _ r1, V_track _ r2) ->
- (to_exp mode env (taint (V_lit diff) (r1 union r2))) end in
- let e =
- (E_aux (E_block
- [(E_aux
- (E_let
- (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
- (Unknown,val_annot ftyp))
- exp) (l,annot));
- (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
- (l,annot)) in
- if mode.eager_eval
- then interp_main mode t_level env lm e
- else debug_out Nothing Nothing e t_level lm env
+ let (ftyp,ttyp,btyp) = (val_typ from_val,val_typ to_val,val_typ by_val) in
+ let augment_annot = (fl, val_annot (combine_typs [ftyp;ttyp])) in
+ let diff = L_aux (L_num (if is_inc then from_num+by_num else from_num - by_num)) fl in
+ let (augment_e,env) = match (from_val_whole,by_val_whole) with
+ | (V_lit _, V_lit _) -> ((E_aux (E_lit diff) augment_annot), env)
+ | (V_track _ rs, V_lit _) -> to_exp mode env (taint (V_lit diff) rs)
+ | (V_lit _, V_track _ rs) -> to_exp mode env (taint (V_lit diff) rs)
+ | (V_track _ r1, V_track _ r2) ->
+ (to_exp mode env (taint (V_lit diff) (r1 union r2)))
+ | _ -> Assert_extra.failwith "For loop from and by values not range" end in
+ let e =
+ (E_aux (E_block
+ [(E_aux
+ (E_let
+ (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
+ (Unknown,val_annot ftyp))
+ exp) (l,annot));
+ (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
+ (l,annot)) in
+ if mode.eager_eval
+ then interp_main mode t_level env lm e
+ else debug_out Nothing Nothing e t_level lm env
| V_unknown ->
- let e =
- (E_aux (E_let
- (LB_aux
- (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
- (fl, val_annot (val_typ from_val)))
- exp) (l,annot)) in
- interp_main mode t_level env lm e
+ let e =
+ (E_aux (E_let
+ (LB_aux
+ (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+ (fl, val_annot (val_typ from_val)))
+ exp) (l,annot)) in
+ interp_main mode t_level env lm e
| _ -> (Error l "internal error: by must be a number",lm,le) end)
(fun a -> update_stack a
- (add_to_top_frame (fun b env -> (E_aux (E_for id from_e to_e b order exp) (l,annot), env))))
- | V_unknown ->
- let e =
- (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
- (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
- interp_main mode t_level env lm e
+ (add_to_top_frame (fun b env -> (E_aux (E_for id from_e to_e b order exp) (l,annot), env))))
+ | V_unknown ->
+ let e =
+ (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+ (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
+ interp_main mode t_level env lm e
| _ -> (Error l "internal error: to must be a number",lm,env) end)
(fun a -> update_stack a
- (add_to_top_frame (fun t env ->
- (E_aux (E_for id from_e t by order exp) (l,annot), env))))
- | V_unknown ->
- let e =
- (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
- (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
- interp_main mode t_level env lm e
+ (add_to_top_frame (fun t env ->
+ (E_aux (E_for id from_e t by order exp) (l,annot), env))))
+ | V_unknown ->
+ let e =
+ (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
+ (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
+ interp_main mode t_level env lm e
| _ -> (Error l "internal error: from must be a number",lm,le) end)
(fun a -> update_stack a (add_to_top_frame (fun f env -> (E_aux (E_for id f to_ by order exp) (l,annot), env))))
| E_case exp pats ->
resolve_outcome
- (interp_main mode t_level l_env l_mem exp)
+ (interp_main mode t_level l_env l_mem exp)
(fun v lm le ->
match find_case t_level pats v with
| [] -> (Error l ("No matching patterns in case for value " ^ (string_of_value v)),lm,le)
| [(env,_,exp)] ->
- if mode.eager_eval
- then interp_main mode t_level (union_env env l_env) lm exp
- else debug_out Nothing Nothing exp t_level lm (union_env env l_env)
- | multi_matches ->
- let (lets,taint_env) =
- List.foldr (fun (env,_,exp) (rst,taint_env) ->
- let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
- interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
- end)
+ if mode.eager_eval
+ then interp_main mode t_level (union_env env l_env) lm exp
+ else debug_out Nothing Nothing exp t_level lm (union_env env l_env)
+ | multi_matches ->
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
+ end)
(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env))))
| E_record(FES_aux (FES_Fexps fexps _) fes_annot) ->
let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
exp_list mode t_level
- (fun es env' ->
- ((E_aux
- (E_record
- (FES_aux (FES_Fexps
- (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es)
- false) fes_annot))
- (l,annot)), env'))
- (fun vs -> (V_record typ (List.zip fields vs))) l_env l_mem [] exps
+ (fun es env' ->
+ ((E_aux
+ (E_record
+ (FES_aux (FES_Fexps
+ (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es)
+ false) fes_annot))
+ (l,annot)), env'))
+ (fun vs -> (V_record typ (List.zip fields vs))) l_env l_mem [] exps
| E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) ->
resolve_outcome
- (interp_main mode t_level l_env l_mem exp)
+ (interp_main mode t_level l_env l_mem exp)
(fun rv lm le -> match rv with
| V_record t fvs ->
let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
resolve_outcome
- (exp_list mode t_level
- (fun es env'->
+ (exp_list mode t_level
+ (fun es env'->
let (e,env'') = (to_exp mode env' rv) in
- ((E_aux (E_record_update e
- (FES_aux (FES_Fexps
- (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
- fields es) false) fes_annot))
- (l,annot)), env''))
+ ((E_aux (E_record_update e
+ (FES_aux (FES_Fexps
+ (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
+ fields es) false) fes_annot))
+ (l,annot)), env''))
(fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
(fun vs lm le -> (Value (fupdate_record rv vs), lm, le))
(fun a -> a) (*Due to exp_list this won't happen, but we want to functionaly update on Value *)
- | V_unknown -> (Value V_unknown, lm, le)
+ | V_unknown -> (Value V_unknown, lm, le)
| _ -> (Error l "internal error: record update requires record",lm,le) end)
(fun a -> update_stack a
- (add_to_top_frame
- (fun e env -> (E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot), env))))
+ (add_to_top_frame
+ (fun e env -> (E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot), env))))
| E_list(exps) ->
exp_list mode t_level (fun exps env' -> (E_aux (E_list exps) (l,annot),env')) V_list l_env l_mem [] exps
| E_cons hd tl ->
resolve_outcome
- (interp_main mode t_level l_env l_mem hd)
+ (interp_main mode t_level l_env l_mem hd)
(fun hdv lm le ->
- resolve_outcome
+ resolve_outcome
(interp_main mode t_level l_env lm tl)
(fun tlv lm le -> match detaint tlv with
| V_list t -> (Value (retaint tlv (V_list (hdv::t))),lm,le)
- | V_unknown -> (Value (retaint tlv V_unknown),lm,le)
+ | V_unknown -> (Value (retaint tlv V_unknown),lm,le)
| _ -> (Error l "Internal error '::' of non-list value",lm,le) end)
(fun a -> update_stack a
(add_to_top_frame
- (fun t env -> let (hde,env') = to_exp mode env hdv in (E_aux (E_cons hde t) (l,annot),env')))))
+ (fun t env -> let (hde,env') = to_exp mode env hdv in (E_aux (E_cons hde t) (l,annot),env')))))
(fun a -> update_stack a (add_to_top_frame (fun h env -> (E_aux (E_cons h tl) (l,annot), env))))
| E_field exp id ->
resolve_outcome
- (interp_main mode t_level l_env l_mem exp)
+ (interp_main mode t_level l_env l_mem exp)
(fun value_whole lm le ->
match detaint value_whole with
| V_record t fexps ->
- (match in_env (env_from_list fexps) (get_id id) with
+ (match in_env (env_from_list fexps) (get_id id) with
| Just v -> (Value (retaint value_whole v),lm,l_env)
| Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end)
- | V_register ((Reg _ annot _) as reg_form) ->
- let id' = match annot with
- | Just((T_id id'),_,_,_,_) -> id'
- | Just((T_abbrev (T_id id') _),_,_,_,_) -> id'
- end in
- (match in_env subregs id' with
- | Just(indexes) ->
- (match in_env indexes (get_id id) with
- | Just ir ->
- let sub_reg = SubReg id reg_form ir in
- (Action (Read_reg sub_reg Nothing) (mk_hole l (val_annot (reg_to_t sub_reg)) t_level le lm),lm,le)
- | _ -> (Error l "internal error, unrecognized read, no id",lm,le) end) end)
- | V_unknown -> (Value (retaint value_whole V_unknown),lm,l_env)
+ | V_register ((Reg _ annot _) as reg_form) ->
+ let id' = match annot with
+ | Just((T_id id'),_,_,_,_) -> id'
+ | Just((T_abbrev (T_id id') _),_,_,_,_) -> id'
+ | _ -> Assert_extra.failwith "annotation not well formed for field access"
+ end in
+ (match in_env subregs id' with
+ | Just(indexes) ->
+ (match in_env indexes (get_id id) with
+ | Just ir ->
+ let sub_reg = SubReg id reg_form ir in
+ (Action (Read_reg sub_reg Nothing)
+ (mk_hole l (val_annot (reg_to_t sub_reg)) t_level le lm),lm,le)
+ | _ -> (Error l "Internal error: unrecognized read, no id",lm,le) end)
+ | Nothing -> (Error l "Internal error: subregs indexes not found", lm, le) end)
+ | V_unknown -> (Value (retaint value_whole V_unknown),lm,l_env)
| _ ->
- (Error l ("Internal error: neither register nor record at field access "
- ^ (string_of_value value_whole)),lm,le) end)
+ (Error l ("Internal error: neither register nor record at field access "
+ ^ (string_of_value value_whole)),lm,le) end)
(fun a ->
- match (exp,a) with
- | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)),
- (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) ->
- match in_env subregs id' with
- | Just(indexes) ->
- (match in_env indexes (get_id id) with
- | Just ir ->
- (Action (Read_reg (SubReg id regf ir) Nothing) s)
- | _ -> Error l "Internal error, unrecognized read, no id"
- end)
- | Nothing -> Error l "Internal error, unrecognized read, no reg" end
+ match (exp,a) with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)),
+ (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) ->
+ match in_env subregs id' with
+ | Just(indexes) ->
+ (match in_env indexes (get_id id) with
+ | Just ir ->
+ (Action (Read_reg (SubReg id regf ir) Nothing) s)
+ | _ -> Error l "Internal error, unrecognized read, no id"
+ end)
+ | Nothing -> Error l "Internal error, unrecognized read, no reg" end
| (E_aux _ (l,Just(_,Tag_extern _,_,_,_)),
(Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))->
- match in_env subregs id' with
- | Just(indexes) ->
- match in_env indexes (get_id id) with
- | Just ir ->
- (Action (Read_reg (SubReg id regf ir) Nothing) s)
- | _ -> Error l "Internal error, unrecognized read, no id"
- end
+ match in_env subregs id' with
+ | Just(indexes) ->
+ match in_env indexes (get_id id) with
+ | Just ir ->
+ (Action (Read_reg (SubReg id regf ir) Nothing) s)
+ | _ -> Error l "Internal error, unrecognized read, no id"
+ end
| Nothing -> Error l "Internal error, unrecognized read, no reg" end
| _ -> update_stack a (add_to_top_frame (fun e env -> (E_aux(E_field e id) (l,annot),env))) end)
| E_vector_access vec i ->
resolve_outcome
- (interp_main mode t_level l_env l_mem i)
+ (interp_main mode t_level l_env l_mem i)
(fun iv lm le ->
- match detaint iv with
- | V_unknown -> (Value iv,lm,le)
- | V_lit (L_aux (L_num n) ln) ->
- let n = natFromInteger n in
+ match detaint iv with
+ | V_unknown -> (Value iv,lm,le)
+ | V_lit (L_aux (L_num n) ln) ->
+ let n = natFromInteger n in
resolve_outcome
- (interp_main mode t_level l_env lm vec)
- (fun vvec lm le ->
- let v_access vvec num = (match (detaint vvec, detaint num) with
- | (V_vector _ _ _,V_lit _) -> Value (access_vector vvec n)
- | (V_vector_sparse _ _ _ _ _,V_lit _) -> Value (access_vector vvec n)
+ (interp_main mode t_level l_env lm vec)
+ (fun vvec lm le ->
+ let v_access vvec num = (match (detaint vvec, detaint num) with
+ | (V_vector _ _ _,V_lit _) -> Value (access_vector vvec n)
+ | (V_vector_sparse _ _ _ _ _,V_lit _) -> Value (access_vector vvec n)
| (V_register reg, V_lit _) ->
Action (Read_reg reg (Just (n,n))) (mk_hole l annot t_level l_env lm)
- | (V_unknown,_) -> Value V_unknown
- | _ -> Assert_extra.failwith
- ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]") end) in
- (v_access (retaint iv vvec) iv,lm,le))
+ | (V_unknown,_) -> Value V_unknown
+ | _ -> Assert_extra.failwith
+ ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]") end) in
+ (v_access (retaint iv vvec) iv,lm,le))
(fun a ->
(*TODO I think this pattern match is no longer necessary *)
- match a with
- | Action (Read_reg reg Nothing) stack ->
- (match vec with
- | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
- | _ -> Action (Read_reg reg Nothing)
- (add_to_top_frame
- (fun v env ->
- let (iv_e, env) = to_exp mode env iv in
- (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
- | Action (Read_reg reg (Just (o,p))) stack ->
- (match vec with
- | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
- | _ -> Action (Read_reg reg (Just (o,p)))
- (add_to_top_frame
- (fun v env ->
- let (iv_e, env) = to_exp mode env iv in
- (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
- | _ ->
- update_stack a
- (add_to_top_frame
- (fun v env ->
- let (iv_e, env) = to_exp mode env iv in
- (E_aux (E_vector_access v iv_e) (l,annot), env))) end)
+ match a with
+ | Action (Read_reg reg Nothing) stack ->
+ (match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
+ | _ -> Action (Read_reg reg Nothing)
+ (add_to_top_frame
+ (fun v env ->
+ let (iv_e, env) = to_exp mode env iv in
+ (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
+ | Action (Read_reg reg (Just (o,p))) stack ->
+ (match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
+ | _ -> Action (Read_reg reg (Just (o,p)))
+ (add_to_top_frame
+ (fun v env ->
+ let (iv_e, env) = to_exp mode env iv in
+ (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
+ | _ ->
+ update_stack a
+ (add_to_top_frame
+ (fun v env ->
+ let (iv_e, env) = to_exp mode env iv in
+ (E_aux (E_vector_access v iv_e) (l,annot), env))) end)
| _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
(fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_access vec i) (l,annot), env))))
| E_vector_subrange vec i1 i2 ->
resolve_outcome
- (interp_main mode t_level l_env l_mem i1)
+ (interp_main mode t_level l_env l_mem i1)
(fun i1v lm le ->
- match detaint i1v with
- | V_unknown -> (Value i1v,lm,le)
- | V_lit (L_aux (L_num n1) nl1) ->
+ match detaint i1v with
+ | V_unknown -> (Value i1v,lm,le)
+ | V_lit (L_aux (L_num n1) nl1) ->
resolve_outcome
- (interp_main mode t_level l_env lm i2)
- (fun i2v lm le ->
- match detaint i2v with
- | V_unknown -> (Value i2v,lm,le)
- | _ ->
- resolve_outcome
- (interp_main mode t_level l_env lm vec)
- (fun vvec lm le ->
- let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
- let take_slice vtup vvec =
- (match vtup with
- | V_tuple [v1;v2] ->
- (match (detaint v1, detaint v2) with
- | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) ->
- let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
- (match detaint vvec with
- | V_vector _ _ _ -> Value (slice_vector vvec n1 n2)
- | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2)
- | V_unknown ->
- let inc = n1 < n2 in
- Value (retaint vvec (V_vector n1 (if inc then IInc else IDec)
- (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown)))
- | V_register reg ->
- Action (Read_reg reg (Just (n1,n2))) (mk_hole l annot t_level le lm)
- | _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end)
- | _ -> Assert_extra.failwith("slice not a tuple of nums " ^ (string_of_value vtup)) end) in
- ((take_slice slice (retaint slice vvec)), lm,le))
- (fun a ->
- let rebuild v env = let (ie1,env) = to_exp mode env i1v in
- let (ie2,env) = to_exp mode env i2v in
+ (interp_main mode t_level l_env lm i2)
+ (fun i2v lm le ->
+ match detaint i2v with
+ | V_unknown -> (Value i2v,lm,le)
+ | V_lit (L_aux (L_num n2) nl2) ->
+ resolve_outcome
+ (interp_main mode t_level l_env lm vec)
+ (fun vvec lm le ->
+ let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
+ let take_slice vvec =
+ let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
+ (match detaint vvec with
+ | V_vector _ _ _ -> Value (slice_vector vvec n1 n2)
+ | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2)
+ | V_unknown ->
+ let inc = n1 < n2 in
+ Value (retaint vvec (V_vector n1 (if inc then IInc else IDec)
+ (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown)))
+ | V_register reg ->
+ Action (Read_reg reg (Just (n1,n2))) (mk_hole l annot t_level le lm)
+ | _ -> (Error l ("Vector slice of non-vector " ^ (string_of_value vvec))) end) in
+ ((take_slice (retaint slice vvec)), lm,le))
+ (fun a ->
+ let rebuild v env = let (ie1,env) = to_exp mode env i1v in
+ let (ie2,env) = to_exp mode env i2v in
(E_aux (E_vector_subrange v ie1 ie2) (l,annot), env) in
(*TODO this pattern match should no longer be needed*)
- match a with
- | Action (Read_reg reg Nothing) stack ->
- match vec with
- | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) ->
- Action (Read_reg reg (Just((natFromInteger (get_num i1v)),(natFromInteger (get_num i2v))))) stack
- | _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end
- | Action (Read_reg reg (Just (o,p))) stack ->
- match vec with
- | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) ->
- Action (Read_reg reg (Just((natFromInteger (get_num i1v)),(natFromInteger (get_num i2v))))) stack
- | _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end
+ match a with
+ | Action (Read_reg reg Nothing) stack ->
+ match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) ->
+ Action (Read_reg reg (Just((natFromInteger (get_num i1v)),
+ (natFromInteger (get_num i2v))))) stack
+ | _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end
+ | Action (Read_reg reg (Just (o,p))) stack ->
+ match vec with
+ | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) ->
+ Action (Read_reg reg (Just((natFromInteger (get_num i1v)),
+ (natFromInteger (get_num i2v))))) stack
+ | _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end
| _ -> update_stack a (add_to_top_frame rebuild) end)
- end)
+ | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env)
+ end)
(fun a -> update_stack a
- (add_to_top_frame
- (fun i2 env ->
- let (ie1,env) = to_exp mode env i1v in
- (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env))))
- end)
+ (add_to_top_frame
+ (fun i2 env ->
+ let (ie1,env) = to_exp mode env i1v in
+ (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env))))
+ | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env) end)
(fun a ->
- update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env))))
+ update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env))))
| E_vector_update vec i exp ->
resolve_outcome
- (interp_main mode t_level l_env l_mem i)
+ (interp_main mode t_level l_env l_mem i)
(fun vi lm le ->
(match (detaint vi) with
| V_lit (L_aux (L_num n1) ln1) ->
(resolve_outcome
- (interp_main mode t_level le lm exp)
+ (interp_main mode t_level le lm exp)
(fun vup lm le ->
resolve_outcome
- (interp_main mode t_level le lm vec)
+ (interp_main mode t_level le lm vec)
(fun vec lm le ->
- let fvup vi vec = (match vec with
- | V_vector _ _ _ -> fupdate_vec vec (natFromInteger n1) vup
- | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec (natFromInteger n1) vup
- | V_unknown -> V_unknown
+ let fvup vi vec = (match vec with
+ | V_vector _ _ _ -> fupdate_vec vec (natFromInteger n1) vup
+ | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec (natFromInteger n1) vup
+ | V_unknown -> V_unknown
| _ -> Assert_extra.failwith "Update of vector given non-vector" end) in
- (Value (binary_taint fvup vi vec),lm,le))
+ (Value (binary_taint fvup vi vec),lm,le))
(fun a -> update_stack a
- (add_to_top_frame
- (fun v env ->
+ (add_to_top_frame
+ (fun v env ->
let (eup,env') = (to_exp mode env vup) in
- let (ei, env') = (to_exp mode env' vi) in
+ let (ei, env') = (to_exp mode env' vi) in
(E_aux (E_vector_update v ei eup) (l,annot), env')))))
(fun a -> update_stack a
- (add_to_top_frame
- (fun e env ->
- let (ei, env) = to_exp mode env vi in
- (E_aux (E_vector_update vec ei e) (l,annot), env)))))
- | V_unknown -> (Value vi,lm,l_env)
+ (add_to_top_frame
+ (fun e env ->
+ let (ei, env) = to_exp mode env vi in
+ (E_aux (E_vector_update vec ei e) (l,annot), env)))))
+ | V_unknown -> (Value vi,lm,l_env)
| _ -> Assert_extra.failwith "Update of vector requires number for access" end))
(fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_update vec i exp) (l,annot), env))))
| E_vector_update_subrange vec i1 i2 exp ->
resolve_outcome
- (interp_main mode t_level l_env l_mem i1)
+ (interp_main mode t_level l_env l_mem i1)
(fun vi1 lm le ->
- match detaint vi1 with
- | V_unknown -> (Value vi1,lm,le)
+ match detaint vi1 with
+ | V_unknown -> (Value vi1,lm,le)
| V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome
(interp_main mode t_level l_env lm i2)
(fun vi2 lm le ->
- match detaint vi2 with
- | V_unknown -> (Value vi2,lm,le)
+ match detaint vi2 with
+ | V_unknown -> (Value vi2,lm,le)
| V_lit (L_aux (L_num n2) ln2) ->
resolve_outcome
- (interp_main mode t_level l_env lm exp)
+ (interp_main mode t_level l_env lm exp)
(fun v_rep lm le ->
(resolve_outcome
(interp_main mode t_level l_env lm vec)
(fun vvec lm le ->
- let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in
- let fup_v_slice v1 vvec = (match vvec with
+ let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in
+ let fup_v_slice v1 vvec = (match vvec with
| V_vector _ _ _ ->
- fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2)
- | V_vector_sparse _ _ _ _ _ ->
- fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2)
- | V_unknown -> V_unknown
- | _ -> Assert_extra.failwith "Vector update requires vector" end) in
- (Value (binary_taint fup_v_slice slice vvec),lm,le))
+ fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2)
+ | V_vector_sparse _ _ _ _ _ ->
+ fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2)
+ | V_unknown -> V_unknown
+ | _ -> Assert_extra.failwith "Vector update requires vector" end) in
+ (Value (binary_taint fup_v_slice slice vvec),lm,le))
(fun a -> update_stack a
(add_to_top_frame
- (fun v env ->
+ (fun v env ->
let (e_rep,env') = to_exp mode env v_rep in
let (ei1, env') = to_exp mode env' vi1 in
let (ei2, env') = to_exp mode env' vi2 in
(E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env'))))))
(fun a -> update_stack a
(add_to_top_frame
- (fun e env ->
+ (fun e env ->
let (ei1,env') = to_exp mode env vi1 in
let (ei2,env') = to_exp mode env' vi2 in
(E_aux (E_vector_update_subrange vec ei1 ei2 e) (l,annot),env'))))
| _ -> Assert_extra.failwith "vector update requires number" end)
(fun a ->
- update_stack a (add_to_top_frame
+ update_stack a (add_to_top_frame
(fun i2 env ->
let (ei1, env') = to_exp mode env vi1 in
(E_aux (E_vector_update_subrange vec ei1 i2 exp) (l,annot), env'))))
| _ -> Assert_extra.failwith "vector update requires number" end)
(fun a ->
- update_stack a
- (add_to_top_frame (fun i1 env -> (E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot), env))))
+ update_stack a
+ (add_to_top_frame (fun i1 env -> (E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot), env))))
| E_vector_append e1 e2 ->
resolve_outcome
- (interp_main mode t_level l_env l_mem e1)
+ (interp_main mode t_level l_env l_mem e1)
(fun v1 lm le ->
match detaint v1 with
- | V_unknown -> (Value v1,lm,l_env)
+ | V_unknown -> (Value v1,lm,l_env)
| _ ->
(resolve_outcome
- (interp_main mode t_level l_env lm e2)
+ (interp_main mode t_level l_env lm e2)
(fun v2 lm le ->
- let append v1 v2 = (match (v1,v2) with
+ let append v1 v2 = (match (v1,v2) with
| (V_vector m dir vals1, V_vector _ _ vals2) ->
- let vals = vals1++vals2 in
- let len = List.length vals in
- if is_inc(dir)
- then V_vector m dir vals
- else if m > len
- then V_vector m dir vals
- else V_vector (len-1) dir vals
- | (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) ->
- let original_len = List.length vals1 in
- let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
- let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
- V_vector_sparse m (len+original_len) dir (sparse_vals ++ sparse_update) d
- | (V_vector_sparse m len dir vals1 d, V_vector _ _ vals2) ->
- let new_len = List.length vals2 in
- let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
- V_vector_sparse m (len+new_len) dir (vals1++sparse_vals) d
- | (V_vector_sparse m len dir vals1 d, V_vector_sparse _ new_len _ vals2 _) ->
- let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
- V_vector_sparse m (len+new_len) dir (vals1 ++ sparse_update) d
- | (V_unknown,_) -> V_unknown (*update to get length from type*)
- | (_,V_unknown) -> V_unknown (*see above*)
+ let vals = vals1++vals2 in
+ let len = List.length vals in
+ if is_inc(dir)
+ then V_vector m dir vals
+ else if m > len
+ then V_vector m dir vals
+ else V_vector (len-1) dir vals
+ | (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) ->
+ let original_len = List.length vals1 in
+ let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
+ let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
+ V_vector_sparse m (len+original_len) dir (sparse_vals ++ sparse_update) d
+ | (V_vector_sparse m len dir vals1 d, V_vector _ _ vals2) ->
+ let new_len = List.length vals2 in
+ let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
+ V_vector_sparse m (len+new_len) dir (vals1++sparse_vals) d
+ | (V_vector_sparse m len dir vals1 d, V_vector_sparse _ new_len _ vals2 _) ->
+ let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
+ V_vector_sparse m (len+new_len) dir (vals1 ++ sparse_update) d
+ | (V_unknown,_) -> V_unknown (*update to get length from type*)
+ | (_,V_unknown) -> V_unknown (*see above*)
| _ -> Assert_extra.failwith "vector concat requires vector" end) in
- (Value (binary_taint append v1 v2),lm,le))
+ (Value (binary_taint append v1 v2),lm,le))
(fun a -> update_stack a (add_to_top_frame
(fun e env ->
let (e1,env') = to_exp mode env v1 in
@@ -1920,146 +1946,151 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let base = (if is_inc then 0 else (List.length exps) - 1) in
exp_list mode t_level
(fun exps env' -> (E_aux (E_vector exps) (l,annot),env'))
- (fun vals -> V_vector base dir vals) l_env l_mem [] exps
+ (fun vals -> V_vector base dir vals) l_env l_mem [] exps
| E_vector_indexed iexps (Def_val_aux default dannot) ->
let (indexes,exps) = List.unzip iexps in
let (dir,base,len) = (match typ with
| T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux Ord_inc _); _]) ->
- (IInc,base,len)
+ (IInc,base,len)
| T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux _ _); _]) ->
- (IDec,base,len) end) in
+ (IDec,base,len)
+ | _ -> Assert_extra.failwith "Vector type not as expected for indexed vector" end) in
(match default with
- | Def_val_empty ->
- exp_list mode t_level
- (fun es env' -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
- (Def_val_aux default dannot)) (l,annot), env'))
+ | Def_val_empty ->
+ exp_list mode t_level
+ (fun es env' -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
+ (Def_val_aux default dannot)) (l,annot), env'))
(fun vals -> V_vector (if indexes=[] then 0 else (natFromInteger (List_extra.head indexes))) dir vals)
- l_env l_mem [] exps
- | Def_val_dec default_exp ->
- let (b,len) = match (base,len) with
- | (Ne_const b,Ne_const l) -> (natFromInteger b, natFromInteger l) end in
- resolve_outcome
- (interp_main mode t_level l_env l_mem default_exp)
- (fun v lm le ->
- exp_list mode t_level
+ l_env l_mem [] exps
+ | Def_val_dec default_exp ->
+ let (b,len) = match (base,len) with
+ | (Ne_const b,Ne_const l) -> (natFromInteger b, natFromInteger l)
+ | _ -> Assert_extra.failwith "Vector start and end unset in vector with default value" end in
+ resolve_outcome
+ (interp_main mode t_level l_env l_mem default_exp)
+ (fun v lm le ->
+ exp_list mode t_level
(fun es env' ->
let (ev,env'') = to_exp mode env' v in
(E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
- (Def_val_aux (Def_val_dec ev) dannot))
- (l,annot), env''))
- (fun vs ->
- (V_vector_sparse b len dir (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
- (fun a ->
- update_stack a
- (add_to_top_frame (fun e env ->
- (E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot), env)))) end)
+ (Def_val_aux (Def_val_dec ev) dannot))
+ (l,annot), env''))
+ (fun vs ->
+ (V_vector_sparse b len dir (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
+ (fun a ->
+ update_stack a
+ (add_to_top_frame (fun e env ->
+ (E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot), env)))) end)
| E_block exps -> interp_block mode t_level l_env l_env l_mem l annot exps
| E_nondet exps ->
(Action (Nondet exps tag)
- (match tag with
- | Tag_unknown (Just id) -> mk_hole l annot t_level l_env l_mem
- | _ -> mk_thunk l annot t_level l_env l_mem end),
+ (match tag with
+ | Tag_unknown (Just id) -> mk_hole l annot t_level l_env l_mem
+ | _ -> mk_thunk l annot t_level l_env l_mem end),
l_mem, l_env)
| E_app f args ->
(match (exp_list mode t_level
(fun es env -> (E_aux (E_app f es) (l,annot),env))
- (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end)
- l_env l_mem [] args) with
+ (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end)
+ l_env l_mem [] args) with
| (Value v,lm,le) ->
let name = get_id f in
(match tag with
| Tag_global ->
- (match Map.lookup name fdefs with
- | Just(funcls) ->
+ (match Map.lookup name fdefs with
+ | Just(funcls) ->
(match find_funcl t_level funcls v with
- | [] ->
- (Error l ("No matching pattern for function " ^ name ^
- " on value " ^ (string_of_value v)),l_mem,l_env)
- | [(env,_,exp)] ->
- resolve_outcome
+ | [] ->
+ (Error l ("No matching pattern for function " ^ name ^
+ " on value " ^ (string_of_value v)),l_mem,l_env)
+ | [(env,_,exp)] ->
+ resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just v) exp t_level (emem name) env))
- (fun ret lm le -> (Value ret, l_mem,l_env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just v) exp t_level (emem name) env))
+ (fun ret lm le -> (Value ret, l_mem,l_env))
(fun a -> update_stack a
- (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
- t_level l_env l_mem stack)))
+ (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
+ t_level l_env l_mem stack)))
| multi_matches ->
- let (lets,taint_env) =
- List.foldr (fun (env,_,exp) (rst,taint_env) ->
- let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
- interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
- end)
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
+ end)
| Nothing ->
- (Error l (String.stringAppend "Internal error: function with tag global unfound " name),lm,le) end)
- | Tag_empty ->
- (match Map.lookup name fdefs with
- | Just(funcls) ->
+ (Error l ("Internal error: function with tag global unfound " ^ name),lm,le) end)
+ | Tag_empty ->
+ (match Map.lookup name fdefs with
+ | Just(funcls) ->
(match find_funcl t_level funcls v with
- | [] ->
- (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
- | [(env,used_unknown,exp)] ->
- resolve_outcome
+ | [] ->
+ (Error l ("No matching pattern for function " ^ name),l_mem,l_env)
+ | [(env,used_unknown,exp)] ->
+ resolve_outcome
(if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just v) exp t_level (emem name) env))
- (fun ret lm le -> (Value ret, l_mem,l_env))
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just v) exp t_level (emem name) env))
+ (fun ret lm le -> (Value ret, l_mem,l_env))
(fun a -> update_stack a
- (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
- t_level l_env l_mem stack)))
+ (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
+ t_level l_env l_mem stack)))
+ | _ -> (Error l ("Internal error: multiple pattern matches found for " ^ name), l_mem, l_env)
end)
| Nothing ->
- (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
- | Tag_spec ->
+ (Error l ("Internal error: function with local tag unfound " ^ name),lm,le) end)
+ | Tag_spec ->
(match Map.lookup name fdefs with
- | Just(funcls) ->
+ | Just(funcls) ->
(match find_funcl t_level funcls v with
- | [] ->
- (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
- | [(env,used_unknown,exp)] ->
+ | [] ->
+ (Error l ("No matching pattern for function " ^ name ),l_mem,l_env)
+ | [(env,used_unknown,exp)] ->
resolve_outcome
- (if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
+ (if mode.eager_eval
+ then (interp_main mode t_level env (emem name) exp)
else (debug_out (Just name) (Just v) exp t_level (emem name) env))
- (fun ret lm le -> (Value ret, l_mem,l_env))
+ (fun ret lm le -> (Value ret, l_mem,l_env))
(fun a -> update_stack a
- (fun stack ->
+ (fun stack ->
(Hole_frame redex_id
(E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem stack)))
+ | _ -> (Error l ("Internal error: multiple pattern matches for " ^ name), l_mem, l_env)
end)
| Nothing ->
- (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
+ (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
| Tag_ctor ->
(match Map.lookup name ctors with
| Just(_) -> (Value (V_ctor f typ C_Union v), lm, le)
| Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
end)
| Tag_extern opt_name ->
- let effects = (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in
+ let effects = (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in
let name_ext = match opt_name with | Just s -> s | Nothing -> name end in
let mk_hole_frame act = (Action act (mk_hole l annot t_level le lm), lm, le) in
- let mk_thunk_frame act = (Action act (mk_thunk l annot t_level le lm), lm, le) in
+ let mk_thunk_frame act = (Action act (mk_thunk l annot t_level le lm), lm, le) in
if has_rmem_effect effects
then mk_hole_frame (Read_mem (id_of_string name_ext) v Nothing)
else if has_barr_effect effects
then mk_thunk_frame (Barrier (id_of_string name_ext) v)
- else if has_depend_effect effects
- then mk_thunk_frame (Footprint (id_of_string name_ext) v)
- else if has_wmem_effect effects
- then let (wv,v) =
- match v with
- | V_tuple params_list ->
- let reved = List.reverse params_list in
- (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) end in
+ else if has_depend_effect effects
+ then mk_thunk_frame (Footprint (id_of_string name_ext) v)
+ else if has_wmem_effect effects
+ then let (wv,v) =
+ match v with
+ | V_tuple params_list ->
+ let reved = List.reverse params_list in
+ (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved)))
+ | _ -> Assert_extra.failwith ("Expected tuple found " ^ (string_of_value v)) end in
mk_hole_frame (Write_mem (id_of_string name_ext) v Nothing wv)
- else if has_eamem_effect effects
- then mk_thunk_frame (Write_ea (id_of_string name_ext) v)
- else if has_wmv_effect effects
- then mk_hole_frame (Write_memv (id_of_string name_ext) v)
+ else if has_eamem_effect effects
+ then mk_thunk_frame (Write_ea (id_of_string name_ext) v)
+ else if has_wmv_effect effects
+ then mk_hole_frame (Write_memv (id_of_string name_ext) v)
else mk_hole_frame (Call_extern name_ext v)
| _ ->
- (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end)
+ (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end)
| out -> out end)
| E_app_infix lft op r ->
let op = match op with
@@ -2068,67 +2099,71 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
end in
let name = get_id op in
resolve_outcome
- (interp_main mode t_level l_env l_mem lft)
+ (interp_main mode t_level l_env l_mem lft)
(fun lv lm le ->
resolve_outcome
- (interp_main mode t_level l_env lm r)
+ (interp_main mode t_level l_env lm r)
(fun rv lm le ->
match tag with
| Tag_global ->
- (match Map.lookup name fdefs with
- | Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
+ (match Map.lookup name fdefs with
+ | Nothing -> (Error l ("Internal error: no function def for " ^ name),lm,le)
| Just (funcls) ->
- (match find_funcl t_level funcls (V_tuple [lv;rv]) with
- | [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
- | [(env,used_unknown,exp)] ->
- resolve_outcome
- (if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
- (fun ret lm le -> (Value ret,l_mem,l_env))
+ (match find_funcl t_level funcls (V_tuple [lv;rv]) with
+ | [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
+ | [(env,used_unknown,exp)] ->
+ resolve_outcome
+ (if mode.eager_eval
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
+ (fun ret lm le -> (Value ret,l_mem,l_env))
(fun a -> update_stack a
- (fun stack ->
- (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
- t_level l_env l_mem stack)))
- end)end)
- | Tag_empty ->
- (match Map.lookup name fdefs with
- | Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
+ (fun stack ->
+ (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
+ t_level l_env l_mem stack)))
+ | _ -> (Error l ("Internal error: multiple pattern matches for " ^ name),lm,le)
+ end)end)
+ | Tag_empty ->
+ (match Map.lookup name fdefs with
+ | Nothing -> (Error l ("Internal error: no function def for " ^ name),lm,le)
| Just (funcls) ->
- (match find_funcl t_level funcls (V_tuple [lv;rv]) with
- | [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
- | [(env,used_unknown,exp)] ->
- resolve_outcome
- (if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
- (fun ret lm le -> (Value ret,l_mem,l_env))
+ (match find_funcl t_level funcls (V_tuple [lv;rv]) with
+ | [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
+ | [(env,used_unknown,exp)] ->
+ resolve_outcome
+ (if mode.eager_eval
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
+ (fun ret lm le -> (Value ret,l_mem,l_env))
(fun a -> update_stack a
- (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,annot))
- t_level l_env l_mem stack)))
- end)end)
+ (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,annot))
+ t_level l_env l_mem stack)))
+ | _ -> (Error l ("Internal error: multiple pattern matches for " ^ name),lm,le)
+ end)end)
| Tag_spec ->
(match Map.lookup name fdefs with
- | Nothing -> (Error l ("No function definition found for " ^ name),lm,le)
+ | Nothing -> (Error l ("Internal error: No function definition found for " ^ name),lm,le)
| Just (funcls) ->
- (match find_funcl t_level funcls (V_tuple [lv;rv]) with
- | [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
- | [(env,used_unknown,exp)] ->
- resolve_outcome
- (if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
- (fun ret lm le -> (Value ret,l_mem,l_env))
+ (match find_funcl t_level funcls (V_tuple [lv;rv]) with
+ | [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
+ | [(env,used_unknown,exp)] ->
+ resolve_outcome
+ (if mode.eager_eval
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level (emem name) env))
+ (fun ret lm le -> (Value ret,l_mem,l_env))
(fun a -> update_stack a
- (fun stack -> (Hole_frame redex_id
- (E_aux (E_id redex_id) (l,(intern_annot annot)))
- t_level l_env l_mem stack)))
- end)end)
+ (fun stack -> (Hole_frame redex_id
+ (E_aux (E_id redex_id) (l,(intern_annot annot)))
+ t_level l_env l_mem stack)))
+ | _ -> (Error l ("Internal error: multiple pattern matches for " ^ name), lm, le)
+ end)end)
| Tag_extern ext_name ->
let ext_name = match ext_name with Just s -> s | Nothing -> name end in
- (Action (Call_extern ext_name (V_tuple [lv;rv]))
- (Hole_frame redex_id
- (E_aux (E_id redex_id) (l,intern_annot annot)) t_level le lm Top),lm,le) end)
+ (Action (Call_extern ext_name (V_tuple [lv;rv]))
+ (Hole_frame redex_id
+ (E_aux (E_id redex_id) (l,intern_annot annot)) t_level le lm Top),lm,le)
+ | _ -> (Error l "Internal error: unexpected tag for app_infix", l_mem, l_env) end)
(fun a -> update_stack a
(add_to_top_frame
(fun r env -> let (el,env') = to_exp mode env lv in (E_aux (E_app_infix el op r) (l,annot), env')))))
@@ -2148,11 +2183,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_lit (L_aux L_zero _) -> (Action (Fail v) (mk_thunk l annot t_level l_env l_mem), lm,le)
| V_lit (L_aux L_false _) -> (Action (Fail v) (mk_thunk l annot t_level l_env l_mem), lm,le)
| V_unknown ->
- let (branches,maybe_id) =
+ let (branches,maybe_id) =
fix_up_nondet typ [unit_e;
E_aux (E_assert (E_aux (E_lit (L_aux L_zero l))
- (l,val_annot (T_id "bit"))) msg) (l,annot)] (l,annot) in
- interp_main mode t_level l_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id))
+ (l,val_annot (T_id "bit"))) msg) (l,annot)]
+ (l,annot) in
+ interp_main mode t_level l_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id))
+ | _ -> (Error l ("assert given unexpected " ^ (string_of_value c)),l_mem,l_env)
end))
(fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_assert c msg) (l,annot), env)))))
(fun a -> update_stack a (add_to_top_frame (fun m env -> (E_aux (E_assert cond m) (l,annot), env))))
@@ -2175,17 +2212,18 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
resolve_outcome outcome
(fun v lm le -> (Value v,lm,le))
(fun a ->
- (match a with
- | (Action (Write_reg regf range value) stack) -> a
- | (Action (Write_mem id a_ range value) stack) -> a
- | (Action (Write_memv _ _) stack) -> a
- | _ -> update_stack a (add_to_top_frame
- (fun e env ->
+ (match a with
+ | (Action (Write_reg regf range value) stack) -> a
+ | (Action (Write_mem id a_ range value) stack) -> a
+ | (Action (Write_memv _ _) stack) -> a
+ | _ -> update_stack a (add_to_top_frame
+ (fun e env ->
let (ev,env') = (to_exp mode env v) in
let (lexp,env') = (lexp_builder e env') in
(E_aux (E_assign lexp ev) (l,annot),env'))) end))
- end))
+ end))
(fun a -> update_stack a (add_to_top_frame (fun v env -> (E_aux (E_assign lexp v) (l,annot), env))))
+ | _ -> (Error l "Internal expression escaped to interpreter", l_mem, l_env)
end
(*TODO shrink location information on recursive calls *)
@@ -2199,11 +2237,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| exp:: exps ->
resolve_outcome (interp_main mode t_level local_env local_mem exp)
(fun _ lm le ->
- if mode.eager_eval
- then interp_block mode t_level init_env le lm l tannot exps
- else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
+ if mode.eager_eval
+ then interp_block mode t_level init_env le lm l tannot exps
+ else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
(fun a -> update_stack a
- (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
+ (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
end
and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot)
@@ -2214,7 +2252,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Just(t, tag, ncs, ef,efr) -> (t,tag,ncs,ef,efr) end in
let recenter_val typ value = match typ with
| T_app "reg" (T_args [T_arg_typ
- (T_app "vector" (T_args [T_arg_nexp (Ne_const start); T_arg_nexp (Ne_const size); _; _ ]))]) ->
+ (T_app "vector" (T_args [T_arg_nexp (Ne_const start); T_arg_nexp (Ne_const size); _; _ ]))]) ->
update_vector_start default_dir (natFromInteger start) (natFromInteger size) value
| T_abbrev _ (T_app "vector" (T_args [T_arg_nexp (Ne_const start); T_arg_nexp (Ne_const size); _; _ ])) ->
update_vector_start default_dir (natFromInteger start) (natFromInteger size) value
@@ -2225,292 +2263,292 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
match tag with
| Tag_intro ->
match detaint (in_lenv l_env id) with
- | V_unknown ->
- if is_top_level then
- if name = "0" then
- ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
- else
- let (LMem owner c m s) = l_mem in
- let l_mem = (LMem owner (c+1) m s) in
- ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem c value,
- (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
- else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
+ | V_unknown ->
+ if is_top_level then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level
- then
- if name = "0" then
- ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
- else
- ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
- Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
+ if is_top_level
+ then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
+ Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
end
| Tag_set ->
- match detaint (in_lenv l_env id) with
- | ((V_boxref n t) as v) ->
- if is_top_level
- then ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
- else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
- | V_unknown ->
- if is_top_level then
- if name = "0" then
- ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
- else
- let (LMem owner c m s) = l_mem in
- let l_mem = (LMem owner (c+1) m s) in
- ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem c value,
- (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
- else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
+ match detaint (in_lenv l_env id) with
+ | ((V_boxref n t) as v) ->
+ if is_top_level
+ then ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+ else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
+ | V_unknown ->
+ if is_top_level then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level
- then
- if name = "0" then
- ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
- else
- ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
- Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
- end
+ if is_top_level
+ then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
+ Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
+ end
| Tag_empty ->
- match detaint (in_lenv l_env id) with
- | ((V_boxref n t) as v) ->
- if is_top_level
- then ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
- else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
- | V_unknown ->
- if is_top_level then
- if name = "0" then
- ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
- else
- let (LMem owner c m s) = l_mem in
- let l_mem = (LMem owner (c+1) m s) in
- ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem c value,
- (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
- else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
+ match detaint (in_lenv l_env id) with
+ | ((V_boxref n t) as v) ->
+ if is_top_level
+ then ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+ else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
+ | V_unknown ->
+ if is_top_level then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level
- then
- if name = "0" then
- ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
- else
- ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
- Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
- end
+ if is_top_level
+ then
+ if name = "0" then
+ ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+ else
+ ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),l_mem,l_env),
+ Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
+ end
| Tag_global ->
- (match in_env lets name with
- | Just v ->
- if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
+ (match in_env lets name with
+ | Just v ->
+ if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
| Nothing ->
- let regf =
- match in_env regs name with (*pull the regform with the most specific type annotation from env *)
- | Just(V_register regform) -> regform
- | _ -> Assert_extra.failwith "Register not known in regenv" end in
+ let regf =
+ match in_env regs name with (*pull the regform with the most specific type annotation from env *)
+ | Just(V_register regform) -> regform
+ | _ -> Assert_extra.failwith "Register not known in regenv" end in
let start_pos = reg_start_pos regf in
let reg_size = reg_size regf in
let request =
(Action (Write_reg regf Nothing
- (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env) in
+ (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env) in
if is_top_level then (request,Nothing)
- else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) end)
+ else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) end)
| Tag_extern _ ->
- let regf =
- match in_env regs name with (*pull the regform with the most specific type annotation from env *)
- | Just(V_register regform) -> regform
- | _ -> Assert_extra.failwith "Register not known in regenv" end in
+ let regf =
+ match in_env regs name with (*pull the regform with the most specific type annotation from env *)
+ | Just(V_register regform) -> regform
+ | _ -> Assert_extra.failwith "Register not known in regenv" end in
let start_pos = reg_start_pos regf in
- let reg_size = reg_size regf in
- let request =
+ let reg_size = reg_size regf in
+ let request =
(Action (Write_reg regf Nothing
- (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env) in
+ (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env) in
if is_top_level then (request,Nothing)
- else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
- | Tag_alias ->
- let request =
- (match in_env aliases name with
- | Just (AL_aux aspec (l,_)) ->
- (match aspec with
- | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_id id),_,_,_,_)) as annot'))) subreg ->
- (match in_env subregs id with
- | Just indexes ->
- (match in_env indexes (get_id subreg) with
- | Just ir ->
- (Action
- (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing
- (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
- t_level l_env l_mem Top), l_mem, l_env)
- | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
- | _ ->
- (Error l ("Internal error: alias spec has unknown register type " ^ id), l_mem, l_env) end)
- | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_,_)) as annot'))) subreg ->
- (match in_env subregs id with
- | Just indexes ->
- (match in_env indexes (get_id subreg) with
- | Just ir ->
- (Action
- (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing
- (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
- t_level l_env l_mem Top), l_mem, l_env)
- | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
- | _ -> (Error l ("Internal error: alias spec has unknown register type "^id), l_mem, l_env) end)
- | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
- resolve_outcome (interp_main mode t_level l_env l_mem e)
- (fun v le lm -> match v with
- | V_lit (L_aux (L_num i) _) ->
- let i = natFromInteger i in
- (Action (Write_reg (Reg reg annot' default_dir) (Just (i,i))
- (update_vector_start default_dir i 1 value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
- t_level l_env l_mem Top), l_mem, l_env)
+ else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
+ | Tag_alias ->
+ let request =
+ (match in_env aliases name with
+ | Just (AL_aux aspec (l,_)) ->
+ (match aspec with
+ | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_id id),_,_,_,_)) as annot'))) subreg ->
+ (match in_env subregs id with
+ | Just indexes ->
+ (match in_env indexes (get_id subreg) with
+ | Just ir ->
+ (Action
+ (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing
+ (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+ t_level l_env l_mem Top), l_mem, l_env)
+ | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
+ | _ ->
+ (Error l ("Internal error: alias spec has unknown register type " ^ id), l_mem, l_env) end)
+ | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_,_)) as annot'))) subreg ->
+ (match in_env subregs id with
+ | Just indexes ->
+ (match in_env indexes (get_id subreg) with
+ | Just ir ->
+ (Action
+ (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing
+ (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+ t_level l_env l_mem Top), l_mem, l_env)
+ | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
+ | _ -> (Error l ("Internal error: alias spec has unknown register type "^id), l_mem, l_env) end)
+ | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
+ resolve_outcome (interp_main mode t_level l_env l_mem e)
+ (fun v le lm -> match v with
+ | V_lit (L_aux (L_num i) _) ->
+ let i = natFromInteger i in
+ (Action (Write_reg (Reg reg annot' default_dir) (Just (i,i))
+ (update_vector_start default_dir i 1 value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+ t_level l_env l_mem Top), l_mem, l_env)
| _ -> (Error l "Internal error: alias bit has non number", l_mem, l_env) end)
(fun a -> a)
- | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop ->
- resolve_outcome (interp_main mode t_level l_env l_mem start)
- (fun v lm le ->
- match detaint v with
- | V_lit (L_aux (L_num start) _) ->
- (resolve_outcome (interp_main mode t_level l_env lm stop)
- (fun v le lm ->
- (match detaint v with
- | V_lit (L_aux (L_num stop) _) ->
- let (start,stop) = (natFromInteger start,natFromInteger stop) in
- let size = if start < stop then stop - start +1 else start -stop +1 in
- (Action (Write_reg (Reg reg annot' default_dir) (Just (start,stop))
- (update_vector_start default_dir start size value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
- t_level l_env l_mem Top),
+ | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop ->
+ resolve_outcome (interp_main mode t_level l_env l_mem start)
+ (fun v lm le ->
+ match detaint v with
+ | V_lit (L_aux (L_num start) _) ->
+ (resolve_outcome (interp_main mode t_level l_env lm stop)
+ (fun v le lm ->
+ (match detaint v with
+ | V_lit (L_aux (L_num stop) _) ->
+ let (start,stop) = (natFromInteger start,natFromInteger stop) in
+ let size = if start < stop then stop - start +1 else start -stop +1 in
+ (Action (Write_reg (Reg reg annot' default_dir) (Just (start,stop))
+ (update_vector_start default_dir start size value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+ t_level l_env l_mem Top),
l_mem, l_env)
| _ -> (Error l "Alias slice has non number",l_mem, l_env) end))
(fun a -> a))
| _ -> (Error l "Alias slice has non number",l_mem,l_env) end)
- (fun a -> a)
- | AL_concat (RI_aux (RI_id reg1) (l1,annot1)) (RI_aux (RI_id reg2) annot2) ->
- let val_typ t = match t with
- | T_app "register" (T_args [T_arg_typ t]) -> t
+ (fun a -> a)
+ | AL_concat (RI_aux (RI_id reg1) (l1,annot1)) (RI_aux (RI_id reg2) annot2) ->
+ let val_typ t = match t with
+ | T_app "register" (T_args [T_arg_typ t]) -> t
| T_abbrev _ (T_app "register" (T_args [T_arg_typ t])) -> t
| _ -> Assert_extra.failwith "alias type ill formed" end in
- let (t1,t2) = match (annot1,annot2) with
+ let (t1,t2) = match (annot1,annot2) with
| (Just (t1,_,_,_,_), (_,(Just (t2,_,_,_,_)))) -> (val_typ t1,val_typ t2)
| _ -> Assert_extra.failwith "type annotations ill formed" end in
(match (t1,t2) with
- | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]),
- T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) ->
- (Action
- (Write_reg (Reg reg1 annot1 default_dir) Nothing
- (slice_vector value (natFromInteger b1) (natFromInteger r1)))
- (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
- (fst (to_exp <| mode with track_values =false|> eenv
+ | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]),
+ T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) ->
+ (Action
+ (Write_reg (Reg reg1 annot1 default_dir) Nothing
+ (slice_vector value (natFromInteger b1) (natFromInteger r1)))
+ (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
+ (fst (to_exp <| mode with track_values =false|> eenv
(slice_vector value (natFromInteger (r1+1)) (natFromInteger r2)))))
- annot2)
+ annot2)
t_level l_env l_mem Top), l_mem,l_env)
| _ -> (Error l "Internal error: alias vector types ill formed", l_mem, l_env) end)
| _ -> (Error l "Internal error: alias spec ill formed", l_mem, l_env) end)
- | _ -> (Error l ("Internal error: alias not found for id " ^(get_id id)),l_mem,l_env) end) in
- (request,Nothing)
+ | _ -> (Error l ("Internal error: alias not found for id " ^(get_id id)),l_mem,l_env) end) in
+ (request,Nothing)
| _ ->
- ((Error l ("Internal error: writing to id with tag other than extern, empty, or alias " ^ (get_id id)),
- l_mem,l_env),Nothing)
+ ((Error l ("Internal error: writing to id with tag other than extern, empty, or alias " ^ (get_id id)),
+ l_mem,l_env),Nothing)
end
| LEXP_memory id exps ->
match (exp_list mode t_level (fun exps env -> (E_aux (E_tuple exps) (Unknown,Nothing),env))
- (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
- l_env l_mem [] exps) with
+ (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
+ l_env l_mem [] exps) with
| (Value v,lm,le) ->
(match tag with
| Tag_extern _ ->
let request =
- let effects = (match ef with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in
- let act = if has_wmem_effect effects then (Write_mem id v Nothing value)
- else if has_wmv_effect effects then (Write_memv id value)
- else Assert_extra.failwith "LEXP_memory with neither wmem or wmv event" in
- (Action act
+ let effects = (match ef with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in
+ let act = if has_wmem_effect effects then (Write_mem id v Nothing value)
+ else if has_wmv_effect effects then (Write_memv id value)
+ else Assert_extra.failwith "LEXP_memory with neither wmem or wmv event" in
+ (Action act
(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top),
- lm,l_env) in
+ lm,l_env) in
if is_top_level then (request,Nothing)
- else
+ else
(request,
Just (fun e env->
let (parms,env) = (to_exps mode env (match v with | V_tuple vs -> vs | v -> [v] end)) in
- (LEXP_aux (LEXP_memory id parms) (l,annot), env)))
- | Tag_global ->
+ (LEXP_aux (LEXP_memory id parms) (l,annot), env)))
+ | Tag_global ->
let name = get_id id in
- (match Map.lookup name fdefs with
- | Just(funcls) ->
- let new_vals = match v with
- | V_tuple vs -> V_tuple (vs ++ [value])
- | V_lit (L_aux L_unit _) -> V_tuple [v;value] (*hmmm may be wrong in some code*)
- | v -> V_tuple [v;value] end in
+ (match Map.lookup name fdefs with
+ | Just(funcls) ->
+ let new_vals = match v with
+ | V_tuple vs -> V_tuple (vs ++ [value])
+ | V_lit (L_aux L_unit _) -> V_tuple [v;value] (*hmmm may be wrong in some code*)
+ | v -> V_tuple [v;value] end in
(match find_funcl t_level funcls new_vals with
- | [] -> ((Error l ("No matching pattern for function " ^ name ^
- " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
- | [(env,used_unknown,exp)] ->
- (match (if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with
- | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
- | (Action action stack,lm,le) ->
- (((update_stack (Action action stack)
- (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
- t_level l_env l_mem stack))), l_mem,l_env), Nothing)
- | (e,lm,le) -> ((e,lm,le),Nothing) end)
+ | [] -> ((Error l ("No matching pattern for function " ^ name ^
+ " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
+ | [(env,used_unknown,exp)] ->
+ (match (if mode.eager_eval
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with
+ | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
+ | (Action action stack,lm,le) ->
+ (((update_stack (Action action stack)
+ (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
+ t_level l_env l_mem stack))), l_mem,l_env), Nothing)
+ | (e,lm,le) -> ((e,lm,le),Nothing) end)
| multi_matches ->
- let (lets,taint_env) =
- List.foldr (fun (env,_,exp) (rst,taint_env) ->
- let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
- (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)),
- Nothing)
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)),
+ Nothing)
end)
| Nothing ->
- ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
- | Tag_spec ->
+ ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
+ | Tag_spec ->
let name = get_id id in
- (match Map.lookup name fdefs with
- | Just(funcls) ->
- let new_vals = match v with
- | V_tuple vs -> V_tuple (vs ++ [value])
- | V_lit (L_aux L_unit _) -> V_tuple [v;value] (*hmmm may be wrong in some code*)
- | v -> V_tuple [v;value] end in
+ (match Map.lookup name fdefs with
+ | Just(funcls) ->
+ let new_vals = match v with
+ | V_tuple vs -> V_tuple (vs ++ [value])
+ | V_lit (L_aux L_unit _) -> V_tuple [v;value] (*hmmm may be wrong in some code*)
+ | v -> V_tuple [v;value] end in
(match find_funcl t_level funcls new_vals with
- | [] -> ((Error l ("No matching pattern for function " ^ name ^
- " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
- | [(env,used_unknown,exp)] ->
- (match (if mode.eager_eval
- then (interp_main mode t_level env (emem name) exp)
- else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with
- | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
- | (Action action stack,lm,le) ->
- (((update_stack (Action action stack)
- (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
- t_level l_env l_mem stack))), l_mem,l_env), Nothing)
- | (e,lm,le) -> ((e,lm,le),Nothing) end)
+ | [] -> ((Error l ("No matching pattern for function " ^ name ^
+ " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
+ | [(env,used_unknown,exp)] ->
+ (match (if mode.eager_eval
+ then (interp_main mode t_level env (emem name) exp)
+ else (debug_out (Just name) (Just new_vals) exp t_level (emem name) env)) with
+ | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
+ | (Action action stack,lm,le) ->
+ (((update_stack (Action action stack)
+ (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot)))
+ t_level l_env l_mem stack))), l_mem,l_env), Nothing)
+ | (e,lm,le) -> ((e,lm,le),Nothing) end)
| multi_matches ->
- let (lets,taint_env) =
- List.foldr (fun (env,_,exp) (rst,taint_env) ->
- let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
- let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
- (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)),
- Nothing)
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
+ (interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,non_det_annot annot maybe_id)),
+ Nothing)
end)
| Nothing ->
- ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
+ ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
| _ -> ((Error l "Internal error: unexpected tag for memory or register write", lm,le),Nothing)
end)
| (Action a s,lm, le) ->
- ((Action a s,lm,le),
+ ((Action a s,lm,le),
Just (fun (E_aux e _) env ->
(match e with | E_tuple es -> (LEXP_aux (LEXP_memory id es) (l,annot), env)
| _ -> Assert_extra.failwith "Lexp builder not well formed" end)))
@@ -2519,248 +2557,248 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
let name = get_id id in
match tag with
| Tag_intro ->
- match detaint (in_lenv l_env id) with
- | V_unknown ->
- if is_top_level
+ match detaint (in_lenv l_env id) with
+ | V_unknown ->
+ if is_top_level
then begin
- let (LMem owner c m s) = l_mem in
- let l_mem = (LMem owner (c+1) m s) in
- ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
- (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
end
else ((Error l ("LEXP:cast1: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
+ if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
end
| Tag_set ->
- match detaint (in_lenv l_env id) with
- | ((V_boxref n t) as v) ->
- if is_top_level
- then ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
- else ((Value v, l_mem, l_env),
- Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
- | V_unknown ->
- if is_top_level
+ match detaint (in_lenv l_env id) with
+ | ((V_boxref n t) as v) ->
+ if is_top_level
+ then ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+ else ((Value v, l_mem, l_env),
+ Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
+ | V_unknown ->
+ if is_top_level
then begin
- let (LMem owner c m s) = l_mem in
- let l_mem = (LMem owner (c+1) m s) in
- ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
- (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
end
else ((Error l ("LEXP:cast2: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
+ if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
end
- | Tag_empty ->
- match detaint (in_lenv l_env id) with
- | ((V_boxref n t) as v) ->
- if is_top_level
- then ((Value (V_lit (L_aux L_unit l)),
- update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
- else ((Value v, l_mem, l_env),
- Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
- | V_unknown ->
- if is_top_level
+ | Tag_empty ->
+ match detaint (in_lenv l_env id) with
+ | ((V_boxref n t) as v) ->
+ if is_top_level
+ then ((Value (V_lit (L_aux L_unit l)),
+ update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+ else ((Value v, l_mem, l_env),
+ Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
+ | V_unknown ->
+ if is_top_level
then begin
- let (LMem owner c m s) = l_mem in
- let l_mem = (LMem owner (c+1) m s) in
- ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
- (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+ let (LMem owner c m s) = l_mem in
+ let l_mem = (LMem owner (c+1) m s) in
+ ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value,
+ (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
end
else ((Error l ("LEXP:cast3: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
| v ->
- if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
- else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
+ if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
end
| Tag_extern _ ->
- let regf =
- match in_env regs name with (*pull the regform with the most specific type annotation from env *)
- | Just(V_register regform) -> regform
- | _ -> Assert_extra.failwith "Register not known in regenv" end in
+ let regf =
+ match in_env regs name with (*pull the regform with the most specific type annotation from env *)
+ | Just(V_register regform) -> regform
+ | _ -> Assert_extra.failwith "Register not known in regenv" end in
let start_pos = reg_start_pos regf in
- let reg_size = reg_size regf in
- let request =
+ let reg_size = reg_size regf in
+ let request =
(Action (Write_reg regf Nothing
- (if is_top_level
- then (update_vector_start default_dir start_pos reg_size value)
- else value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env) in
+ (if is_top_level
+ then (update_vector_start default_dir start_pos reg_size value)
+ else value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env) in
if is_top_level then (request,Nothing)
- else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
+ else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
| _ ->
- ((Error l ("Internal error: writing to id not extern or empty " ^(get_id id)),l_mem,l_env),
- Nothing)
+ ((Error l ("Internal error: writing to id not extern or empty " ^(get_id id)),l_mem,l_env),
+ Nothing)
end
| LEXP_vector lexp exp ->
match (interp_main mode t_level l_env l_mem exp) with
| (Value i,lm,le) ->
(match detaint i with
- | V_unknown -> ((Value i,lm,le),Nothing)
+ | V_unknown -> ((Value i,lm,le),Nothing)
| V_lit (L_aux (L_num n) ln) ->
let next_builder le_builder =
(fun e env ->
let (lexp,env) = le_builder e env in
let (ie,env) = to_exp mode env i in
- (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in
- let n = natFromInteger n in
+ (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in
+ let n = natFromInteger n in
(match (create_write_message_or_update mode t_level value l_env lm false lexp) with
| ((Value v_whole,lm,le),maybe_builder) ->
let v = detaint v_whole in
let nth _ = detaint (access_vector v n) in
(match v with
- | V_unknown -> ((Value v_whole,lm,le),Nothing)
- | V_boxref i _ ->
- (match (in_mem lm i,is_top_level,maybe_builder) with
- | ((V_vector _ _ _ as vec),true,_) ->
- let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
- ((Value (V_lit (L_aux L_unit Unknown)),
- update_mem mode.track_lmem lm i new_vec, l_env), Nothing)
- | ((V_track (V_vector _ _ _ as vec) r), true,_) ->
- let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
- ((Value (V_lit (L_aux L_unit Unknown)),
- update_mem mode.track_lmem lm i (taint new_vec r),l_env),Nothing)
- | ((V_vector _ _ _ as vec),false, Just lexp_builder) ->
- ((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder))
- | (v,_,_) ->
- Assert_extra.failwith("no vector findable in set bit, found " ^ (string_of_value v))
- end )
+ | V_unknown -> ((Value v_whole,lm,le),Nothing)
+ | V_boxref i _ ->
+ (match (in_mem lm i,is_top_level,maybe_builder) with
+ | ((V_vector _ _ _ as vec),true,_) ->
+ let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_mem mode.track_lmem lm i new_vec, l_env), Nothing)
+ | ((V_track (V_vector _ _ _ as vec) r), true,_) ->
+ let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_mem mode.track_lmem lm i (taint new_vec r),l_env),Nothing)
+ | ((V_vector _ _ _ as vec),false, Just lexp_builder) ->
+ ((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder))
+ | (v,_,_) ->
+ Assert_extra.failwith("no vector findable in set bit, found " ^ (string_of_value v))
+ end )
| V_vector inc m vs ->
- (match (nth(),is_top_level,maybe_builder) with
- | (V_register regform,true,_) ->
- let start_pos = reg_start_pos regform in
- let reg_size = reg_size regform in
- ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env),
- Nothing)
- | (V_register regform,false,Just lexp_builder) ->
- let start_pos = reg_start_pos regform in
- let reg_size = reg_size regform in
- ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env),
+ (match (nth(),is_top_level,maybe_builder) with
+ | (V_register regform,true,_) ->
+ let start_pos = reg_start_pos regform in
+ let reg_size = reg_size regform in
+ ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env),
+ Nothing)
+ | (V_register regform,false,Just lexp_builder) ->
+ let start_pos = reg_start_pos regform in
+ let reg_size = reg_size regform in
+ ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env),
Just (next_builder lexp_builder))
- | (V_boxref n t,true,_) ->
- ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env),
- Nothing)
- | (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing)
- | (v,true,_) ->
- ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
- | ((V_boxref n t),false, Just lexp_builder) ->
- ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
- | (v,false, Just lexp_builder) ->
+ | (V_boxref n t,true,_) ->
+ ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env),
+ Nothing)
+ | (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing)
+ | (v,true,_) ->
+ ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
+ | ((V_boxref n t),false, Just lexp_builder) ->
+ ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+ | (v,false, Just lexp_builder) ->
((Value v,lm,le), Just (next_builder lexp_builder))
| _ -> Assert_extra.failwith "Vector assignment logic incomplete"
end)
- | V_vector_sparse n m inc vs d ->
+ | V_vector_sparse n m inc vs d ->
(match (nth(),is_top_level,maybe_builder) with
- | (V_register regform,true,_) ->
- let start_pos = reg_start_pos regform in
- let reg_size = reg_size regform in
- ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env),Nothing)
- | (V_register regform,false,Just lexp_builder) ->
- let start_pos = reg_start_pos regform in
- let reg_size = reg_size regform in
- ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
- (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
- l_mem,l_env),
- Just (next_builder lexp_builder))
- | (V_boxref n t,true,_) ->
- ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env),
- Nothing)
- | (v,true,_) ->
- ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),
- lm,l_env), Nothing)
- | ((V_boxref n t),false, Just lexp_builder) ->
- ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
- | (v,false, Just lexp_builder) ->
+ | (V_register regform,true,_) ->
+ let start_pos = reg_start_pos regform in
+ let reg_size = reg_size regform in
+ ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env),Nothing)
+ | (V_register regform,false,Just lexp_builder) ->
+ let start_pos = reg_start_pos regform in
+ let reg_size = reg_size regform in
+ ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value))
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
+ l_mem,l_env),
+ Just (next_builder lexp_builder))
+ | (V_boxref n t,true,_) ->
+ ((Value (V_lit (L_aux L_unit Unknown)), update_mem mode.track_lmem lm n value, l_env),
+ Nothing)
+ | (v,true,_) ->
+ ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),
+ lm,l_env), Nothing)
+ | ((V_boxref n t),false, Just lexp_builder) ->
+ ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+ | (v,false, Just lexp_builder) ->
((Value v,lm,le), Just (next_builder lexp_builder))
| _ -> Assert_extra.failwith "Vector assignment logic incomplete"
end)
| v ->
- ((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing)
- end)
+ ((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing)
+ end)
| ((Action a s,lm,le),Just lexp_builder) ->
(match (a,is_top_level) with
| ((Write_reg regf Nothing value),true) ->
- ((Action (Write_reg regf (Just (n,n))
- (if (vector_length value) = 1
- then (update_vector_start default_dir n 1 value)
- else (access_vector value n))) s, lm,le), Nothing)
+ ((Action (Write_reg regf (Just (n,n))
+ (if (vector_length value) = 1
+ then (update_vector_start default_dir n 1 value)
+ else (access_vector value n))) s, lm,le), Nothing)
| ((Write_reg regf Nothing value),false) ->
- ((Action (Write_reg regf (Just (n,n))
- (if (vector_length value) = 1
- then (update_vector_start default_dir n 1 value)
- else (access_vector value n))) s,lm,le),
- Just (next_builder lexp_builder))
+ ((Action (Write_reg regf (Just (n,n))
+ (if (vector_length value) = 1
+ then (update_vector_start default_dir n 1 value)
+ else (access_vector value n))) s,lm,le),
+ Just (next_builder lexp_builder))
| ((Write_mem id a Nothing value),true) ->
- ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
+ ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
| ((Write_mem id a Nothing value),false) ->
- ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
+ ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
| _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
| e -> e end)
| v ->
- ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing) end)
+ ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing) end)
| (Action a s,lm,le) ->
- ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
+ ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
| e -> (e,Nothing) end
| LEXP_vector_range lexp exp1 exp2 ->
match (interp_main mode t_level l_env l_mem exp1) with
| (Value i1, lm, le) ->
(match detaint i1 with
- | V_unknown -> ((Value i1,lm,le),Nothing)
+ | V_unknown -> ((Value i1,lm,le),Nothing)
| V_lit (L_aux (L_num n1) ln1) ->
(match (interp_main mode t_level l_env l_mem exp2) with
| (Value i2,lm,le) ->
(match detaint i2 with
- | V_unknown -> ((Value i2,lm,le),Nothing)
+ | V_unknown -> ((Value i2,lm,le),Nothing)
| V_lit (L_aux (L_num n2) ln2) ->
let next_builder le_builder =
- (fun e env ->
+ (fun e env ->
let (e1,env) = to_exp mode env i1 in
let (e2,env) = to_exp mode env i2 in
let (lexp,env) = le_builder e env in
(LEXP_aux (LEXP_vector_range lexp e1 e2) (l,annot), env)) in
- let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
+ let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
(match (create_write_message_or_update mode t_level value l_env lm false lexp) with
| ((Value v,lm,le), Just lexp_builder) ->
- (match (detaint v,is_top_level) with
+ (match (detaint v,is_top_level) with
| (V_vector m inc vs,true) ->
((Value (V_lit (L_aux L_unit Unknown)),
- update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing)
- | (V_boxref _ _, true) ->
- ((Value (V_lit (L_aux L_unit Unknown)),
- update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing)
+ update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing)
+ | (V_boxref _ _, true) ->
+ ((Value (V_lit (L_aux L_unit Unknown)),
+ update_vector_slice mode.track_lmem v value n1 n2 lm, l_env), Nothing)
| (V_vector m inc vs,false) ->
((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
| (V_register regform,true) ->
- let start_pos = reg_start_pos regform in
+ let start_pos = reg_start_pos regform in
let reg_size = reg_size regform in
- ((Action (Write_reg regform (Just (n1,n2)) (update_vector_start default_dir start_pos reg_size v))
- (mk_thunk l annot t_level l_env l_mem),
- l_mem,l_env),
+ ((Action (Write_reg regform (Just (n1,n2)) (update_vector_start default_dir start_pos reg_size v))
+ (mk_thunk l annot t_level l_env l_mem),
+ l_mem,l_env),
Just (next_builder lexp_builder))
- | (V_unknown,_) ->
- let inc = n1 < n2 in
- let start = if inc then n1 else (n2-1) in
- let size = if inc then n2-n1 +1 else n1 -n2 +1 in
- ((Value (V_vector start (if inc then IInc else IDec) (List.replicate size V_unknown)),
- lm,l_env),Nothing)
+ | (V_unknown,_) ->
+ let inc = n1 < n2 in
+ let start = if inc then n1 else (n2-1) in
+ let size = if inc then n2-n1 +1 else n1 -n2 +1 in
+ ((Value (V_vector start (if inc then IInc else IDec) (List.replicate size V_unknown)),
+ lm,l_env),Nothing)
| _ -> ((Error l "Vector required",lm,le),Nothing) end)
| ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
- let len = (if n1 < n2 then n2 -n1 else n1 - n2) +1 in
+ let len = (if n1 < n2 then n2 -n1 else n1 - n2) +1 in
((Action
- (Write_reg regf (Just (n1,n2))
- (if (vector_length value) <= len
- then (update_vector_start default_dir n1 len value)
- else (slice_vector value n1 n2))) s,lm,le),
- Just (next_builder lexp_builder))
+ (Write_reg regf (Just (n1,n2))
+ (if (vector_length value) <= len
+ then (update_vector_start default_dir n1 len value)
+ else (slice_vector value n1 n2))) s,lm,le),
+ Just (next_builder lexp_builder))
| ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
((Action (Write_mem id a (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
| ((Action a s,lm,le), Just lexp_builder) ->
@@ -2784,7 +2822,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(LEXP_aux (LEXP_field lexp id) (l,annot), env)) in
match (in_env (env_from_list fexps) (get_id id),is_top_level) with
| (Just (V_boxref n t),true) ->
- ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem lm n value, l_env),Nothing)
+ ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem lm n value, l_env),Nothing)
| (Just (V_boxref n t),false) -> ((Value (in_mem lm n),lm,l_env),next_builder)
| (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing)
| (Just v,false) -> ((Value v,lm,l_env),next_builder)
@@ -2797,30 +2835,30 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Read_mem _ _ _ -> ((Action a s,lm,le), next_builder)
| Call_extern _ _ -> ((Action a s,lm,le), next_builder)
| Write_reg ((Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value ->
- match in_env subregs id' with
- | Just(indexes) ->
- match in_env indexes (get_id id) with
- | Just ir ->
- ((Action
- (Write_reg (SubReg id regf ir) Nothing
- (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s,
- lm,le),
- (if is_top_level then Nothing else next_builder))
- | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
- end
+ match in_env subregs id' with
+ | Just(indexes) ->
+ match in_env indexes (get_id id) with
+ | Just ir ->
+ ((Action
+ (Write_reg (SubReg id regf ir) Nothing
+ (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s,
+ lm,le),
+ (if is_top_level then Nothing else next_builder))
+ | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
+ end
| Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
| Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value ->
- match in_env subregs id' with
- | Just(indexes) ->
- match in_env indexes (get_id id) with
- | Just ir ->
- ((Action
- (Write_reg (SubReg id regf ir) Nothing
- (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s,
- lm,le),
- (if is_top_level then Nothing else next_builder))
- | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
- end
+ match in_env subregs id' with
+ | Just(indexes) ->
+ match in_env indexes (get_id id) with
+ | Just ir ->
+ ((Action
+ (Write_reg (SubReg id regf ir) Nothing
+ (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s,
+ lm,le),
+ (if is_top_level then Nothing else next_builder))
+ | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
+ end
| Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
| _ -> ((Error l "Internal error, unrecognized write, no matching action",lm,le),Nothing)
end
@@ -2845,7 +2883,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
| _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
| (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
| e -> (e,Nothing) end
-end
+end
and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in
@@ -2860,30 +2898,30 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
| AL_subreg (RI_aux (RI_id reg) (li,((Just (t,_,_,_,_)) as annot'))) subreg ->
let reg_ti = get_reg_typ_name t in
(match in_env subregs reg_ti with
- | Just indexes ->
- (match in_env indexes (get_id subreg) with
- | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing) stack, l_mem, l_env)
- | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
- | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
+ | Just indexes ->
+ (match in_env indexes (get_id subreg) with
+ | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing) stack, l_mem, l_env)
+ | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
+ | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
| AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
resolve_outcome (interp_main mode t_level l_env l_mem e)
(fun v le lm -> match v with
- | V_lit (L_aux (L_num i) _) ->
- let i = natFromInteger i in
+ | V_lit (L_aux (L_num i) _) ->
+ let i = natFromInteger i in
(Action (Read_reg (Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env)
| _ -> Assert_extra.failwith "alias bit did not reduce to number" end)
(fun a -> a) (*Should not currently happen as type system enforces constants*)
| AL_slice (RI_aux (RI_id reg) (_,annot')) start stop ->
resolve_outcome (interp_main mode t_level l_env l_mem start)
(fun v lm le ->
- match v with
- | V_lit (L_aux (L_num start) _) ->
- (resolve_outcome
- (interp_main mode t_level l_env lm stop)
- (fun v le lm ->
- (match v with
- | V_lit (L_aux (L_num stop) _) ->
- let (start,stop) = (natFromInteger start,natFromInteger stop) in
+ match v with
+ | V_lit (L_aux (L_num start) _) ->
+ (resolve_outcome
+ (interp_main mode t_level l_env lm stop)
+ (fun v le lm ->
+ (match v with
+ | V_lit (L_aux (L_num stop) _) ->
+ let (start,stop) = (natFromInteger start,natFromInteger stop) in
(Action (Read_reg (Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env)
| _ -> Assert_extra.failwith ("Alias slice evaluted non-lit " ^ (string_of_value v))
end))
@@ -2893,10 +2931,10 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
(fun a -> a) (*Neither action function should occur, due to above*)
| AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) ->
(Action (Read_reg (Reg reg1 annot1 default_dir) Nothing)
- (Hole_frame redex_id
- (E_aux (E_vector_append (E_aux (E_id redex_id) (l1, (intern_annot annot1)))
- (E_aux (E_id reg2) annot2))
- (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env)
+ (Hole_frame redex_id
+ (E_aux (E_vector_append (E_aux (E_id redex_id) (l1, (intern_annot annot1)))
+ (E_aux (E_id reg2) annot2))
+ (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env)
| _ -> Assert_extra.failwith "alias spec not well formed"
end
@@ -2905,12 +2943,12 @@ let rec eval_toplevel_let handle_action tlevel env mem lbind =
| ((Value v, lm, (LEnv _ le)),_) -> Just le
| ((Action a s,lm,le), Just le_builder) ->
(match handle_action (Action a s) with
- | Just value ->
- (match s with
- | Hole_frame id exp tl lenv lmem s ->
+ | Just value ->
+ (match s with
+ | Hole_frame id exp tl lenv lmem s ->
eval_toplevel_let handle_action tl (add_to_env (id,value) lenv) lmem (le_builder exp)
| _ -> Assert_extra.failwith "Top level def evaluation created a thunk frame" end)
- | Nothing -> Nothing end)
+ | Nothing -> Nothing end)
| _ -> Nothing end
let rec to_global_letbinds handle_action (Defs defs) t_level =
@@ -2921,22 +2959,22 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
match def with
| DEF_val lbind ->
match eval_toplevel_let handle_action t_level eenv (emem "global_letbinds") lbind with
- | Just le ->
- to_global_letbinds handle_action (Defs defs)
- (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases)
- | Nothing ->
- to_global_letbinds handle_action (Defs defs)
- (Env fdefs instrs default_dir lets regs ctors subregs aliases) end
+ | Just le ->
+ to_global_letbinds handle_action (Defs defs)
+ (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases)
+ | Nothing ->
+ to_global_letbinds handle_action (Defs defs)
+ (Env fdefs instrs default_dir lets regs ctors subregs aliases) end
| DEF_type (TD_aux tdef _) ->
match tdef with
| TD_enum id ns ids _ ->
- let typ = T_id (get_id id) in
+ let typ = T_id (get_id id) in
let enum_vals =
- Map.fromList
- (snd
- (List.foldl (fun (c,rst) eid -> (1+c,(get_id eid,V_ctor eid typ (C_Enum c) unitv)::rst)) (0,[]) ids)) in
+ Map.fromList
+ (snd
+ (List.foldl (fun (c,rst) eid -> (1+c,(get_id eid,V_ctor eid typ (C_Enum c) unitv)::rst)) (0,[]) ids)) in
to_global_letbinds
- handle_action (Defs defs)
+ handle_action (Defs defs)
(Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases)
| _ -> to_global_letbinds handle_action (Defs defs) t_level end
| _ -> to_global_letbinds handle_action (Defs defs) t_level
@@ -2958,8 +2996,8 @@ let to_top_env external_functions defs =
(extract_instructions "execute" defs)
direction
Map.empty (* empty letbind and enum values, call below will fill in any *)
- (to_registers direction defs)
- (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+ (to_registers direction defs)
+ (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
let (o,t_level) = to_global_letbinds (external_functions direction) defs t_level in
match o with
| (Value _,_,_) -> (Nothing,t_level)
@@ -2988,7 +3026,7 @@ let rec resume_with_env mode stack value =
| (Hole_frame id exp t_level env mem stack, Nothing) ->
match resume_with_env mode stack Nothing with
| (Value v,e) ->
- match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,e) -> (o,e) end
+ match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,e) -> (o,e) end
| (Action action stack,e) -> (Action action (Hole_frame id exp t_level env mem stack),e)
| (Error l s,e) -> (Error l s,e)
end
@@ -3020,7 +3058,7 @@ let rec resume mode stack value =
| (Hole_frame id exp t_level env mem stack, Nothing) ->
match resume mode stack Nothing with
| (Value v,_,_) ->
- interp_main mode t_level (add_to_env (id,v) env) mem exp
+ interp_main mode t_level (add_to_env (id,v) env) mem exp
| (Action action stack,lm,le) -> (Action action (Hole_frame id exp t_level env mem stack),lm,le)
| (Error l s,lm,le) -> (Error l s,lm,le)
end
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index fcf5dd69..9ed4efed 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -30,7 +30,7 @@ let bitl_to_ibit = function
| Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
| Bitl_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown))
| Bitl_undef -> (Interp.V_lit (L_aux L_undef Interp_ast.Unknown))
- | Bitl_unknown -> Interp.V_unknown
+ | Bitl_unknown -> Interp.V_unknown
end
let bit_to_ibit = function
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index dae1ec80..61074ca0 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1029,6 +1029,7 @@ let rec bytes_of_bits bits = match bits with
| [] -> []
| b0::b1::b2::b3::b4::b5::b6::b7::bits ->
(Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits)
+ | _ -> failwith "bytes_of_bits not given bits divisible by 8"
end
val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*)
@@ -1036,6 +1037,7 @@ let rec byte_lifteds_of_bit_lifteds bits = match bits with
| [] -> []
| b0::b1::b2::b3::b4::b5::b6::b7::bits ->
(Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits)
+ | _ -> failwith "byte_lifteds of bit_lifteds not given bits divisible by 8"
end
@@ -1142,7 +1144,9 @@ let clear_low_order_bits_of_address a =
let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in
let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in
Address bytes (integer_of_byte_list bytes)
- end
+ | _ -> failwith "Byte does not contain 8 bits"
+ end
+ | _ -> failwith "Address does not contain 8 bytes"
end
val translate_address : context -> end_flag -> string -> address -> maybe address * maybe nat
@@ -1213,8 +1217,9 @@ let address_lifted_of_register_value (rv:register_value) : maybe address_lifted
else
Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits)
(if List.all concretizable_bitl rv.rv_bits
- then let (Just(bits)) = (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) in
- Just (integer_of_bit_list bits)
+ then match (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) with
+ | (Just(bits)) -> Just (integer_of_bit_list bits)
+ | Nothing -> Nothing end
else Nothing))
val address_of_address_lifted : address_lifted -> maybe address
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 2d43596a..c84588ef 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -891,6 +891,7 @@ let library_functions direction = [
("bitwise_or_bit", bitwise_binop_bit (||) "|");
("bitwise_xor_bit", bitwise_binop_bit xor "^");
("lt", compare_op (<));
+ ("lt_signed", compare_op (<));
("gt", compare_op (>));
("lteq", compare_op (<=));
("gteq", compare_op (>=));
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 8b24d692..13e697d4 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -87,7 +87,9 @@ let doc_effect (BE_aux (e,_)) =
| BE_depend -> "depend"
| BE_undef -> "undef"
| BE_unspec -> "unspec"
- | BE_nondet -> "nondet")
+ | BE_escape -> "escape"
+ | BE_nondet -> "nondet"
+ | BE_lset -> "(*lset*)")
let doc_effects (Effect_aux(e,_)) = match e with
| Effect_var v -> doc_var v
@@ -110,9 +112,6 @@ let doc_typ, doc_atomic_typ, doc_nexp =
| Typ_tup typs -> parens (separate_map comma_sp app_typ typs)
| _ -> app_typ ty
and app_typ ((Typ_aux (t, _)) as ty) = match t with
- | Typ_app(id,args) ->
- (* trailing space to avoid >> token in case of nested app types *)
- (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space
| Typ_app(Id_aux (Id "vector", _), [
Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
@@ -120,11 +119,14 @@ let doc_typ, doc_atomic_typ, doc_nexp =
Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
(doc_id id) ^^
(brackets (if equal n zero_big then doc_int m
- else doc_op colon (doc_int n) (doc_int (add n (sub m one_big)))))
+ else doc_op colon (doc_int n) (doc_int (add n (sub m one_big)))))
| Typ_app(Id_aux (Id "range", _), [
Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
Typ_arg_aux(Typ_arg_nexp m, _);]) ->
(squarebars (if equal n zero_big then nexp m else doc_op colon (doc_int n) (nexp m)))
+ | Typ_app(id,args) ->
+ (* trailing space to avoid >> token in case of nested app types *)
+ (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space
| _ -> atomic_typ ty
and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
| Typ_id id -> doc_id id
@@ -163,9 +165,10 @@ let doc_typ, doc_atomic_typ, doc_nexp =
minus ^^ (atomic_nexp_typ n1)
| _ -> atomic_nexp_typ ne
and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
- | Nexp_var v -> doc_var v
- | Nexp_constant i -> doc_int i
- | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _ ->
+ | Nexp_id id -> doc_id id
+ | Nexp_var v -> doc_var v
+ | Nexp_constant i -> doc_int i
+ | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _ ->
group (parens (nexp ne))
(* expose doc_typ, doc_atomic_typ and doc_nexp *)
@@ -314,7 +317,7 @@ let doc_exp, doc_let =
string "in " ^^ doc_ord order
]
)) ^/^
- (exp env add_red exp4)
+ (exp env add_red exp4)
| E_let(leb,e) -> doc_op (string "in") (let_exp env add_red leb) (exp env add_red e)
| _ -> group (parens (exp env add_red expr))
and app_exp env add_red ((E_aux(e,_)) as expr) = match e with
@@ -342,10 +345,10 @@ let doc_exp, doc_let =
| E_id id ->
(match id with
| Id_aux(Id("0"), _) ->
- (match Interp.in_lenv env id with
- | Interp.V_unknown -> string (add_red "[_]")
- | v -> (*string ("\x1b[1;31m" ^ Interp.string_of_value v ^ "\x1b[m")*)
- string (add_red (Interp.string_of_value v)))
+ (match Interp.in_lenv env id with
+ | Interp.V_unknown -> string (add_red "[_]")
+ | v -> (*string ("\x1b[1;31m" ^ Interp.string_of_value v ^ "\x1b[m")*)
+ string (add_red (Interp.string_of_value v)))
| _ -> doc_id id)
| E_lit lit -> doc_lit lit
| E_cast(typ,e) ->
@@ -365,19 +368,28 @@ let doc_exp, doc_let =
| E_vector exps ->
let default_print _ = brackets (separate_map comma (exp env add_red) exps) in
(match exps with
- | [] -> default_print ()
- | es ->
- if (List.for_all (fun e -> match e with (E_aux(E_lit(L_aux((L_one | L_zero),_)),_)) -> true | _ -> false) es)
- then
- utf8string
- ("0b" ^
- (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst | L_undef -> "u"^rst) exps ""))
- else default_print ())
+ | [] -> default_print ()
+ | es ->
+ if (List.for_all
+ (fun e -> match e with
+ | (E_aux(E_lit(L_aux((L_one | L_zero | L_undef),_)),_)) -> true
+ | _ -> false) es)
+ then
+ utf8string
+ ("0b" ^
+ (List.fold_right (fun (E_aux(e,_)) rst ->
+ match e with
+ | E_lit(L_aux(l, _)) -> (match l with | L_one -> "1"^rst
+ | L_zero -> "0"^rst
+ | L_undef -> "u"^rst
+ | _ -> failwith "bit vector not just bit values")
+ | _ -> failwith "bit vector not all lits") exps ""))
+ else default_print ())
| E_vector_indexed (iexps, (Def_val_aux(default,_))) ->
let default_string =
(match default with
- | Def_val_empty -> string ""
- | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env add_red e)]) in
+ | Def_val_empty -> string ""
+ | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env add_red e)]) in
let iexp (i,e) = doc_op equals (doc_int i) (exp env add_red e) in
brackets (concat [(separate_map comma iexp iexps);default_string])
| E_vector_update(v,e1,e2) ->
@@ -424,7 +436,8 @@ let doc_exp, doc_let =
failwith ("unexpected app_infix operator " ^ (pp_format_id op))
(* doc_op (doc_id op) (exp l) (exp r) *)
(* XXX missing case *)
- | E_internal_exp _ -> assert false
+ | E_comment _ | E_comment_struc _ -> string ""
+ | _-> failwith "internal expression escpaed"
and let_exp env add_red (LB_aux(lb,_)) = match lb with
| LB_val_explicit(ts,pat,e) ->
@@ -467,6 +480,7 @@ let doc_exp, doc_let =
let doc_default (DT_aux(df,_)) = match df with
| DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v]
| DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id]
+ | DT_order o -> separate space [string "default"; string "Order"; doc_ord o]
let doc_spec (VS_aux(v,_)) = match v with
| VS_val_spec(ts,id) ->
@@ -549,8 +563,9 @@ let doc_fundef env add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) =
string "effect"; doc_effects_opt efa;
clauses]
-let doc_dec (DEC_aux(DEC_reg(typ,id),_)) =
- separate space [string "register"; doc_atomic_typ typ; doc_id id]
+let doc_dec (DEC_aux(d,_)) = match d with
+ | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id]
+ | _ -> failwith "interpreter printing out declarations unexpectedly"
let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with
| SD_scattered_function (r, typa, efa, id) ->
@@ -570,16 +585,22 @@ let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with
string "member"; doc_type_union tu]
| SD_scattered_end id -> string "end" ^^ space ^^ doc_id id
-let doc_def env add_red def = group (match def with
+let rec doc_def env add_red def = group (match def with
| DEF_default df -> doc_default df
| DEF_spec v_spec -> doc_spec v_spec
| DEF_type t_def -> doc_typdef t_def
+ | DEF_kind k_def -> failwith "interpreter unexpectedly printing kind def"
| DEF_fundef f_def -> doc_fundef env add_red f_def
| DEF_val lbind -> doc_let env add_red lbind
| DEF_reg_dec dec -> doc_dec dec
| DEF_scattered sdef -> doc_scattered env add_red sdef
+ | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env add_red comm_dec ^^ string "*)"
) ^^ hardline
+and doc_comm_dec env add_red dec = match dec with
+ | DC_comm s -> string s
+ | DC_comm_struct d -> doc_def env add_red d
+
let doc_defs env add_red (Defs(defs)) =
separate_map hardline (doc_def env add_red) defs
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:02:42 +0000