diff options
| -rw-r--r-- | lib/sail.h | 9 | ||||
| -rw-r--r-- | src/c_backend.ml | 4 | ||||
| -rw-r--r-- | src/rewrites.ml | 2 | ||||
| -rw-r--r-- | src/specialize.ml | 47 | ||||
| -rw-r--r-- | test/c/option.expect | 3 | ||||
| -rw-r--r-- | test/c/option.sail | 40 | ||||
| -rw-r--r-- | test/c/sail.h | 4 |
7 files changed, 91 insertions, 18 deletions
@@ -12,6 +12,10 @@ typedef int unit; #define UNIT 0 +unit undefined_unit(const unit u) { + return UNIT; +} + typedef struct { mp_bitcnt_t len; mpz_t *bits; @@ -867,7 +871,7 @@ void load_image(char *file) { FILE *fp = fopen(file, "r"); if (!fp) { - fprintf(stderr, "Image file could not be loaded\n"); + fprintf(stderr, "Image file %s could not be loaded\n", file); exit(EXIT_FAILURE); } @@ -898,8 +902,7 @@ void load_instr(uint64_t addr, uint32_t instr) { // ***** Setup and cleanup functions for library code ***** -void setup_library(char *file) { - load_image(file); +void setup_library(void) { mpf_set_default_prec(FLOAT_PRECISION); mpz_init(eq_bits_test); } diff --git a/src/c_backend.ml b/src/c_backend.ml index d7d9b27f..6ab45574 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -837,7 +837,7 @@ let rec is_stack_ctyp ctyp = match ctyp with | CT_uint64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true | CT_bv _ | CT_mpz | CT_real | CT_string | CT_list _ | CT_vector _ -> false | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields - | CT_variant (_, ctors) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors + | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (*FIXME*) | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps | CT_ref ctyp -> is_stack_ctyp ctyp @@ -1498,7 +1498,7 @@ let compile_funcall ctx id args typ = let rec compile_match ctx apat cval case_label = match apat, cval with - | AP_id pid, (frag, ctyp) when is_ct_variant ctyp -> + | AP_id pid, (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], [] | AP_global (pid, _), _ -> [icopy (CL_id pid) cval], [] diff --git a/src/rewrites.ml b/src/rewrites.ml index d6144755..af621b47 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3036,6 +3036,8 @@ let rewrite_defs_c = [ ("constraint", rewrite_constraint); ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); + ("merge function clauses", merge_funcls); + ("recheck_defs", recheck_defs) ] let rewrite_defs_interpreter = [ diff --git a/src/specialize.ml b/src/specialize.ml index 0a4e0fbb..1b978fbc 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -150,8 +150,16 @@ let id_of_instantiation id instantiation = let str = string_of_instantiation instantiation in prepend_id (str ^ "#") id +let rec variant_generic_typ id (Defs defs) = + match defs with + | DEF_type (TD_aux (TD_variant (id', _, typq, _, _), _)) :: _ when Id.compare id id' = 0 -> + mk_typ (Typ_app (id', List.map (fun kopt -> mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))) (quant_kopts typq))) + | _ :: defs -> variant_generic_typ id (Defs defs) + | [] -> failwith ("No variant with id " ^ string_of_id id) + (* Returns a list of all the instantiations of a function id in an - ast. *) + ast. Also works with union constructors, and searches for them in + patterns. *) let rec instantiations_of id ast = let instantiations = ref [] in @@ -163,8 +171,30 @@ let rec instantiations_of id ast = | exp -> exp in - let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in - let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in + (* We need to to check patterns in case id is a union constructor + that is never called like a function. *) + let inspect_pat = function + | P_aux (P_app (id', _), annot) as pat when Id.compare id id' = 0 -> + begin match Type_check.typ_of_annot annot with + | Typ_aux (Typ_app (variant_id, _), _) as typ -> + let open Type_check in + let instantiation, _, _ = unify (fst annot) (env_of_annot annot) + (variant_generic_typ variant_id ast) + typ + in + instantiations := fix_instantiation instantiation :: !instantiations; + pat + | Typ_aux (Typ_id variant_id, _) -> pat + | _ -> failwith ("Union constructor " ^ string_of_pat pat ^ " has non-union type") + end + | pat -> pat + in + + let rewrite_pat = { id_pat_alg with p_aux = (fun (pat, annot) -> inspect_pat (P_aux (pat, annot))) } in + let rewrite_exp = { id_exp_alg with pat_alg = rewrite_pat; + e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in + let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); + rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in !instantiations @@ -329,7 +359,6 @@ let remove_unused_valspecs env ast = match defs with | def :: defs when is_fundef id def -> remove_unused (Defs defs) id | def :: defs when is_valspec id def -> - prerr_endline ("Removing: " ^ string_of_id id); remove_unused (Defs defs) id | DEF_overload (overload_id, overloads) :: defs -> begin @@ -379,13 +408,6 @@ let specialize_ids ids ast = (***** Specialising polymorphic variant types, e.g. option *****) -let rec variant_generic_typ id (Defs defs) = - match defs with - | DEF_type (TD_aux (TD_variant (id', _, typq, _, _), _)) :: _ -> - mk_typ (Typ_app (id', List.map (fun kopt -> mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))) (quant_kopts typq))) - | _ :: defs -> variant_generic_typ id (Defs defs) - | [] -> failwith ("No variant with id " ^ string_of_id id) - let rewrite_polymorphic_constructors id ast = let rewrite_e_aux = function | E_aux (E_app (id', args), annot) as exp when Id.compare id id' = 0 -> @@ -461,6 +483,5 @@ let rec specialize ast env = if IdSet.is_empty ids then specialize_variants ast env else - (prerr_endline (Util.string_of_list ", " string_of_id (IdSet.elements ids)); let ast, env = specialize_ids ids ast in - specialize ast env) + specialize ast env diff --git a/test/c/option.expect b/test/c/option.expect new file mode 100644 index 00000000..f099c714 --- /dev/null +++ b/test/c/option.expect @@ -0,0 +1,3 @@ +a = 5 +b = 0xF +c = 0xA diff --git a/test/c/option.sail b/test/c/option.sail new file mode 100644 index 00000000..1ca59372 --- /dev/null +++ b/test/c/option.sail @@ -0,0 +1,40 @@ +default Order dec + +val print = "print_endline" : string -> unit + +val "print_int" : (string, int) -> unit +val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit + +union option ('a : Type) = { + None : unit, + Some : 'a +} + +union soption ('a : Type) = { + sNone : unit, + sSome : 'a +} + +val main : unit -> unit + +function main () = { + let x : option(int) = Some(5); + let y : option(int) = None(); + let z : option(vector(4, dec, bit)) = Some(0xF); + + match x { + Some(a) => print_int("a = ", 5), + None() => print("None") + }; + + match z { + Some(b) => print_bits("b = ", b), + None() => print("None") + }; + + let q : soption(vector(4, dec, bit)) = sSome(0xA); + + match q { + sSome(c) => print_bits("c = ", c) + } +} diff --git a/test/c/sail.h b/test/c/sail.h index b29e9535..c0f2674b 100644 --- a/test/c/sail.h +++ b/test/c/sail.h @@ -12,6 +12,10 @@ typedef int unit; #define UNIT 0 +unit undefined_unit(const unit u) { + return UNIT; +} + typedef struct { mp_bitcnt_t len; mpz_t *bits; |