From 6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 10 May 2018 17:40:48 +0100 Subject: latex: don't include the prefix in the label. This means we have the option of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels. --- src/latex.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index f16dddd8..8688eaa8 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -123,7 +123,7 @@ let commands = ref StringSet.empty let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l, _) as annot) = let labelling = match label with | None -> "" - | Some l -> Printf.sprintf "\\label{%s%s}" prefix l + | Some l -> Printf.sprintf "\\label{%s}" l in let cmd = !opt_prefix_latex ^ prefix ^ cmd in if StringSet.mem cmd !commands then -- cgit v1.2.3 From 619bd9b568f6f8f5691a66602b7635834d3d13a2 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 11 May 2018 11:31:47 +0100 Subject: Avoid generating latex files that differ only by case because this causes confusion on case insensitive file systems (e.g. mac). --- src/latex.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 8688eaa8..3233a4ac 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -126,11 +126,12 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l | Some l -> Printf.sprintf "\\label{%s}" l in let cmd = !opt_prefix_latex ^ prefix ^ cmd in - if StringSet.mem cmd !commands then + let lcmd = String.lowercase cmd in (* lowercase to avoid file names differing only by case *) + if StringSet.mem lcmd !commands then latex_command ~label:label dir (cmd ^ "v") no_loc annot else begin - commands := StringSet.add cmd !commands; + commands := StringSet.add lcmd !commands; let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l)); close_out oc; -- cgit v1.2.3 From 17c786ea27bf644efdae271b8a93bd5ce1d730e8 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 11 May 2018 11:32:31 +0100 Subject: Remove unneeded _sail suffix from latex files. --- src/latex.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 3233a4ac..0520d074 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -132,10 +132,10 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l else begin commands := StringSet.add lcmd !commands; - let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in + let oc = open_out (Filename.concat dir (cmd ^ ".tex")) in output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l)); close_out oc; - string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s_sail.tex}}" dir cmd) + string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s.tex}}" dir cmd) end let latex_command_id ?prefix:(prefix="") dir id no_loc annot = -- cgit v1.2.3 From db3b6d21c18f4ac516c2554db6890274d2b8292c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 10 May 2018 14:23:49 +0100 Subject: Remove buggy bit list comparison functions from Lem library Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do. --- src/gen_lib/sail_operators.lem | 30 ------------------------------ src/gen_lib/sail_operators_bitlists.lem | 16 ---------------- src/gen_lib/sail_operators_mwords.lem | 16 ---------------- src/pretty_print_lem.ml | 22 ++++++++-------------- 4 files changed, 8 insertions(+), 76 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 78aab65e..0c5da675 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -194,36 +194,6 @@ let neq_bv l r = not (eq_bv l r) let inline neq_mword l r = (l <> r) -val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r)) -let ulteq_bv l r = (eq_bv l r) || (ult_bv l r) -let ugt_bv l r = not (ulteq_bv l r) -let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r) - -val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let slt_bv l r = - match (most_significant l, most_significant r) with - | (B0, B0) -> ult_bv l r - | (B0, B1) -> false - | (B1, B0) -> true - | (B1, B1) -> - let l' = add_one_bit_ignore_overflow (bits_of l) in - let r' = add_one_bit_ignore_overflow (bits_of r) in - ugt_bv l' r' - | (BU, BU) -> ult_bv l r - | (BU, _) -> true - | (_, BU) -> false - end -let slteq_bv l r = (eq_bv l r) || (slt_bv l r) -let sgt_bv l r = not (slteq_bv l r) -let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r) - -val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool -let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r) - -val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool -let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) - val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a let get_slice_int_bv len n lo = let hi = lo + len - 1 in diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index fed293b4..19e9b519 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -308,21 +308,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v = val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool -val ult_vec : list bitU -> list bitU -> bool -val slt_vec : list bitU -> list bitU -> bool -val ugt_vec : list bitU -> list bitU -> bool -val sgt_vec : list bitU -> list bitU -> bool -val ulteq_vec : list bitU -> list bitU -> bool -val slteq_vec : list bitU -> list bitU -> bool -val ugteq_vec : list bitU -> list bitU -> bool -val sgteq_vec : list bitU -> list bitU -> bool let eq_vec = eq_bv let neq_vec = neq_bv -let ult_vec = ult_bv -let slt_vec = slt_bv -let ugt_vec = ugt_bv -let sgt_vec = sgt_bv -let ulteq_vec = ulteq_bv -let slteq_vec = slteq_bv -let ugteq_vec = ugteq_bv -let sgteq_vec = sgteq_bv diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 077dfb02..22d5b246 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -329,21 +329,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v = val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val slt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ugt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val sgt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool let inline eq_vec = eq_mword let inline neq_vec = neq_mword -let inline ult_vec = ucmp_mword (<) -let inline slt_vec = scmp_mword (<) -let inline ugt_vec = ucmp_mword (>) -let inline sgt_vec = scmp_mword (>) -let inline ulteq_vec = ucmp_mword (<=) -let inline slteq_vec = scmp_mword (<=) -let inline ugteq_vec = ucmp_mword (>=) -let inline sgteq_vec = scmp_mword (>=) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c181249d..58bbfc4b 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -111,10 +111,7 @@ let rec fix_id remove_tick name = match name with let doc_id_lem (Id_aux(i,_)) = match i with | Id i -> string (fix_id false i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) + | DeIid x -> string (Util.zencode_string ("op " ^ x)) let doc_id_lem_type (Id_aux(i,_)) = match i with @@ -122,10 +119,7 @@ let doc_id_lem_type (Id_aux(i,_)) = | Id("nat") -> string "ii" | Id("option") -> string "maybe" | Id i -> string (fix_id false i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) + | DeIid x -> string (Util.zencode_string ("op " ^ x)) let doc_id_lem_ctor (Id_aux(i,_)) = match i with @@ -135,10 +129,11 @@ let doc_id_lem_ctor (Id_aux(i,_)) = | Id("Some") -> string "Just" | Id("None") -> string "Nothing" | Id i -> string (fix_id false (String.capitalize i)) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - separate space [colon; string (String.capitalize x); empty] + | DeIid x -> string (Util.zencode_string ("op " ^ x)) + +let deinfix = function + | Id_aux (Id v, l) -> Id_aux (DeIid v, l) + | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l) let doc_var_lem kid = string (fix_id true (string_of_kid kid)) @@ -880,8 +875,7 @@ let doc_exp_lem, doc_let_lem = | E_assert (e1,e2) -> align (liftR (separate space [string "assert_exp"; expY e1; expY e2])) | E_app_infix (e1,id,e2) -> - raise (Reporting_basic.err_unreachable l - "E_app_infix should have been rewritten before pretty-printing") + expV aexp_needed (E_aux (E_app (deinfix id, [e1; e2]), (l, annot))) | E_var(lexp, eq_exp, in_exp) -> raise (report l "E_vars should have been removed before pretty-printing") | E_internal_plet (pat,e1,e2) -> -- cgit v1.2.3 From 1763b8b5dceb614c04ccab83a8100268e0852626 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 11 May 2018 10:16:23 +0100 Subject: Use type from funcl in singleton rewriting The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing --- src/monomorphise.ml | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 0585d9fa..3af0b480 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2241,13 +2241,16 @@ let rewrite_size_parameters env (Defs defs) = let open Rewriter in let open Util in - let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,_))) = + let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,ann))) = let pat,guard,exp,pannot = destruct_pexp pexp in - let parameters = match pat with - | P_aux (P_tup ps,_) -> ps - | _ -> [pat] + let env = env_of_annot (l,ann) in + let _, typ = Env.get_val_spec_orig id env in + let types = + match pat, Env.expand_synonyms env typ with + | P_aux (P_tup ps,_), Typ_aux (Typ_tup ts,_) -> ts + | _, _ -> [typ] in - let add_parameter (i,nmap) (P_aux (_,(_,Some (env,typ,_)))) = + let add_parameter (i,nmap) typ = let nmap = match Env.base_typ_of env typ with Typ_aux (Typ_app(Id_aux (Id "range",_), @@ -2262,8 +2265,13 @@ let rewrite_size_parameters env (Defs defs) = | _ -> nmap in (i+1,nmap) in - let (_,nexp_map) = List.fold_left add_parameter (0,NexpMap.empty) parameters in + let (_,nexp_map) = List.fold_left add_parameter (0,NexpMap.empty) types in let nexp_list = NexpMap.bindings nexp_map in +(* let () = + print_endline ("Type of pattern for " ^ string_of_id id ^": " ^string_of_typ (pat_typ_of pat)); + print_endline ("Nexp map for " ^ string_of_id id); + List.iter (fun (nexp, i) -> print_endline (" " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list +in *) let parameters_for = function | Some (env,typ,_) -> begin match Env.base_typ_of env typ with -- cgit v1.2.3 From 4c7507ae9d605bd3c1d3e6d2ca1e040f040705c8 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 11 May 2018 11:00:25 +0100 Subject: Handle automatic existential unpacking in function application in mono analysis --- src/monomorphise.ml | 44 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 37 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 3af0b480..48a7ac65 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2704,12 +2704,10 @@ let kids_bound_by_pat pat = | ((s,p),ann) -> s, P_aux (p,ann)) }) pat) -(* Add bound variables from a pattern to the environment with the given dependency. *) +(* Diff the type environment to find new type variables and record that they + depend on deps *) -let update_env env deps pat typ_env_pre typ_env_post = - let bound = bindings_from_pat pat in - let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in - (* Diff the type environment to find the new variables *) +let update_env_new_kids env deps typ_env_pre typ_env_post = let kbound = KBindings.merge (fun k x y -> match x,y with @@ -2719,7 +2717,15 @@ let update_env env deps pat typ_env_pre typ_env_post = (Env.get_typ_vars typ_env_pre) in let kid_deps = KBindings.fold (fun v _ ds -> KBindings.add v deps ds) kbound env.kid_deps in - { env with var_deps = var_deps; kid_deps = kid_deps } + { env with kid_deps = kid_deps } + +(* Add bound variables from a pattern to the environment with the given dependency, + plus any new type variables. *) + +let update_env env deps pat typ_env_pre typ_env_post = + let bound = bindings_from_pat pat in + let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in + update_env_new_kids { env with var_deps = var_deps } deps typ_env_pre typ_env_post let assigned_vars_exps es = List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp)) @@ -2894,6 +2900,30 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let deps, _, rs = split3 (List.map (analyse_exp fn_id env assigns) es) in (deps, assigns, List.fold_left merge empty rs) in + (* We allow for arguments to functions being executed non-deterministically, but + follow the type checker in processing them in-order to detect the automatic + unpacking of existentials. When we spot a new type variable (using + update_env_new_kids) we set them to depend on the previous argument. *) + let non_det_args es = + let assigns = remove_assigns es " assigned in non-deterministic expressions" in + let rec aux prev_typ_env prev_deps env = function + | [] -> [], empty + | h::t -> + let typ_env = env_of h in + let env = update_env_new_kids env prev_deps prev_typ_env typ_env in + let new_deps, _, new_r = analyse_exp fn_id env assigns h in + let t_deps, t_r = aux typ_env new_deps env t in + new_deps::t_deps, merge new_r t_r + in + let deps, r = match es with + | [] -> [], empty + | h::t -> + let new_deps, _, new_r = analyse_exp fn_id env assigns h in + let t_deps, t_r = aux (env_of h) new_deps env t in + new_deps::t_deps, merge new_r t_r + in + (deps, assigns, r) + in let merge_deps deps = List.fold_left dmerge dempty deps in let deps, assigns, r = match e with @@ -2930,7 +2960,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = | E_lit _ -> (dempty,assigns,empty) | E_cast (_,e) -> analyse_exp fn_id env assigns e | E_app (id,args) -> - let deps, assigns, r = non_det args in + let deps, assigns, r = non_det_args args in let typ_env = env_of_annot (l,annot) in let (_,fn_typ) = Env.get_val_spec id typ_env in let fn_effect = match fn_typ with -- cgit v1.2.3 From 58b895c8c5c6f1c98370876c87bb4ac5b980f770 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 11 May 2018 15:55:26 +0100 Subject: Be much more careful to introduce the right bitvector casts to the right sizes --- src/monomorphise.ml | 94 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 59 insertions(+), 35 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 48a7ac65..3f49689b 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3810,10 +3810,21 @@ end module BitvectorSizeCasts = struct +let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) = + match solve env nexp with + | Some n -> Some (nconstant n) + | None -> + let is_equal kid = + prove env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + in + match List.find is_equal quant_kids with + | kid -> Some (Nexp_aux (Nexp_var kid,Generated l)) + | exception Not_found -> None + (* These functions add cast functions across case splits, so that when a bitvector size becomes known in sail, the generated Lem code contains a function call to change mword 'n to (say) mword ty16, and vice versa. *) -let make_bitvector_cast_fns env src_typ target_typ = +let make_bitvector_cast_fns env quant_kids src_typ target_typ = let genunk = Generated Unknown in let fresh = let counter = ref 0 in @@ -3822,7 +3833,7 @@ let make_bitvector_cast_fns env src_typ target_typ = let () = counter := n+1 in mk_id ("cast#" ^ string_of_int n) in - let required = ref false in + let at_least_one = ref None in let rec aux (Typ_aux (src_t,src_l) as src_typ) (Typ_aux (tar_t,tar_l) as tar_typ) = let src_ann = Some (env,src_typ,no_effect) in let tar_ann = Some (env,tar_typ,no_effect) in @@ -3834,18 +3845,26 @@ let make_bitvector_cast_fns env src_typ target_typ = | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp size,_); _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]), - Typ_app (Id_aux (Id "vector",_), - [Typ_arg_aux (Typ_arg_nexp size',_); _; - Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) - when Nexp.compare size size' <> 0 -> - let () = required := true in - let var = fresh () in - P_aux (P_id var,(Generated src_l,src_ann)), - E_aux - (E_cast (tar_typ, - E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), - [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))), - (genunk, tar_ann)) + Typ_app (Id_aux (Id "vector",_) as t_id, + [Typ_arg_aux (Typ_arg_nexp size',l_size'); t_ord; + Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_) as t_bit]) -> begin + match simplify_size_nexp env quant_kids size, simplify_size_nexp env quant_kids size' with + | Some size, Some size' when Nexp.compare size size' <> 0 -> + let var = fresh () in + let tar_typ' = Typ_aux (Typ_app (t_id, [Typ_arg_aux (Typ_arg_nexp size',l_size');t_ord;t_bit]), + tar_l) in + let () = at_least_one := Some tar_typ' in + P_aux (P_id var,(Generated src_l,src_ann)), + E_aux + (E_cast (tar_typ', + E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), + [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))), + (genunk, tar_ann)) + | _ -> + let var = fresh () in + P_aux (P_id var,(Generated src_l,src_ann)), + E_aux (E_id var,(Generated src_l,tar_ann)) + end | _ -> let var = fresh () in P_aux (P_id var,(Generated src_l,src_ann)), @@ -3854,8 +3873,8 @@ let make_bitvector_cast_fns env src_typ target_typ = let src_typ' = Env.base_typ_of env src_typ in let target_typ' = Env.base_typ_of env target_typ in let pat, e' = aux src_typ' target_typ' in - if !required - then + match !at_least_one with + | Some one_target_typ -> begin let src_ann = Some (env,src_typ,no_effect) in let tar_ann = Some (env,target_typ,no_effect) in match src_typ' with @@ -3863,12 +3882,12 @@ let make_bitvector_cast_fns env src_typ target_typ = | Typ_aux (Typ_app _,_) -> (fun var exp -> let exp_ann = Some (env,typ_of exp,effect_of exp) in - E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)), + E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)), E_aux (E_app (Id_aux (Id "bitvector_cast",genunk), [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)), exp),(genunk,exp_ann))), (fun (E_aux (_,(exp_l,exp_ann)) as exp) -> - E_aux (E_cast (target_typ, + E_aux (E_cast (one_target_typ, E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [exp]), (Generated exp_l,tar_ann))), (Generated exp_l,tar_ann))) | _ -> @@ -3879,16 +3898,17 @@ let make_bitvector_cast_fns env src_typ target_typ = exp),(genunk,exp_ann))),(genunk,exp_ann))), (fun (E_aux (_,(exp_l,exp_ann)) as exp) -> E_aux (E_let (LB_aux (LB_val (pat, exp),(Generated exp_l,exp_ann)), e'),(Generated exp_l,tar_ann))) - else (fun _ e -> e),(fun e -> e) + end + | None -> (fun _ e -> e),(fun e -> e) (* TODO: bound vars *) -let make_bitvector_env_casts env (kid,i) exp = - let mk_cast var typ exp = (fst (make_bitvector_cast_fns env typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in +let make_bitvector_env_casts env quant_kids (kid,i) exp = + let mk_cast var typ exp = (fst (make_bitvector_cast_fns env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in let locals = Env.get_locals env in Bindings.fold (fun var (mut,typ) exp -> if mut = Immutable then mk_cast var typ exp else exp) locals exp -let make_bitvector_cast_exp typ target_typ exp = (snd (make_bitvector_cast_fns (env_of exp) typ target_typ)) exp +let make_bitvector_cast_exp env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns env quant_kids typ target_typ)) exp let rec extract_value_from_guard var (E_aux (e,_)) = match e with @@ -3909,14 +3929,14 @@ let fill_in_type env typ = | BK_type | BK_order -> subst | BK_int -> - match solve env (nvar kid) with + (match solve env (nvar kid) with | None -> subst - | Some n -> KBindings.add kid (nconstant n) subst) tyvars KBindings.empty in + | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in subst_src_typ subst typ (* TODO: top-level patterns *) let add_bitvector_casts (Defs defs) = - let rewrite_body ret_typ exp = + let rewrite_body id quant_kids top_env ret_typ exp = let rewrite_aux (e,ann) = match e with | E_case (E_aux (e',ann') as exp',cases) -> begin @@ -3931,16 +3951,17 @@ let add_bitvector_casts (Defs defs) = let body = match pat, guard with | P_aux (P_lit (L_aux (L_num i,_)),_), _ -> let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in - make_bitvector_cast_exp src_typ result_typ - (make_bitvector_env_casts env (kid,i) body) + make_bitvector_cast_exp env quant_kids src_typ result_typ + (make_bitvector_env_casts env quant_kids (kid,i) body) | P_aux (P_id var,_), Some guard -> (match extract_value_from_guard var guard with | Some i -> let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in - make_bitvector_cast_exp src_typ result_typ - (make_bitvector_env_casts env (kid,i) body) + make_bitvector_cast_exp env quant_kids src_typ result_typ + (make_bitvector_env_casts env quant_kids (kid,i) body) | None -> body) - | _ -> body + | _ -> + body in construct_pexp (pat, guard, body, ann) in @@ -3948,10 +3969,10 @@ let add_bitvector_casts (Defs defs) = | _ -> E_aux (e,ann) end | E_return e' -> - E_aux (E_return (make_bitvector_cast_exp (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) + E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) | E_assign (LEXP_aux (lexp,lexp_annot),e') -> E_aux (E_assign (LEXP_aux (lexp,lexp_annot), - make_bitvector_cast_exp (fill_in_type (env_of e') (typ_of e')) + make_bitvector_cast_exp (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e')) (typ_of_annot lexp_annot) e'),ann) | _ -> E_aux (e,ann) in @@ -3961,8 +3982,10 @@ let add_bitvector_casts (Defs defs) = e_aux = rewrite_aux } exp in let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann)) = + let (tq,typ) = Env.get_val_spec_orig id (env_of_annot fcl_ann) in + let quant_kids = List.map kopt_kid (quant_kopts tq) in let ret_typ = - match typ_of_annot fcl_ann with + match typ with | Typ_aux (Typ_fn (_,ret,_),_) -> ret | Typ_aux (_,l) as typ -> raise (Reporting_basic.err_unreachable l @@ -3970,10 +3993,11 @@ let add_bitvector_casts (Defs defs) = " is not a function type")) in let pat,guard,body,annot = destruct_pexp pexp in - let body = rewrite_body ret_typ body in + let env = env_of body in + let body = rewrite_body id quant_kids env ret_typ body in (* Also add a cast around the entire function clause body, if necessary *) let body = - make_bitvector_cast_exp (fill_in_type (env_of body) (typ_of body)) ret_typ body + make_bitvector_cast_exp env quant_kids (fill_in_type (env_of body) (typ_of body)) ret_typ body in let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) -- cgit v1.2.3 From 7c0117f992fbe27ea0684b55cb7f39bd87393cdc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 11 May 2018 17:02:18 +0100 Subject: Actually use the correct type for singleton rewriting this time --- src/monomorphise.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 3f49689b..6dcd14ba 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2245,6 +2245,10 @@ let rewrite_size_parameters env (Defs defs) = let pat,guard,exp,pannot = destruct_pexp pexp in let env = env_of_annot (l,ann) in let _, typ = Env.get_val_spec_orig id env in + let typ = match typ with + | Typ_aux (Typ_fn (arg_typ,_,_),_) -> arg_typ + | _ -> typ (* TODO: error *) + in let types = match pat, Env.expand_synonyms env typ with | P_aux (P_tup ps,_), Typ_aux (Typ_tup ts,_) -> ts @@ -2269,6 +2273,7 @@ let rewrite_size_parameters env (Defs defs) = let nexp_list = NexpMap.bindings nexp_map in (* let () = print_endline ("Type of pattern for " ^ string_of_id id ^": " ^string_of_typ (pat_typ_of pat)); + print_endline ("Types : " ^ String.concat ", " (List.map string_of_typ types)); print_endline ("Nexp map for " ^ string_of_id id); List.iter (fun (nexp, i) -> print_endline (" " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list in *) -- cgit v1.2.3 From d03a5adef64d66a49b69f1c9125e20c45e8b45b0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 11 May 2018 17:03:11 +0100 Subject: Make nexp simplification a little smarter (should really make the Lem pretty printer use the solver properly, but this is a useful stopgap) --- src/ast_util.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index f7574b9d..968cb320 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -244,6 +244,13 @@ and nexp_simp_aux = function when Big_int.equal c1 (Big_int.negate c2) -> n | _, _ -> Nexp_minus (n1, n2) end + | Nexp_neg n -> + begin + let (Nexp_aux (n_simp, _) as n) = nexp_simp n in + match n_simp with + | Nexp_constant c -> Nexp_constant (Big_int.negate c) + | _ -> Nexp_neg n + end | Nexp_app (Id_aux (Id "div",_) as id,[n1;n2]) -> begin let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in -- cgit v1.2.3 From 8041ff0692b7f16a09afb36cd35199d5021e63b2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 11 May 2018 17:20:56 +0100 Subject: More builtin names in constant propagation --- src/monomorphise.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 6dcd14ba..4f257712 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -856,7 +856,7 @@ let try_app (l,ann) (id,args) = | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann))) | _ -> None - else if is_id "mult_int" || is_id "mult_range" then + else if is_id "mult_atom" || is_id "mult_int" || is_id "mult_range" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann))) @@ -866,7 +866,7 @@ let try_app (l,ann) (id,args) = | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.div i j),new_l)),(l,ann))) | _ -> None - else if is_id "add_range" then + else if is_id "add_atom" || is_id "add_int" || is_id "add_range" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.add i j),new_l)),(l,ann))) -- cgit v1.2.3 From 526b71d5fed2f6a79c41fe482a578a8634a0345a Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 12 May 2018 11:16:27 +0100 Subject: Fix bug in handling of registers with option type Also add test cases and Isabelle lemmas --- src/state.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index 5a360456..ab63747c 100644 --- a/src/state.ml +++ b/src/state.ml @@ -286,7 +286,7 @@ let register_refs_lem mwords registers = ""; "val option_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (maybe 'a)"; "let option_of_regval of_regval = function"; - " | Regval_option v -> Maybe.map of_regval v"; + " | Regval_option v -> Just (Maybe.bind v of_regval)"; " | _ -> Nothing"; "end"; ""; @@ -388,6 +388,19 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = "proof -"; " from assms have \"of_rv \\ rv_of = Some\" by auto"; " then show ?thesis by (auto simp: vector_of_regval_def regval_of_vector_def)"; + "qed"; + ""; + "lemma option_of_rv_rv_of_option[simp]:"; + " assumes \"\\v. of_rv (rv_of v) = Some v\""; + " shows \"option_of_regval of_rv (regval_of_option rv_of v) = Some v\""; + " using assms by (cases v) (auto simp: option_of_regval_def regval_of_option_def)"; + ""; + "lemma list_of_rv_rv_of_list[simp]:"; + " assumes \"\\v. of_rv (rv_of v) = Some v\""; + " shows \"list_of_regval of_rv (regval_of_list rv_of v) = Some v\""; + "proof -"; + " from assms have \"of_rv \\ rv_of = Some\" by auto"; + " with assms show ?thesis by (induction v) (auto simp: list_of_regval_def regval_of_list_def)"; "qed"] ^^ hardline ^^ hardline ^^ separate_map (hardline ^^ hardline) register_lemmas registers -- cgit v1.2.3