summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail_operators_mwords.lem74
-rw-r--r--src/gen_lib/sail_values.lem1
-rw-r--r--src/gen_lib/state.lem2
-rw-r--r--src/lem_interp/pretty_interp.ml32
-rw-r--r--src/lem_interp/printing_functions.ml3
-rw-r--r--src/lem_interp/printing_functions.mli1
-rw-r--r--src/lem_interp/run_interp.ml45
-rw-r--r--src/lem_interp/sail_impl_base.lem5
-rw-r--r--src/monomorphise.ml311
-rw-r--r--src/process_file.ml3
-rw-r--r--src/process_file.mli1
-rw-r--r--src/sail.ml3
12 files changed, 295 insertions, 186 deletions
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 44ae9d7c..f10ed9f7 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -118,9 +118,9 @@ let bitwise_not (Bitvector bs start is_inc) =
let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
Bitvector (op bsl bsr) start is_inc
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
+let bitwise_and x = bitwise_binop lAnd x
+let bitwise_or x = bitwise_binop lOr x
+let bitwise_xor x = bitwise_binop lXor x
let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
let unsigned_big = unsigned
@@ -317,9 +317,9 @@ let arith_op_range_vec_range op sign l r = op l (to_num sign r)
* add_range_vec_range_signed
* minus_range_vec_range
*)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
+let add_IVI x = arith_op_range_vec_range integerAdd false x
+let addS_IVI x = arith_op_range_vec_range integerAdd true x
+let minus_IVI x = arith_op_range_vec_range integerMinus false x
let arith_op_vec_range_range op sign l r = op (to_num sign l) r
@@ -327,9 +327,9 @@ let arith_op_vec_range_range op sign l r = op (to_num sign l) r
* add_vec_range_range_signed
* minus_vec_range_range
*)
-let add_VII = arith_op_vec_range_range integerAdd false
-let addS_VII = arith_op_vec_range_range integerAdd true
-let minus_VII = arith_op_vec_range_range integerMinus false
+let add_VII x = arith_op_vec_range_range integerAdd false x
+let addS_VII x = arith_op_vec_range_range integerAdd true x
+let minus_VII x = arith_op_vec_range_range integerMinus false x
@@ -340,8 +340,8 @@ let arith_op_vec_vec_range op sign l r =
(* add_vec_vec_range
* add_vec_vec_range_signed
*)
-let add_VVI = arith_op_vec_vec_range integerAdd false
-let addS_VVI = arith_op_vec_vec_range integerAdd true
+let add_VVI x = arith_op_vec_vec_range integerAdd false x
+let addS_VVI x = arith_op_vec_vec_range integerAdd true x
let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
let l' = to_num sign l in
@@ -352,9 +352,9 @@ let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
* add_vec_bit_signed
* minus_vec_bit_signed
*)
-let add_VBV = arith_op_vec_bit integerAdd false 1
-let addS_VBV = arith_op_vec_bit integerAdd true 1
-let minus_VBV = arith_op_vec_bit integerMinus true 1
+let add_VBV x = arith_op_vec_bit integerAdd false 1 x
+let addS_VBV x = arith_op_vec_bit integerAdd true 1 x
+let minus_VBV x = arith_op_vec_bit integerMinus true 1 x
(* TODO: these can't be done directly in Lem because of the one_more size calculation
val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
@@ -432,9 +432,9 @@ let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
Bitvector (rotateLeft n bs) start is_inc
end
-let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
-let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
-let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
+let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*)
+let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*)
+let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*)
let shiftl = bitwise_leftshift
@@ -508,37 +508,37 @@ let compare_op_vec op sign (l,r) =
let (l',r') = (to_num sign l, to_num sign r) in
compare_op op (l',r')
-let lt_vec = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
+let lt_vec x = compare_op_vec (<) true x
+let gt_vec x = compare_op_vec (>) true x
+let lteq_vec x = compare_op_vec (<=) true x
+let gteq_vec x = compare_op_vec (>=) true x
-let lt_vec_signed = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
+let lt_vec_signed x = compare_op_vec (<) true x
+let gt_vec_signed x = compare_op_vec (>) true x
+let lteq_vec_signed x = compare_op_vec (<=) true x
+let gteq_vec_signed x = compare_op_vec (>=) true x
+let lt_vec_unsigned x = compare_op_vec (<) false x
+let gt_vec_unsigned x = compare_op_vec (>) false x
+let lteq_vec_unsigned x = compare_op_vec (<=) false x
+let gteq_vec_unsigned x = compare_op_vec (>=) false x
let lt_svec = lt_vec_signed
let compare_op_vec_range op sign (l,r) =
compare_op op ((to_num sign l),r)
-let lt_vec_range = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
+let lt_vec_range x = compare_op_vec_range (<) true x
+let gt_vec_range x = compare_op_vec_range (>) true x
+let lteq_vec_range x = compare_op_vec_range (<=) true x
+let gteq_vec_range x = compare_op_vec_range (>=) true x
let compare_op_range_vec op sign (l,r) =
compare_op op (l, (to_num sign r))
-let lt_range_vec = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
+let lt_range_vec x = compare_op_range_vec (<) true x
+let gt_range_vec x = compare_op_range_vec (>) true x
+let lteq_range_vec x = compare_op_range_vec (<=) true x
+let gteq_range_vec x = compare_op_range_vec (>=) true x
val eq : forall 'a. Eq 'a => 'a * 'a -> bool
let eq (l,r) = (l = r)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index e2cbb98a..4d3ddbce 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -260,7 +260,6 @@ let vec_to_bvec (Vector elems start is_inc) =
(*** Vector operations *)
-
(* Bytes and addresses *)
val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 914955e0..0ea65551 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -181,7 +181,7 @@ val barrier : forall 'regs. barrier_kind -> M 'regs unit
let barrier _ = return ()
val footprint : forall 'regs. M 'regs unit
-let footprint = return ()
+let footprint s = return () s
val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index a51598b3..9f1ea3e3 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -127,36 +127,6 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
;;
-let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function
- | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory)
- | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | Interp_ast.V_tuple l ->
- let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in
- sprintf "(%s)" repr
- | Interp_ast.V_list l ->
- let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in
- sprintf "[||%s||]" repr
- | Interp_ast.V_vector (first_index, inc, l) ->
- let last_index = (if (Interp_ast.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index in
- let repr =
- try bitvec_to_string l
- with Failure _ ->
- sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in
- sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index)
- | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) ->
- val_to_string_internal mem (Interp_lib.fill_in_sparse v)
- | Interp_ast.V_record(_, l) ->
- let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in
- let repr = String.concat "; " (List.map pp l) in
- sprintf "{%s}" repr
- | Interp_ast.V_ctor (id,_,_, value) ->
- sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value)
- | Interp_ast.V_register _ | Interp_ast.V_register_alias _ ->
- sprintf "reg-as-value"
- | Interp_ast.V_unknown -> "unknown"
- | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v)
-;;
-
(****************************************************************************
* PPrint-based source-to-source pretty printer
****************************************************************************)
@@ -582,7 +552,7 @@ let doc_exp, doc_let =
(* XXX missing case *)
| E_comment _ | E_comment_struc _ -> string ""
| E_internal_value v ->
- string (val_to_string_internal mem v)
+ string (Interp.string_of_value v)
| _-> failwith "internal expression escaped"
and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 79a86113..a19256a2 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -49,7 +49,6 @@ open Interp_interface ;;
open Nat_big_num ;;
-let val_to_string_internal = Pretty_interp.val_to_string_internal ;;
let lit_to_string = Pretty_interp.lit_to_string ;;
let id_to_string = Pretty_interp.id_to_string ;;
let loc_to_string = Pretty_interp.loc_to_string ;;
@@ -451,7 +450,7 @@ let local_variables_to_string (IState(stack,_)) =
String.concat ", " (option_map (fun (id,value)->
match id with
| "0" -> None (*Let's not print out the context hole again*)
- | _ -> Some (id ^ "=" ^ val_to_string_internal mem value)) (Pmap.bindings_list env))
+ | _ -> Some (id ^ "=" ^ Interp.string_of_value value)) (Pmap.bindings_list env))
let instr_parm_to_string (name, typ, value) =
name ^"="^
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index 85744d61..f1a0cd4a 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -10,7 +10,6 @@ val loc_to_string : l -> string
val get_loc : tannot exp -> string
(*interp_interface.value to string*)
val reg_value_to_string : register_value -> string
-val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string
(*(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
val val_to_hex_string : value0 -> string*)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 6f5ca07a..f61d9aaf 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -114,33 +114,6 @@ let rec reg_to_string = function
| SubReg (id,r,_) -> sprintf "%s.%s" (reg_to_string r) (id_to_string id)
;;
-let rec val_to_string_internal = function
- | V_boxref(n, t) -> sprintf "boxref %d" n
- | V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | V_tuple l ->
- let repr = String.concat ", " (List.map val_to_string_internal l) in
- sprintf "(%s)" repr
- | V_list l ->
- let repr = String.concat "; " (List.map val_to_string_internal l) in
- sprintf "[||%s||]" repr
- | V_vector (first_index, inc, l) ->
- let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index in
- let repr =
- try bitvec_to_string (* (if inc then l else List.rev l)*) l
- with Failure _ ->
- sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in
- sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
- | V_record(_, l) ->
- let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in
- let repr = String.concat "; " (List.map pp l) in
- sprintf "{%s}" repr
- | V_ctor (id,_, value) ->
- sprintf "%s %s" (id_to_string id) (val_to_string_internal value)
- | V_register r ->
- sprintf "reg-as-value %s" (reg_to_string r)
- | V_unknown -> "unknown"
-;;
-
let rec top_frame_exp_state = function
| Top -> raise (Invalid_argument "top_frame_exp")
| Hole_frame(_, e, _, env, mem, Top)
@@ -210,7 +183,7 @@ let id_compare i1 i2 =
module Reg = struct
include Map.Make(struct type t = id let compare = id_compare end)
let to_string id v =
- sprintf "%s -> %s" (id_to_string id) (val_to_string_internal v)
+ sprintf "%s -> %s" (id_to_string id) (string_of_value v)
let find id m =
(* eprintf "reg_find called with %s\n" (id_to_string id);*)
let v = find id m in
@@ -255,7 +228,7 @@ module Mem = struct
v
*)
let to_string idx v =
- sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string_internal v)
+ sprintf "[%s] -> %s" (string_of_big_int idx) (string_of_value v)
end ;;
@@ -412,7 +385,7 @@ let run
in
let rec loop mode env = function
| Value v ->
- debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string_internal v);
+ debugf "%s: %s %s\n" (grey name) (blue "return") (string_of_value v);
true, mode, env
| Action (a, s) ->
let (top_exp,(top_env,top_mem)) = top_frame_exp_state s in
@@ -429,25 +402,25 @@ let run
let left = "<-" and right = "->" in
let (mode',env',s) = begin match a with
| Read_reg (reg, sub) ->
- show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string_internal return);
+ show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (string_of_value return);
step (),env',s
| Write_reg (reg, sub, value) ->
assert (return = unit_lit);
- show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string_internal value);
+ show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (string_of_value value);
step (),env',s
| Read_mem (id, args, sub) ->
- show "read_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) right (val_to_string_internal return);
+ show "read_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) right (string_of_value return);
step (),env',s
| Write_mem (id, args, sub, value) ->
assert (return = unit_lit);
- show "write_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) left (val_to_string_internal value);
+ show "write_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) left (string_of_value value);
step (),env',s
(* distinguish single argument for pretty-printing *)
| Call_extern (f, (V_tuple _ as args)) ->
- show "call_lib" (f ^ val_to_string_internal args) right (val_to_string_internal return);
+ show "call_lib" (f ^ string_of_value args) right (string_of_value return);
step (),env',s
| Call_extern (f, arg) ->
- show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return);
+ show "call_lib" (sprintf "%s(%s)" f (string_of_value arg)) right (string_of_value return);
step (),env',s
| Interp.Step _ ->
assert (return = unit_lit);
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 167e7de9..ba939108 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -465,6 +465,11 @@ type barrier_kind =
| Barrier_TM_COMMIT
(* MIPS barriers *)
| Barrier_MIPS_SYNC
+ (* RISC-V barriers *)
+ | Barrier_RISCV_rw_rw
+ | Barrier_RISCV_r_rw
+ | Barrier_RISCV_rw_w
+
instance (Show barrier_kind)
let show = function
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d9ee73b8..cc68fbe3 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -28,8 +28,9 @@ let isubst_union s1 s2 =
| _, _ -> None) s1 s2
let subst_src_typ substs t =
- let rec s_snexp (Nexp_aux (ne,l) as nexp) =
+ let rec s_snexp substs (Nexp_aux (ne,l) as nexp) =
let re ne = Nexp_aux (ne,l) in
+ let s_snexp = s_snexp substs in
match ne with
| Nexp_var (Kid_aux (_,l) as kid) ->
(try KSubst.find kid substs
@@ -42,22 +43,25 @@ let subst_src_typ substs t =
| Nexp_exp ne -> re (Nexp_exp (s_snexp ne))
| Nexp_neg ne -> re (Nexp_neg (s_snexp ne))
in
- let rec s_styp ((Typ_aux (t,l)) as ty) =
+ let rec s_styp substs ((Typ_aux (t,l)) as ty) =
let re t = Typ_aux (t,l) in
match t with
| Typ_wild
| Typ_id _
| Typ_var _
-> ty
- | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp t1, s_styp t2,e))
- | Typ_tup ts -> re (Typ_tup (List.map s_styp ts))
- | Typ_app (id,tas) -> re (Typ_app (id,List.map s_starg tas))
- and s_starg (Typ_arg_aux (ta,l) as targ) =
+ | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp substs t1, s_styp substs t2,e))
+ | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
+ | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
+ | Typ_exist (kids,nc,t) ->
+ let substs = List.fold_left (fun sub v -> KSubst.remove v sub) substs kids in
+ re (Typ_exist (kids,nc,s_styp substs t))
+ and s_starg substs (Typ_arg_aux (ta,l) as targ) =
match ta with
- | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (s_snexp ne),l)
- | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp t),l)
+ | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (s_snexp substs ne),l)
+ | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp substs t),l)
| Typ_arg_order _ -> targ
- in s_styp t
+ in s_styp substs t
let make_vector_lit sz i =
let f j = if (i lsr (sz-j-1)) mod 2 = 0 then '0' else '1' in
@@ -128,6 +132,111 @@ let rec cross = function
let t' = cross t in
List.concat (List.map (fun y -> List.map (fun l' -> (x,y)::l') t') l)
+let rec cross' = function
+ | [] -> [[]]
+ | (h::t) ->
+ let t' = cross' t in
+ List.concat (List.map (fun x -> List.map (List.cons x) t') h)
+
+let rec cross'' = function
+ | [] -> [[]]
+ | (k,None)::t -> List.map (List.cons (k,None)) (cross'' t)
+ | (k,Some h)::t ->
+ let t' = cross'' t in
+ List.concat (List.map (fun x -> List.map (List.cons (k,Some x)) t') h)
+
+let kidset_bigunion = function
+ | [] -> KidSet.empty
+ | h::t -> List.fold_left KidSet.union h t
+
+(* TODO: deal with non-set constraints, intersections, etc somehow *)
+let extract_set_nc var (NC_aux (_,l) as nc) =
+ let rec aux (NC_aux (nc,l)) =
+ let re nc = NC_aux (nc,l) in
+ match nc with
+ | NC_nat_set_bounded (id,is) when Kid.compare id var = 0 -> Some (is,re NC_true)
+ | NC_and (nc1,nc2) ->
+ (match aux nc1, aux nc2 with
+ | None, None -> None
+ | None, Some (is,nc2') -> Some (is, re (NC_and (nc1,nc2')))
+ | Some (is,nc1'), None -> Some (is, re (NC_and (nc1',nc2)))
+ | Some _, Some _ ->
+ raise (Reporting_basic.err_general l ("Multiple set constraints for " ^ string_of_kid var)))
+ | _ -> None
+ in match aux nc with
+ | Some is -> is
+ | None ->
+ raise (Reporting_basic.err_general l ("No set constraint for " ^ string_of_kid var))
+
+let rec peel = function
+ | [], l -> ([], l)
+ | h1::t1, h2::t2 -> let (l1,l2) = peel (t1, t2) in ((h1,h2)::l1,l2)
+ | _,_ -> assert false
+
+let rec split_insts = function
+ | [] -> [],[]
+ | (k,None)::t -> let l1,l2 = split_insts t in l1,k::l2
+ | (k,Some v)::t -> let l1,l2 = split_insts t in (k,v)::l1,l2
+
+let apply_kid_insts kid_insts t =
+ let kid_insts, kids' = split_insts kid_insts in
+ let kid_insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) kid_insts in
+ let subst = ksubst_from_list kid_insts in
+ kids', subst_src_typ subst t
+
+let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
+ match ty with
+ | Typ_wild
+ | Typ_id _
+ | Typ_var _
+ -> insts,typ
+ | Typ_fn _ ->
+ raise (Reporting_basic.err_general l "Function type in constructor")
+ | Typ_tup ts ->
+ let insts,ts =
+ List.fold_right
+ (fun typ (insts,ts) -> let insts,typ = inst_src_type insts typ in insts,typ::ts)
+ ts (insts,[])
+ in insts, Typ_aux (Typ_tup ts,l)
+ | Typ_app (id,args) ->
+ let insts,ts =
+ List.fold_right
+ (fun arg (insts,args) -> let insts,arg = inst_src_typ_arg insts arg in insts,arg::args)
+ args (insts,[])
+ in insts, Typ_aux (Typ_app (id,ts),l)
+ | Typ_exist (kids, nc, t) ->
+ let kid_insts, insts' = peel (kids,insts) in
+ let kids', t' = apply_kid_insts kid_insts t in
+ (* TODO: subst in nc *)
+ match kids' with
+ | [] -> insts', t'
+ | _ -> insts', Typ_aux (Typ_exist (kids', nc, t'), l)
+and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) =
+ match ta with
+ | Typ_arg_nexp _
+ | Typ_arg_order _
+ -> insts, tyarg
+ | Typ_arg_typ typ ->
+ let insts', typ' = inst_src_type insts typ in
+ insts', Typ_arg_aux (Typ_arg_typ typ',l)
+
+let rec contains_exist (Typ_aux (ty,_)) =
+ match ty with
+ | Typ_wild
+ | Typ_id _
+ | Typ_var _
+ -> false
+ | Typ_fn (t1,t2,_) -> contains_exist t1 || contains_exist t2
+ | Typ_tup ts -> List.exists contains_exist ts
+ | Typ_app (_,args) -> List.exists contains_exist_arg args
+ | Typ_exist _ -> true
+and contains_exist_arg (Typ_arg_aux (arg,_)) =
+ match arg with
+ | Typ_arg_nexp _
+ | Typ_arg_order _
+ -> false
+ | Typ_arg_typ typ -> contains_exist typ
+
(* Given a type for a constructor, work out which refinements we ought to produce *)
(* TODO collision avoidance *)
let split_src_type id ty (TypQ_aux (q,ql)) =
@@ -146,65 +255,87 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
| Nexp_neg n
-> size_nvars_nexp n
in
- let rec size_nvars_ty (Typ_aux (ty,l)) =
+ (* This was originally written for the general case, but I cut it down to the
+ more manageable prenex-form below *)
+ let rec size_nvars_ty (Typ_aux (ty,l) as typ) =
match ty with
| Typ_wild
| Typ_id _
| Typ_var _
- -> []
+ -> (KidSet.empty,[[],typ])
| Typ_fn _ ->
raise (Reporting_basic.err_general l ("Function type in constructor " ^ i))
- | Typ_tup ts -> List.concat (List.map size_nvars_ty ts)
+ | Typ_tup ts ->
+ let (vars,tys) = List.split (List.map size_nvars_ty ts) in
+ let insttys = List.map (fun x -> let (insts,tys) = List.split x in
+ List.concat insts, Typ_aux (Typ_tup tys,l)) (cross' tys) in
+ (kidset_bigunion vars, insttys)
| Typ_app (Id_aux (Id "vector",_),
[_;Typ_arg_aux (Typ_arg_nexp sz,_);
_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
- size_nvars_nexp sz
+ (KidSet.of_list (size_nvars_nexp sz), [[],typ])
| Typ_app (_, tas) ->
- [] (* We only support sizes for bitvectors mentioned explicitly, not any buried
- inside another type *)
+ (KidSet.empty,[[],typ]) (* We only support sizes for bitvectors mentioned explicitly, not any buried
+ inside another type *)
+ | Typ_exist (kids, nc, t) ->
+ let (vars,tys) = size_nvars_ty t in
+ let find_insts k (insts,nc) =
+ let inst,nc' =
+ if KidSet.mem k vars then
+ let is,nc' = extract_set_nc k nc in
+ Some is,nc'
+ else None,nc
+ in (k,inst)::insts,nc'
+ in
+ let (insts,nc') = List.fold_right find_insts kids ([],nc) in
+ let insts = cross'' insts in
+ let ty_and_inst (inst0,ty) inst =
+ let kids, ty = apply_kid_insts inst ty in
+ let ty = Typ_aux (Typ_exist (kids, nc', ty),l) in
+ inst@inst0, ty
+ in
+ let tys = List.concat (List.map (fun instty -> List.map (ty_and_inst instty) insts) tys) in
+ let free = List.fold_left (fun vars k -> KidSet.remove k vars) vars kids in
+ (free,tys)
+ in
+ (* Only single-variable prenex-form for now *)
+ let size_nvars_ty (Typ_aux (ty,l) as typ) =
+ match ty with
+ | Typ_exist (kids,_,t) ->
+ begin
+ match snd (size_nvars_ty typ) with
+ | [] -> []
+ | tys ->
+ if contains_exist t then
+ raise (Reporting_basic.err_general l
+ "Only prenex types in unions are supported by monomorphisation")
+ else if List.length kids > 1 then
+ raise (Reporting_basic.err_general l
+ "Only single-variable existential types in unions are currently supported by monomorphisation")
+ else tys
+ end
+ | _ -> []
in
- let nvars = List.sort_uniq Kid.compare (size_nvars_ty ty) in
- match nvars with
+ (* TODO: reject universally quantification or monomorphise it *)
+ let variants = size_nvars_ty ty in
+ match variants with
| [] -> None
| sample::__ ->
- (* Only check for constraints if we found a size to constrain *)
- let qs =
- match q with
- | TypQ_no_forall ->
- raise (Reporting_basic.err_general ql
- ("No set constraint for variable " ^ string_of_kid sample ^ " in constructor " ^ i))
- | TypQ_tq qs -> qs
- in
- let find_set (Kid_aux (Var nvar,_) as kid) =
- match list_extract (function
- | QI_aux (QI_const (NC_aux (NC_nat_set_bounded (Kid_aux (Var nvar',_),vals),_)),_)
- -> if nvar = nvar' then Some vals else None
- | _ -> None) qs with
- | None ->
- raise (Reporting_basic.err_general ql
- ("No set constraint for variable " ^ nvar ^ " in constructor " ^ i))
- | Some vals -> (kid,vals)
- in
- let nvar_sets = List.map find_set nvars in
- let total_variants = List.fold_left ( * ) 1 (List.map (fun (_,l) -> List.length l) nvar_sets) in
- let () = if total_variants > size_set_limit then
+ let () = if List.length variants > size_set_limit then
raise (Reporting_basic.err_general ql
- (string_of_int total_variants ^ "variants for constructor " ^ i ^
+ (string_of_int (List.length variants) ^ "variants for constructor " ^ i ^
"bigger than limit " ^ string_of_int size_set_limit)) else ()
in
- let variants = cross nvar_sets in
let wrap = match id with
| Id_aux (Id i,l) -> (fun f -> Id_aux (Id (f i),Generated l))
| Id_aux (DeIid i,l) -> (fun f -> Id_aux (DeIid (f i),l))
in
- let name l i = String.concat "_" (i::(List.map (fun (v,i) -> string_of_kid v ^ string_of_int i) l)) in
- Some (List.map (fun l -> (l, wrap (name l))) variants)
-
-(* TODO: maybe fold this into subst_src_typ? *)
-let inst_src_type insts ty =
- let insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) insts in
- let subst = ksubst_from_list insts in
- subst_src_typ subst ty
+ let name_seg = function
+ | (_,None) -> ""
+ | (k,Some i) -> string_of_kid k ^ string_of_int i
+ in
+ let name l i = String.concat "_" (i::(List.map name_seg l)) in
+ Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants)
let reduce_nexp subst ne =
let rec eval (Nexp_aux (ne,_) as nexp) =
@@ -394,6 +525,7 @@ let bindings_from_pat p =
| P_typ (_,p) -> aux_pat p
| P_id id ->
if pat_id_is_variable env id then [id] else []
+ | P_var kid -> [id_of_kid kid]
| P_vector ps
| P_vector_concat ps
| P_app (_,ps)
@@ -408,7 +540,7 @@ let bindings_from_pat p =
let remove_bound env pat =
let bound = bindings_from_pat pat in
- List.fold_left (fun sub v -> ISubst.remove v env) env bound
+ List.fold_left (fun sub v -> ISubst.remove v sub) env bound
(* Remove explicit existential types from the AST, so that the sizes of
bitvectors will be filled in throughout.
@@ -461,6 +593,8 @@ let rec deexist_exp (E_aux (e,(l,(annot : Type_check.tannot))) as exp) =
| E_let (lb,e1) -> re (E_let (deexist_letbind lb, deexist_exp e1))
| E_assign (le,e1) -> re (E_assign (deexist_lexp le, deexist_exp e1))
| E_exit e1 -> re (E_exit (deexist_exp e1))
+ | E_throw e1 -> re (E_throw (deexist_exp e1))
+ | E_try (e1,cases) -> re (E_try (deexist_exp e1, List.map deexist_pexp cases))
| E_return e1 -> re (E_return (deexist_exp e1))
| E_assert (e1,e2) -> re (E_assert (deexist_exp e1,deexist_exp e2))
and deexist_pexp (Pat_aux (pe,(l,annot))) =
@@ -548,6 +682,13 @@ let can_match (E_aux (e,(l,annot)) as exp0) cases =
in findpat_generic checkpat "bit" cases
| _ -> None
+(* Remove top-level casts from an expression. Useful when we need to look at
+ subexpressions to reduce something, but could break type-checking if we used
+ it everywhere. *)
+let rec drop_casts = function
+ | E_aux (E_cast (_,e),_) -> drop_casts e
+ | exp -> exp
+
(* Similarly, simple conditionals *)
let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) =
@@ -566,8 +707,8 @@ let neq_fns = [Id "neq_anything"]
let try_app (l,ann) (Id_aux (id,_),args) =
let is_eq = List.mem id eq_fns in
let is_neq = (not is_eq) && List.mem id neq_fns in
+ let new_l = Generated l in
if is_eq || is_neq then
- let new_l = Generated l in
match args with
| [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] ->
let lit b = if b then L_true else L_false in
@@ -576,6 +717,11 @@ let try_app (l,ann) (Id_aux (id,_),args) =
| None -> None
| Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann))))
| _ -> None
+ else if id = Id "cast_bit_bool" then
+ match args with
+ | [E_aux (E_lit L_aux (L_zero,_),_)] -> Some (E_aux (E_lit (L_aux (L_false,new_l)),(l,ann)))
+ | [E_aux (E_lit L_aux (L_one ,_),_)] -> Some (E_aux (E_lit (L_aux (L_true ,new_l)),(l,ann)))
+ | _ -> None
else None
@@ -591,7 +737,6 @@ let try_app_infix (l,ann) (E_aux (e1,ann1)) (Id_aux (id,_)) (E_aux (e2,ann2)) =
| None -> None)
| _ -> None
-
(* We may need to split up a pattern match if (1) we've been told to case split
on a variable by the user, or (2) we monomorphised a constructor that's used
in the pattern. *)
@@ -610,7 +755,7 @@ let split_defs splits defs =
| None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)])
| Some variants ->
([(id,variants)],
- List.map (fun (insts, id') -> Tu_aux (Tu_ty_id (inst_src_type insts ty,id'),Generated l)) variants))
+ List.map (fun (insts, id', ty) -> Tu_aux (Tu_ty_id (ty,id'),Generated l)) variants))
in
let sc_type_def ((TD_aux (tda,annot)) as td) =
match tda with
@@ -710,7 +855,7 @@ let split_defs splits defs =
| E_if (e1,e2,e3) ->
let e1' = const_prop_exp substs e1 in
let e2',e3' = const_prop_exp substs e2, const_prop_exp substs e3 in
- (match e1' with
+ (match drop_casts e1' with
| E_aux (E_lit (L_aux ((L_true|L_false) as lit ,_)),_) ->
let e' = match lit with L_true -> e2' | _ -> e3' in
(match e' with E_aux (_,(_,annot')) ->
@@ -745,6 +890,10 @@ let split_defs splits defs =
re (E_let (lb', const_prop_exp substs' e))
| E_assign (le,e) -> re (E_assign (const_prop_lexp substs le, const_prop_exp substs e))
| E_exit e -> re (E_exit (const_prop_exp substs e))
+ | E_throw e -> re (E_throw (const_prop_exp substs e))
+ | E_try (e,cases) ->
+ let e' = const_prop_exp substs e in
+ re (E_case (e', List.map (const_prop_pexp substs) cases))
| E_return e -> re (E_return (const_prop_exp substs e))
| E_assert (e1,e2) -> re (E_assert (const_prop_exp substs e1,const_prop_exp substs e2))
| E_internal_cast (ann,e) -> re (E_internal_cast (ann,const_prop_exp substs e))
@@ -836,7 +985,7 @@ let split_defs splits defs =
(* Substitute what we've learned about nvars into the term *)
let nsubsts = isubst_from_list !nexp_substs in
let () = nexp_substs := [] in
- nexp_subst_exp nsubsts refinements exp'
+ (*nexp_subst_exp nsubsts refinements*) exp'
in
(* Split a variable pattern into every possible value *)
@@ -933,6 +1082,7 @@ let split_defs splits defs =
match p with
| P_lit _
| P_wild
+ | P_var _
-> None
| P_as (p',id) when id_matches id ->
raise (Reporting_basic.err_general l
@@ -978,29 +1128,34 @@ let split_defs splits defs =
| None ->
match p with
| P_app (id,args) ->
- (try
- let (_,variants) = List.find (fun (id',_) -> Id.compare id id' = 0) refinements in
- let env,_ = env_typ_expected l tannot in
- let constr_out_typ =
- match Env.get_val_spec id env with
- | (qs,Typ_aux (Typ_fn(_,outt,_),_)) -> outt
- | _ -> raise (Reporting_basic.err_general l
- ("Constructor " ^ string_of_id id ^ " is not a construtor!"))
- in
- let varmap = build_nexp_subst l constr_out_typ tannot in
- let map_inst (insts,id') =
- let insts = List.map (fun (v,i) ->
- ((match List.assoc (string_of_kid v) varmap with
- | Nexp_aux (Nexp_var s, _) -> s
- | _ -> raise (Reporting_basic.err_general l
- ("Constructor parameter not a variable: " ^ string_of_kid v))),
- Nexp_aux (Nexp_constant i,Generated l)))
- insts in
- P_aux (P_app (id',args),(Generated l,tannot)),
- ksubst_from_list insts
- in
- ConstrSplit (List.map map_inst variants)
- with Not_found -> NoSplit)
+ begin
+ let kid,kid_annot =
+ match args with
+ | [P_aux (P_var kid,ann)] -> kid,ann
+ | _ ->
+ raise (Reporting_basic.err_general l
+ "Pattern match not currently supported by monomorphisation")
+ in match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with
+ | (_,variants) ->
+ let map_inst (insts,id',_) =
+ let insts =
+ match insts with [(v,Some i)] -> [(kid,Nexp_aux (Nexp_constant i, Generated l))]
+ | _ -> assert false
+ in
+(*
+ let insts,_ = split_insts insts in
+ let insts = List.map (fun (v,i) ->
+ (??,
+ Nexp_aux (Nexp_constant i,Generated l)))
+ insts in
+ P_aux (P_app (id',args),(Generated l,tannot)),
+*)
+ P_aux (P_app (id',[P_aux (P_id (id_of_kid kid),kid_annot)]),(Generated l,tannot)),
+ ksubst_from_list insts
+ in
+ ConstrSplit (List.map map_inst variants)
+ | exception Not_found -> NoSplit
+ end
| _ -> NoSplit
in
@@ -1055,6 +1210,8 @@ let split_defs splits defs =
| E_let (lb,e) -> re (E_let (map_letbind lb, map_exp e))
| E_assign (le,e) -> re (E_assign (map_lexp le, map_exp e))
| E_exit e -> re (E_exit (map_exp e))
+ | E_throw e -> re (E_throw e)
+ | E_try (e,cases) -> re (E_try (map_exp e, List.concat (List.map map_pexp cases)))
| E_return e -> re (E_return (map_exp e))
| E_assert (e1,e2) -> re (E_assert (map_exp e1,map_exp e2))
| E_internal_cast (ann,e) -> re (E_internal_cast (ann,map_exp e))
diff --git a/src/process_file.ml b/src/process_file.ml
index 0f789c9d..22f25f6e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -110,8 +110,11 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E
let () = if !opt_just_check then exit 0 else () in
(ast, env)
+let opt_ddump_raw_mono_ast = ref false
+
let monomorphise_ast locs ast =
let ast = Monomorphise.split_defs locs ast in
+ let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in
let ienv = Type_check.Env.no_casts Type_check.initial_env in
Type_check.check ienv ast
diff --git a/src/process_file.mli b/src/process_file.mli
index 53a6f3f2..c477d185 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -58,6 +58,7 @@ val opt_just_check : bool ref
val opt_ddump_tc_ast : bool ref
val opt_ddump_rewrite_ast : ((string * int) option) ref
val opt_dno_cast : bool ref
+val opt_ddump_raw_mono_ast : bool ref
type out_type =
| Lem_ast_out
diff --git a/src/sail.ml b/src/sail.ml
index b63f807c..312a3c7c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -94,6 +94,9 @@ let options = Arg.align ([
| [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split
| _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))),
"<filename>:<line>:<variable> to case split for monomorphisation");
+ ( "-ddump_raw_mono_ast",
+ Arg.Set opt_ddump_raw_mono_ast,
+ " (debug) dump the monomorphised ast before type-checking");
( "-new_parser",
Arg.Set Process_file.opt_new_parser,
" (experimental) use new parser");
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:58:07 +0000