From bde6c320997b104b0dcdc24259875a1791416d51 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 11 Jul 2017 16:34:33 +0100 Subject: Various typechecker improvements: * Fixed a bug where non-polymorphic function return types could be incorrect * Added support for LEXP_memory AST node * Flow typing constraint generation for all inequality operators * Better support for increasing vector indices in field access expressions --- mips_new_tc/mips_insts.sail | 43 ++++++++++---------- src/type_check_new.ml | 76 ++++++++++++++++++++++++++---------- test/typecheck/fail/funret1.sail | 16 ++++++++ test/typecheck/fail/funret2.sail | 16 ++++++++ test/typecheck/fail/funret3.sail | 16 ++++++++ test/typecheck/pass/lexp_memory.sail | 65 ++++++++++++++++++++++++++++++ test/typecheck/pass/union_infer.sail | 16 ++++++++ 7 files changed, 208 insertions(+), 40 deletions(-) create mode 100644 test/typecheck/fail/funret1.sail create mode 100644 test/typecheck/fail/funret2.sail create mode 100644 test/typecheck/fail/funret3.sail create mode 100644 test/typecheck/pass/lexp_memory.sail create mode 100644 test/typecheck/pass/union_infer.sail diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail index d85ba0a5..07d4d841 100644 --- a/mips_new_tc/mips_insts.sail +++ b/mips_new_tc/mips_insts.sail @@ -35,9 +35,11 @@ (* misp_insts.sail: mips instruction decode and execute clauses and AST node declarations *) -scattered function unit execute scattered typedef ast = const union +val ast -> unit effect pure execute +scattered function unit execute + val bit[32] -> option effect pure decode scattered function option decode @@ -56,7 +58,7 @@ function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = function clause execute (DADDIU (rs, rt, imm)) = { - wGPR(rt) := rGPR(rs) + EXTS(imm) + wGPR(rt) := rGPR(rs) + (bit[64]) (EXTS(imm)) } (* DADDU Doubleword Add Unsigned -- another very simple instruction, @@ -82,7 +84,7 @@ function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = function clause execute (DADDI (rs, rt, imm)) = { - let (bit[65]) sum65 = (EXTS(rGPR(rs)) + EXTS(imm)) in + let (bit[65]) sum65 = ((bit[65]) (EXTS(rGPR(rs))) + (bit[65]) (EXTS(imm))) in { if (sum65[64] != sum65[63]) then (SignalException(Ov)) @@ -101,7 +103,7 @@ function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b0000 function clause execute (DADD (rs, rt, rd)) = { - let (bit[65]) sum65 = (EXTS(rGPR(rs)) + EXTS(rGPR(rt))) in + let (bit[65]) sum65 = ((bit[65]) (EXTS(rGPR(rs))) + (bit[65]) (EXTS(rGPR(rt)))) in { if sum65[64] != sum65[63] then (SignalException(Ov)) @@ -117,18 +119,18 @@ union ast member regregreg ADD function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100000) = Some(ADD(rs, rt, rd)) -function clause execute (ADD(rs, rt, rd)) = +function clause execute (ADD(rs, rt, rd)) = { (bit[64]) opA := rGPR(rs); (bit[64]) opB := rGPR(rt); if NotWordVal(opA) | NotWordVal(opB) then - wGPR(rd) := undefined (* XXX could exit instead *) + wGPR(rd) := (bit[64]) undefined (* XXX could exit instead *) else - let (bit[33]) sum33 = (EXTS(opA[31 .. 0]) + EXTS(opB[31 .. 0])) in + let (bit[33]) sum33 = ((bit[33]) (EXTS(opA[31 .. 0])) + (bit[33]) (EXTS(opB[31 .. 0]))) in if sum33[32] != sum33[31] then (SignalException(Ov)) else - wGPR(rd) := EXTS(sum33[31..0]) + wGPR(rd) := (bit[64]) (EXTS(sum33[31..0])) } (* ADDI 32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception *) @@ -1011,7 +1013,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = (* Co-opt syscall 0xfffff for use as thread start in pccmem *) union ast member unit SYSCALL_THREAD_START function clause decode (0b000000 : 0xfffff : 0b001100) = - Some(SYSCALL_THREAD_START) + Some((ast) SYSCALL_THREAD_START) function clause execute (SYSCALL_THREAD_START) = () @@ -1024,7 +1026,7 @@ function clause execute (ImplementationDefinedStopFetching) = () union ast member unit SYSCALL function clause decode (0b000000 : (bit[20]) code : 0b001100) = - Some(SYSCALL) (* code is ignored *) + Some((ast) SYSCALL) (* code is ignored *) function clause execute (SYSCALL) = { (SignalException(Sys)) @@ -1033,7 +1035,7 @@ function clause execute (SYSCALL) = (* BREAK is identical to SYSCALL exception for the exception raised *) union ast member unit BREAK function clause decode (0b000000 : (bit[20]) code : 0b001101) = - Some(BREAK) (* code is ignored *) + Some((ast) BREAK) (* code is ignored *) function clause execute (BREAK) = { (SignalException(Bp)) @@ -1042,7 +1044,7 @@ function clause execute (BREAK) = (* Accept WAIT as a NOP *) union ast member unit WAIT function clause decode (0b010000 : 0x80000 : 0b100000) = - Some(WAIT) (* we only accept code == 0 *) + Some((ast) WAIT) (* we only accept code == 0 *) function clause execute (WAIT) = { nextPC := PC; } @@ -1397,7 +1399,7 @@ function clause execute (PREF(base, op, imm)) = (* SYNC - Memory barrier *) union ast member unit SYNC function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = - Some(SYNC()) (* stype is currently ignored *) + Some((ast) SYNC) (* stype is currently ignored *) function clause execute(SYNC) = MEM_sync() @@ -1479,10 +1481,10 @@ function clause execute (MFC0(rt, rd, sel, double)) = { (* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *) union ast member unit HCF function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) = - Some(HCF()) + Some((ast) HCF) function clause decode (0b010000 : 0b00100 : (regno) rt : 0b11010 : 0b00000000000) = - Some(HCF()) + Some((ast) HCF) function clause execute (HCF) = () (* halt instruction actually executed by interpreter framework *) @@ -1580,21 +1582,21 @@ function unit TLBWriteEntry((TLBIndexT) idx) = { } *) union ast member TLBWI -function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some(TLBWI) +function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some((ast) TLBWI) function clause execute (TLBWI) = { checkCP0Access(); TLBWriteEntry(TLBIndex); } union ast member TLBWR -function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some(TLBWR) +function clause decode (0b010000 : 0b10000000000000000000 : 0b000110) = Some((ast) TLBWR) function clause execute (TLBWR) = { checkCP0Access(); TLBWriteEntry(TLBRandom); } union ast member TLBR -function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some(TLBR) +function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some((ast) TLBR) function clause execute (TLBR) = { checkCP0Access(); let entry = TLBEntries[TLBIndex] in { @@ -1620,7 +1622,7 @@ function clause execute (TLBR) = { } union ast member TLBP -function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some(TLBP) +function clause decode (0b010000 : 0b10000000000000000000 : 0b001000) = Some((ast) TLBP) function clause execute ((TLBP)) = { checkCP0Access(); let result = tlbSearch(TLBEntryHi) in @@ -1655,8 +1657,9 @@ function clause execute (RDHWR(rt, rd)) = { } union ast member unit ERET + function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) = - Some(ERET) + Some((ast) ERET) function clause execute (ERET) = { checkCP0Access(); diff --git a/src/type_check_new.ml b/src/type_check_new.ml index d60d8280..133c6db7 100644 --- a/src/type_check_new.ml +++ b/src/type_check_new.ml @@ -46,7 +46,7 @@ open Util open Ast_util open Big_int -let debug = ref 1 +let debug = ref 2 let depth = ref 0 let rec indent n = match n with @@ -848,6 +848,7 @@ let rec normalize_typ env (Typ_aux (typ, l)) = end | Typ_var kid -> Tnf_var kid | Typ_tup typs -> Tnf_tup (List.map (normalize_typ env) typs) + | Typ_app (f, []) -> normalize_typ env (Typ_aux (Typ_id f, l)) | Typ_app (Id_aux (Id "range", _), [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]) -> let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(n1, nvar kid); (nvar kid, n2)])) @@ -1181,6 +1182,12 @@ let unify l env typ1 typ2 = | Typ_id v1, Typ_id v2 -> if Id.compare v1 v2 = 0 then KBindings.empty else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) + | Typ_id v1, Typ_app (f2, []) -> + if Id.compare v1 f2 = 0 then KBindings.empty + else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) + | Typ_app (f1, []), Typ_id v2 -> + if Id.compare f1 v2 = 0 then KBindings.empty + else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) | Typ_var kid, _ when KidSet.mem kid goals -> KBindings.singleton kid (U_typ typ2) | Typ_var kid1, Typ_var kid2 when Kid.compare kid1 kid2 = 0 -> KBindings.empty | Typ_tup typs1, Typ_tup typs2 -> @@ -1382,6 +1389,18 @@ let rec infer_flow env (E_aux (exp_aux, (l, _))) = let n1 = destructure_atom_nexp (typ_of x) in let n2 = destructure_atom_nexp (typ_of y) in [], [nc_lteq n1 n2] + | E_app (f, [x; y]) when string_of_id f = "gteq_atom_atom" -> + let n1 = destructure_atom_nexp (typ_of x) in + let n2 = destructure_atom_nexp (typ_of y) in + [], [nc_gteq n1 n2] + | E_app (f, [x; y]) when string_of_id f = "lt_atom_atom" -> + let n1 = destructure_atom_nexp (typ_of x) in + let n2 = destructure_atom_nexp (typ_of y) in + [], [nc_lt n1 n2] + | E_app (f, [x; y]) when string_of_id f = "gt_atom_atom" -> + let n1 = destructure_atom_nexp (typ_of x) in + let n2 = destructure_atom_nexp (typ_of y) in + [], [nc_gt n1 n2] | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" -> let kid = Env.fresh_kid env in let c = destructure_atom (typ_of y) in @@ -1436,7 +1455,10 @@ let rec match_typ (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) = | Typ_id v, Typ_app (f, _) when string_of_id v = "nat" && string_of_id f = "range" -> true | Typ_id v, Typ_app (f, _) when string_of_id v = "int" && string_of_id f = "range" -> true | Typ_app (f1, _), Typ_app (f2, _) when string_of_id f1 = "range" && string_of_id f2 = "atom" -> true + | Typ_app (f1, _), Typ_app (f2, _) when string_of_id f1 = "atom" && string_of_id f2 = "range" -> true | Typ_app (f1, _), Typ_app (f2, _) when Id.compare f1 f2 = 0 -> true + | Typ_id v1, Typ_app (f2, _) when Id.compare v1 f2 = 0 -> true + | Typ_app (f1, _), Typ_id v2 when Id.compare f1 v2 = 0 -> true | _, _ -> false let rec filter_casts env from_typ to_typ casts = @@ -1670,7 +1692,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | Typ_tup typs -> typs | _ -> [typ] in - match ctor_typ with + match Env.expand_synonyms env ctor_typ with | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) -> begin try @@ -1762,6 +1784,8 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign (annot_lexp (LEXP_field (annot_lexp_effect (LEXP_id v) regtyp (mk_effect [BE_wreg]), field)) vec_typ) checked_exp, env | _ -> typ_error l "Field l-expression has invalid type" end + | LEXP_memory (f, xs) -> + check_exp env (E_aux (E_app (f, xs @ [exp]), (l, ()))) unit_typ, env | _ -> let inferred_exp = irule infer_exp env exp in let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in @@ -1852,7 +1876,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | Local (_, typ) | Enum typ -> annot_exp (E_id v) typ | Register typ -> annot_exp_effect (E_id v) typ (mk_effect [BE_rreg]) | Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound") - | Union _ -> typ_error l ("Cannot infer the type of polymorphic union indentifier " ^ string_of_id v) + | Union (typq, typ) -> + if quant_items typq = [] + then annot_exp (E_id v) typ + else typ_error l ("Cannot infer the type of polymorphic union indentifier " ^ string_of_id v) end | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit) | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)]))) @@ -1868,7 +1895,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = match Env.expand_synonyms env (typ_of inferred_exp) with (* Accessing a (bit) field of a register *) | Typ_aux (Typ_id regtyp, _) when Env.is_regtyp regtyp env -> - typ_print "REGTYP"; let base, top, ranges = Env.get_regtyp regtyp env in let range, _ = try List.find (fun (_, id) -> Id.compare id field = 0) ranges with @@ -1877,17 +1903,22 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = begin match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant 1) (mk_typ (Typ_id (mk_id "bit"))) in + let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in annot_exp (E_field (inferred_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) (mk_typ (Typ_id (mk_id "bit"))) in + let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) bit_typ in + annot_exp (E_field (inferred_exp, field)) vec_typ + | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) -> + let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in annot_exp (E_field (inferred_exp, field)) vec_typ - | _, _ -> typ_error l "Not implemented this register field type yet..." (* FIXME *) + | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) -> + let vec_typ = dvector_typ env (nconstant n) (nconstant (m - n + 1)) bit_typ in + annot_exp (E_field (inferred_exp, field)) vec_typ + | _, _ -> typ_error l "Invalid register field type" end (* Accessing a field of a record *) | Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env -> begin - typ_print "RECTYP"; let inferred_acc = infer_funapp' l (Env.no_casts env) field (Env.get_accessor field env) [strip_exp inferred_exp] None in match inferred_acc with | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) @@ -2027,18 +2058,23 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = (quants', typs', ret_typ') end in - match f_typ with - | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) -> - let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) typ_args typ_ret in - let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in - let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in - annot_exp (E_app (f, xs_reordered)) typ_ret eff - | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) -> - let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) [typ_arg] typ_ret in - let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in - let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in - annot_exp (E_app (f, xs_reordered)) typ_ret eff - | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type") + let exp = + match Env.expand_synonyms env f_typ with + | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) -> + let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) typ_args typ_ret in + let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in + let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in + annot_exp (E_app (f, xs_reordered)) typ_ret eff + | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) -> + let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) [typ_arg] typ_ret in + let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in + let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in + annot_exp (E_app (f, xs_reordered)) typ_ret eff + | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type") + in + match ret_ctx_typ with + | None -> exp + | Some rct -> type_coercion env exp rct (**************************************************************************) (* 6. Effect system *) diff --git a/test/typecheck/fail/funret1.sail b/test/typecheck/fail/funret1.sail new file mode 100644 index 00000000..09a4fd54 --- /dev/null +++ b/test/typecheck/fail/funret1.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + +let (option) x = C + diff --git a/test/typecheck/fail/funret2.sail b/test/typecheck/fail/funret2.sail new file mode 100644 index 00000000..19536599 --- /dev/null +++ b/test/typecheck/fail/funret2.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option test2 () = C diff --git a/test/typecheck/fail/funret3.sail b/test/typecheck/fail/funret3.sail new file mode 100644 index 00000000..d178f2ad --- /dev/null +++ b/test/typecheck/fail/funret3.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<(option)> test () = Some(C) diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail new file mode 100644 index 00000000..83313ac7 --- /dev/null +++ b/test/typecheck/pass/lexp_memory.sail @@ -0,0 +1,65 @@ +default Order dec + +register (bit[64]) GPR00 (* should never be read or written *) +register (bit[64]) GPR01 +register (bit[64]) GPR02 +register (bit[64]) GPR03 +register (bit[64]) GPR04 +register (bit[64]) GPR05 +register (bit[64]) GPR06 +register (bit[64]) GPR07 +register (bit[64]) GPR08 +register (bit[64]) GPR09 +register (bit[64]) GPR10 +register (bit[64]) GPR11 +register (bit[64]) GPR12 +register (bit[64]) GPR13 +register (bit[64]) GPR14 +register (bit[64]) GPR15 +register (bit[64]) GPR16 +register (bit[64]) GPR17 +register (bit[64]) GPR18 +register (bit[64]) GPR19 +register (bit[64]) GPR20 +register (bit[64]) GPR21 +register (bit[64]) GPR22 +register (bit[64]) GPR23 +register (bit[64]) GPR24 +register (bit[64]) GPR25 +register (bit[64]) GPR26 +register (bit[64]) GPR27 +register (bit[64]) GPR28 +register (bit[64]) GPR29 +register (bit[64]) GPR30 +register (bit[64]) GPR31 + +let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = + [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, + GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, + GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 + ] + +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec + +overload (deinfix ==) [eq_vec] + +val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec +val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned +val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref + +val (bit[5], bit[64]) -> unit effect {wreg} wGPR + +function unit wGPR (idx, v) = +{ + if idx == 0 then () else GPR[idx] := v +} + +function unit test () = +{ + wGPR(0b00001) := 0 +} diff --git a/test/typecheck/pass/union_infer.sail b/test/typecheck/pass/union_infer.sail new file mode 100644 index 00000000..397525e0 --- /dev/null +++ b/test/typecheck/pass/union_infer.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option test () = Some(C) -- cgit v1.2.3