diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/anf.ml | 26 | ||||
| -rw-r--r-- | src/c_backend.ml | 4 | ||||
| -rw-r--r-- | src/reporting.ml | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 113 |
4 files changed, 21 insertions, 124 deletions
@@ -57,9 +57,6 @@ open PPrint module Big_int = Nat_big_num -let anf_error ?loc:(l=Parse_ast.Unknown) message = - raise (Reporting.err_general l ("\nANF translation: " ^ message)) - (**************************************************************************) (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) @@ -453,7 +450,8 @@ let rec split_block l = function | exp :: exps -> let exps, last = split_block l exps in exp :: exps, last - | [] -> anf_error ~loc:l "empty block" + | [] -> + raise (Reporting.err_unreachable l __POS__ "empty block found when converting to ANF") let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in @@ -469,7 +467,9 @@ let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat)) | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat))) | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat)) - | _ -> anf_error ~loc:(fst annot) ("Could not convert pattern to ANF: " ^ string_of_pat pat) + | _ -> + raise (Reporting.err_unreachable (fst annot) __POS__ + ("Could not convert pattern to ANF: " ^ string_of_pat pat)) let rec apat_globals (AP_aux (aux, _, _)) = match aux with @@ -529,7 +529,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = mk_aexp (AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp)) | E_assign (lexp, _) -> - failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") + raise (Reporting.err_unreachable l __POS__ + ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) | E_loop (loop_typ, cond, exp) -> let acond = anf cond in @@ -665,7 +666,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp)) | E_var (lexp, _, _) -> - failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") + raise (Reporting.err_unreachable l __POS__ + ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) | E_let (LB_aux (LB_val (pat, binding), _), body) -> anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), exp_annot)) @@ -690,19 +692,19 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ -> (* Should be re-written by type checker *) - failwith "encountered raw vector operation when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered raw vector operation when converting to ANF") | E_internal_value _ -> (* Interpreter specific *) - failwith "encountered E_internal_value when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered E_internal_value when converting to ANF") | E_sizeof _ | E_constraint _ -> (* Sizeof nodes removed by sizeof rewriting pass *) - failwith "encountered E_sizeof or E_constraint node when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered E_sizeof or E_constraint node when converting to ANF") | E_nondet _ -> (* We don't compile E_nondet nodes *) - failwith "encountered E_nondet node when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered E_nondet node when converting to ANF") | E_internal_return _ | E_internal_plet _ -> - failwith "encountered unexpected internal node when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered unexpected internal node when converting to ANF") diff --git a/src/c_backend.ml b/src/c_backend.ml index 97477163..b198c340 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -441,10 +441,8 @@ let analyze_primop' ctx id args typ = | "eq_bit", [AV_C_fragment (a, _); AV_C_fragment (b, _)] -> AE_val (AV_C_fragment (F_op (a, "==", b), typ)) - (* - | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] -> + | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] when is_stack_typ ctx typ -> AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), typ)) - *) | "undefined_bit", _ -> AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ)) diff --git a/src/reporting.ml b/src/reporting.ml index 358a99a8..3f5f1627 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -254,7 +254,7 @@ let issues = "\n\nPlease report this as an issue on GitHub at https://github.com let dest_err = function | Err_general (l, m) -> ("Error", false, Loc l, m) | Err_unreachable (l, (file, line, _, _), m) -> - ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m ^ issues) + ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)\n" file line), false, Loc l, m ^ issues) | Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "") | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m) | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m) diff --git a/src/rewrites.ml b/src/rewrites.ml index 53a20465..f10c0059 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1739,6 +1739,7 @@ let updates_vars exp = (u || lexp_is_local lexp (env_of exp), E_assign (lexp, exp)) in fst (fold_exp { (compute_exp_alg false (||)) with e_assign = e_assign } exp) + (*Expects to be called after rewrite_defs; thus the following should not appear: internal_exp of any form lit vectors in patterns or expressions @@ -1762,72 +1763,18 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f let effects = union_eff_exps exps' in let block = E_aux (E_block exps', (gen_loc l, mk_tannot env unit_typ effects)) in [fix_eff_exp (E_aux (E_var(le', e', block), annot))] - (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps -> - let vars_t = introduced_variables t in - let vars_e = introduced_variables e in - let new_vars = Envmap.intersect vars_t vars_e in - if Envmap.is_empty new_vars - then (rewrite_base exp)::walker exps - else - let new_nmap = match nmap with - | None -> Some(Nexpmap.empty,new_vars) - | Some(nm,s) -> Some(nm, Envmap.union new_vars s) in - let c' = rewrite_base c in - let t' = rewriters.rewrite_exp rewriters new_nmap t in - let e' = rewriters.rewrite_exp rewriters new_nmap e in - let exps' = walker exps in - fst ((Envmap.fold - (fun (res,effects) i (t,e) -> - let bitlit = E_aux (E_lit (L_aux(L_zero, Parse_ast.Generated l)), - (Parse_ast.Generated l, simple_annot bit_t)) in - let rangelit = E_aux (E_lit (L_aux (L_num 0, Parse_ast.Generated l)), - (Parse_ast.Generated l, simple_annot nat_t)) in - let set_exp = - match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> bitlit - | Tapp("range", _) | Tapp("atom", _) -> rangelit - | Tapp("vector", [_;_;_;TA_typ ( {t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})]) - | Tapp(("reg"|"register"),[TA_typ ({t = Tapp("vector", - [_;_;_;TA_typ ( {t=Tid "bit"} - | {t=Tabbrev(_,{t=Tid "bit"})})])})]) - | Tabbrev(_,{t = Tapp("vector", - [_;_;_;TA_typ ( {t=Tid "bit"} - | {t=Tabbrev(_,{t=Tid "bit"})})])}) -> - E_aux (E_vector_indexed([], Def_val_aux(Def_val_dec bitlit, - (Parse_ast.Generated l,simple_annot bit_t))), - (Parse_ast.Generated l, simple_annot t)) - | _ -> e in - let unioneffs = union_effects effects (get_effsum_exp set_exp) in - ([E_aux (E_var (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Generated l)), - (Parse_ast.Generated l, (tag_annot t Emp_intro))), - set_exp, - E_aux (E_block res, (Parse_ast.Generated l, (simple_annot_efr unit_t effects)))), - (Parse_ast.Generated l, simple_annot_efr unit_t unioneffs))],unioneffs))) - (E_aux(E_if(c',t',e'),(Parse_ast.Generated l, annot))::exps',eff_union_exps (c'::t'::e'::exps')) new_vars)*) | e::exps -> (rewrite_rec e)::(walker exps) in - check_exp (env_of full_exp) - (E_aux (E_block (List.map strip_exp (walker exps)), (l, ()))) (typ_of full_exp) + E_aux (E_block (walker exps), annot) + | E_assign(le,e) when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) -> let (le', re') = rewrite_lexp_to_rhs le in let e' = re' (rewrite_base e) in let block = annot_exp (E_block []) (gen_loc l) (env_of full_exp) unit_typ in - check_exp (env_of full_exp) - (strip_exp (E_aux (E_var(le', e', block), annot))) (typ_of full_exp) - | _ -> rewrite_base full_exp - -(*let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) = - let rewrap le = LEXP_aux(le,annot) in - let rewrite_base = rewrite_lexp rewriters in - match lexp, annot with - | (LEXP_id id | LEXP_cast (_,id)), (l, Some (env, typ, eff)) -> - (match Env.lookup_id id env with - | Unbound | Local _ -> - LEXP_aux (lexp, (l, Some (env, typ, union_effects eff (mk_effect [BE_lset])))) - | _ -> rewrap lexp) - | _ -> rewrite_base le*) + E_aux (E_var (le', e', block), annot) + | _ -> rewrite_base full_exp let rewrite_defs_exp_lift_assign defs = rewrite_defs_base {rewrite_exp = rewrite_exp_lift_assign_intro; @@ -1869,56 +1816,6 @@ let rewrite_register_ref_writes (Defs defs) = | [] -> [] in Defs (rewrite (write_reg_spec @ defs)) - (* rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } - (Defs (write_reg_spec @ defs)) *) - - -(*let rewrite_exp_separate_ints rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) = - (*let tparms,t,tag,nexps,eff,cum_eff,bounds = match annot with - | Base((tparms,t),tag,nexps,eff,cum_eff,bounds) -> tparms,t,tag,nexps,eff,cum_eff,bounds - | _ -> [],unit_t,Emp_local,[],pure_e,pure_e,nob in*) - let rewrap e = E_aux (e,annot) in - (*let rewrap_effects e effsum = - E_aux (e,(l,Base ((tparms,t),tag,nexps,eff,effsum,bounds))) in*) - let rewrite_rec = rewriters.rewrite_exp rewriters in - let rewrite_base = rewrite_exp rewriters in - match exp with - | E_lit (L_aux (((L_num _) as lit),_)) -> - (match (is_within_machine64 t nexps) with - | Yes -> let _ = Printf.eprintf "Rewriter of num_const, within 64bit int yes\n" in rewrite_base full_exp - | Maybe -> let _ = Printf.eprintf "Rewriter of num_const, within 64bit int maybe\n" in rewrite_base full_exp - | No -> let _ = Printf.eprintf "Rewriter of num_const, within 64bit int no\n" in E_aux(E_app(Id_aux (Id "integer_of_int",l),[rewrite_base full_exp]), - (l, Base((tparms,t),External(None),nexps,eff,cum_eff,bounds)))) - | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite_rec exp)) - | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite_rec exps)) - | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite_rec el,id,rewrite_rec er)) - | E_for (id, e1, e2, e3, o, body) -> - rewrap (E_for (id, rewrite_rec e1, rewrite_rec e2, rewrite_rec e3, o, rewrite_rec body)) - | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite_rec vec,rewrite_rec index)) - | E_vector_subrange (vec,i1,i2) -> - rewrap (E_vector_subrange (rewrite_rec vec,rewrite_rec i1,rewrite_rec i2)) - | E_vector_update (vec,index,new_v) -> - rewrap (E_vector_update (rewrite_rec vec,rewrite_rec index,rewrite_rec new_v)) - | E_vector_update_subrange (vec,i1,i2,new_v) -> - rewrap (E_vector_update_subrange (rewrite_rec vec,rewrite_rec i1,rewrite_rec i2,rewrite_rec new_v)) - | E_case (exp ,pexps) -> - rewrap (E_case (rewrite_rec exp, - (List.map - (fun (Pat_aux (Pat_exp(p,e),pannot)) -> - Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite_rec e),pannot)) pexps))) - | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite_rec body)) - | E_var (lexp,exp,body) -> - rewrap (E_var (rewriters.rewrite_lexp rewriters nmap lexp, rewrite_rec exp, rewrite_rec body)) - | _ -> rewrite_base full_exp - -let rewrite_defs_separate_numbs defs = rewrite_defs_base - {rewrite_exp = rewrite_exp_separate_ints; - rewrite_pat = rewrite_pat; - rewrite_let = rewrite_let; (*will likely need a new one?*) - rewrite_lexp = rewrite_lexp; (*will likely need a new one?*) - rewrite_fun = rewrite_fun; - rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} defs*) (* Remove redundant return statements, and translate remaining ones into an (effectful) call to builtin function "early_return" (in the Lem shallow |