diff options
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 100 |
1 files changed, 62 insertions, 38 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 689df577..5f3930b6 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -51,7 +51,7 @@ open Ast open Util open Ast_util -open Big_int +module Big_int = Nat_big_num let opt_undefined_gen = ref false let opt_magic_hash = ref false @@ -131,7 +131,7 @@ let string_of_parse_id_aux = function | Parse_ast.DeIid v -> v let string_contains str char = - try (String.index str char; true) with + try (ignore (String.index str char); true) with | Not_found -> false let to_ast_id (Parse_ast.Id_aux(id, l)) = @@ -185,12 +185,12 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) let make_r bot top = match bot,top with | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) | bot,(Parse_ast.ATyp_aux(_,l) as top) -> Parse_ast.ATyp_aux((Parse_ast.ATyp_sum ((Parse_ast.ATyp_aux (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant unit_big_int,Parse_ast.Unknown)), + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), Parse_ast.Unknown)), (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in let base = to_ast_nexp k_env b in @@ -206,9 +206,9 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> let make_sub_one t = match t with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (sub_big_int t unit_big_int),l) + | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (minus_big_int unit_big_int),Parse_ast.Unknown)), + (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.negate (Big_int.of_int 1)),Parse_ast.Unknown)), Parse_ast.Unknown)) in let (base,rise) = match def_ord with | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r) @@ -291,10 +291,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in (match mk with - | Some(k) -> (match k.k with - | K_Efct -> Effect_var v - | K_infer -> k.k <- K_Efct; Effect_var v - | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k)) + | Some k -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k) | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_set(effects) -> Effect_set( List.map @@ -475,6 +472,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | None -> E_block(List.map (to_ast_exp k_env def_ord) exps)) | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env def_ord) exps) | Parse_ast.E_id(id) -> E_id(to_ast_id id) + | Parse_ast.E_ref(id) -> E_ref(to_ast_id id) | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit) | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env def_ord typ, to_ast_exp k_env def_ord exp) | Parse_ast.E_app(f,args) -> @@ -516,18 +514,21 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps) | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp) | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp) + | Parse_ast.E_var(lexp,exp1,exp2) -> E_var(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp) | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc) | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp) | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp) | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp) | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg) + | _ -> raise (Reporting_basic.err_unreachable l "Unparsable construct in to_ast_exp") ), (l,())) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = LEXP_aux( (match exp with | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) + | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp) | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) | Parse_ast.E_tuple(tups) -> @@ -535,7 +536,7 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l let is_ok_in_tup (LEXP_aux (le,(l,_))) = match le with | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () - | LEXP_memory _ -> + | LEXP_memory _ | LEXP_deref _ -> typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in List.iter is_ok_in_tup ltups; LEXP_tup(ltups) @@ -690,13 +691,12 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_de let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,())) in (* Add check that all enums have unique names *) let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in td_enum, (names,k_env,def_ord) - | Parse_ast.TD_register(id,t1,t2,ranges) -> + | Parse_ast.TD_bitfield(id,typ,ranges) -> let id = to_ast_id id in let key = id_to_string id in - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in - TD_aux(TD_register(id,n1,n2,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)) + let typ = to_ast_typ k_env def_ord typ in + let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in + TD_aux(TD_bitfield(id,typ,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)) let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def) envs_out = match td with @@ -750,7 +750,7 @@ let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.funde (*let _ = Printf.eprintf "to_ast_fundef\n" in*) let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord) - + type def_progress = No_def | Def_place_holder of id * Parse_ast.l @@ -826,6 +826,9 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | Parse_ast.DEF_reg_dec(dec) -> let d = to_ast_dec envs dec in ((Finished(DEF_reg_dec(d))),envs),partial_defs + | Parse_ast.DEF_internal_mutrec _ -> + (* Should never occur because of remove_mutrec *) + typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) -> (match sd with | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> @@ -890,8 +893,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out ((Finished def), envs),partial_defs | _, true -> typ_error l "Scattered definition ended multiple times" (Some id) None None - | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) - + | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) + let rec to_ast_defs_helper envs partial_defs = function | [] -> ([],envs,partial_defs) | d::ds -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in @@ -943,20 +946,26 @@ let initial_kind_env = ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); + ("ref", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) }); - ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); + ("vector", {k = K_Lam( [{k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) }); ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} ); ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ] +let exp_of_string order str = + let exp = Parser.exp_eof Lexer.token (Lexing.from_string str) in + to_ast_exp initial_kind_env order exp + let typschm_of_string order str = - let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in + let typschm = Parser.typschm_eof Lexer.token (Lexing.from_string str) in let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in typschm -let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false)) +let extern_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false)) +let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> None), false)) let val_spec_ids (Defs defs) = let val_spec_id (VS_aux (vs_aux, _)) = @@ -991,28 +1000,39 @@ let undefined_typschm id typq = let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef]))) +let have_undefined_builtins = ref false + let generate_undefineds vs_ids (Defs defs) = let gen_vs id str = - if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str] + if (IdSet.mem id vs_ids) then [] else [extern_of_string dec_ord id str] in - let undefined_builtins = List.concat - [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}"; - gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}"; - gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}"; - gen_vs (mk_id "undefined_int") "unit -> int effect {undef}"; - gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}"; - gen_vs (mk_id "undefined_real") "unit -> real effect {undef}"; - gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; - gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; - gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; - (* FIXME: How to handle inc/dec order correctly? *) - gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; - (* Only used with lem_mwords *) - gen_vs (mk_id "undefined_bitvector") "forall 'n 'm. (atom('n), atom('m)) -> vector('n, 'm, dec,bit) effect {undef}"; - gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] + let undefined_builtins = + if !have_undefined_builtins then + [] + else + begin + have_undefined_builtins := true; + List.concat + [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}"; + gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}"; + gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}"; + gen_vs (mk_id "undefined_int") "unit -> int effect {undef}"; + gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}"; + gen_vs (mk_id "undefined_real") "unit -> real effect {undef}"; + gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; + gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; + gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; + (* FIXME: How to handle inc/dec order correctly? *) + gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; + (* Only used with lem_mwords *) + gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}"; + gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] + end in let undefined_tu = function | Tu_aux (Tu_id id, _) -> mk_exp (E_id id) + | Tu_aux (Tu_ty_id (Typ_aux (Typ_tup typs, _), id), _) -> + mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs)) | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef])) in let undefined_td = function @@ -1077,3 +1097,7 @@ let process_ast order defs = let ast = generate_undefineds vs_ids ast in generate_initialize_registers vs_ids ast end + +let ast_of_def_string order str = + let def = Parser.def_eof Lexer.token (Lexing.from_string str) in + process_ast order (Parse_ast.Defs [def]) |