From 249079742b63d43cdc4c445de3229f594c6d59fc Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 13 Jul 2017 16:42:57 +0100 Subject: Modified MIPS model so it typechecks with the new typechecker --- lib/prelude.sail | 101 ++++++++---- mips_new_tc/mips_epilogue.sail | 2 +- mips_new_tc/mips_insts.sail | 362 +++++++++++++++++++++-------------------- mips_new_tc/mips_wrappers.sail | 12 +- src/ast_util.ml | 1 + src/type_check_new.ml | 64 ++++++-- test/typecheck/run_tests.sh | 9 +- 7 files changed, 317 insertions(+), 234 deletions(-) diff --git a/lib/prelude.sail b/lib/prelude.sail index 350c6c20..9a52e5fb 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -1,32 +1,34 @@ -val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned +val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned -val forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed +val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed -val forall Nat 'n, Nat 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec +val forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec + +val forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec (* Vector access can't actually be properly polymorphic on vector direction because of the ranges being different for each type, so we overload it instead *) -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 +val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Num 'n, Num '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] (* Type safe vector subrange *) -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. +val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. +val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec -val forall Nat 'n, Nat 'l, Order 'ord. +val forall Num 'n, Num 'l, Order 'ord. (vector<'n,'l,'ord,bit>, int, int) -> list effect pure vector_subrange_bl overload vector_subrange [vector_subrange_inc; vector_subrange_dec; vector_subrange_bl] (* Type safe vector append *) -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. +val forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append val (list, list) -> list effect pure list_append @@ -37,89 +39,98 @@ overload vector_append [vec_append; list_append] val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref (* Bitvector duplication *) -val forall Nat 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate +val forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate val (bit, int) -> list effect pure duplicate_to_list -val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord. +val forall Num 'n, Num 'm, Num 'o, Order 'ord. (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits -val forall Nat 'n, Nat 'o, Order 'ord. +val forall Num 'n, Num 'o, Order 'ord. (vector<'o,'n,'ord,bit>, int) -> list effect pure duplicate_bits_to_list overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list] (* Bitvector extension *) -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. +val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz -val forall Nat 'm, Nat 'p, Order 'ord. +val forall Num 'm, Num 'p, Order 'ord. list -> vector<'p, 'm, 'ord, bit> effect pure extz_bl -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. +val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts -val forall Nat 'm, Nat 'p, Order 'ord. +val forall Num 'm, Num 'p, Order 'ord. list -> vector<'p, 'm, 'ord, bit> effect pure exts_bl +val cast forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi + overload EXTZ [extz; extz_bl] overload EXTS [exts; exts_bl] -val forall Type 'a, Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'o. +val forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask (* Adjust the start index of a decreasing bitvector *) -val cast forall Nat 'n, Nat 'm, 'n >= 'm - 1. +val cast forall Num 'n, Num 'm, 'n >= 'm - 1. vector<'n,'m,dec,bit> -> vector<'m - 1,'m,dec,bit> effect pure norm_dec -val cast forall Nat 'n, Nat 'm, Nat 'o, 'n >= 'm - 1, 'o >= 'm - 1. +val cast forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1. vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> effect pure adjust_dec (* Various casts from 0 and 1 to bitvectors *) -val cast forall Nat 'n, Nat 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec -val cast forall Nat 'n, Nat 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_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 Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec +val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec -val cast forall Nat 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool +val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool val cast bit -> bool effect pure cast_bit_bool +val cast forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. bit -> vector<'n,'m,dec,bit> effect pure cast_bit_vec + (* MSB *) -val forall Nat 'n, Nat 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant +val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant (* Arithmetic *) -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p. +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add val (nat, nat) -> nat effect pure add_nat val (int, int) -> int effect pure add_int -val forall Nat 'n, Nat 'o, Order 'ord. +val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec -val forall Nat 'n, Nat 'o, Order 'ord. +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int + +val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec -val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p. +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub val (int, int) -> int effect pure sub_int -val forall Nat 'n, Nat 'm, Order 'ord. +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int -val forall Nat 'n, Nat 'o, Order 'ord. +val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure sub_vec -val forall Nat 'n, Nat 'o, Order 'ord. +val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure sub_underflow_vec overload (deinfix +) [ add_vec; add_overflow_vec; + add_vec_int; add; add_nat; add_int @@ -133,21 +144,35 @@ overload (deinfix -) [ sub_int ] -val forall Nat 'n, Nat 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_svec +val bool -> bit effect pure bool_to_bit + +val (int, int) -> int effect pure mul_int +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure mul_vec + +overload (deinfix * ) [ + mul_vec; + mul_int +] + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure mul_svec overload (deinfix *_s) [ - add_svec + mul_svec ] -val forall Nat 'n, Nat 'o, Order 'ord. +val (bool, bool) -> bool effect pure bool_xor + +val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec overload (deinfix ^) [ + bool_xor; xor_vec ] -val forall Nat 'n, Nat 'o, Order 'ord. +val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftl overload (deinfix <<) [ @@ -230,6 +255,10 @@ val (int, int) -> int effect pure quotient overload (deinfix quot) [quotient] +val (int, int) -> int effect pure modulus + +overload (deinfix mod) [modulus] + val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure length val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper diff --git a/mips_new_tc/mips_epilogue.sail b/mips_new_tc/mips_epilogue.sail index 50993949..09ce7688 100644 --- a/mips_new_tc/mips_epilogue.sail +++ b/mips_new_tc/mips_epilogue.sail @@ -38,4 +38,4 @@ end decode end execute end ast -function option supported_instructions (instr) = Some(instr) +function option supported_instructions (ast) instr = Some(instr) diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail index 19176c72..88c78e80 100644 --- a/mips_new_tc/mips_insts.sail +++ b/mips_new_tc/mips_insts.sail @@ -32,12 +32,12 @@ (* SUCH DAMAGE. *) (*========================================================================*) -(* misp_insts.sail: mips instruction decode and execute clauses and AST node +(* misp_insts.sail: mips instruction decode and execute clauses and AST node declarations *) scattered typedef ast = const union -val ast -> unit effect pure execute +val ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} execute scattered function unit execute val bit[32] -> option effect pure decode @@ -47,13 +47,13 @@ scattered function option decode (* [D]ADD[I][U] various forms of ADD *) (**************************************************************************************) -(* DADDIU Doubleword Add Immediate Unsigned -- - the simplest possible instruction, no undefined behaviour or exceptions +(* DADDIU Doubleword Add Immediate Unsigned -- + the simplest possible instruction, no undefined behaviour or exceptions reg, reg, immediate *) union ast member regregimm16 DADDIU -function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = Some(DADDIU(rs, rt, imm)) function clause execute (DADDIU (rs, rt, imm)) = @@ -66,7 +66,7 @@ function clause execute (DADDIU (rs, rt, imm)) = union ast member regregreg DADDU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) = Some(DADDU(rs, rt, rd)) function clause execute (DADDU (rs, rt, rd)) = @@ -79,7 +79,7 @@ function clause execute (DADDU (rs, rt, rd)) = union ast member regregimm16 DADDI -function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = Some(DADDI(rs, rt, imm)) function clause execute (DADDI (rs, rt, imm)) = @@ -98,7 +98,7 @@ function clause execute (DADDI (rs, rt, imm)) = union ast member regregreg DADD -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = Some(DADD(rs, rt, rd)) function clause execute (DADD (rs, rt, rd)) = @@ -140,7 +140,7 @@ union ast member regregimm16 ADDI function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) = Some(ADDI(rs, rt, imm)) -function clause execute (ADDI(rs, rt, imm)) = +function clause execute (ADDI(rs, rt, imm)) = { (bit[64]) opA := rGPR(rs); if NotWordVal(opA) then @@ -160,7 +160,7 @@ union ast member regregreg ADDU function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100001) = Some(ADDU(rs, rt, rd)) -function clause execute (ADDU(rs, rt, rd)) = +function clause execute (ADDU(rs, rt, rd)) = { (bit[64]) opA := rGPR(rs); (bit[64]) opB := rGPR(rt); @@ -178,7 +178,7 @@ union ast member regregimm16 ADDIU function clause decode (0b001001 : (regno) rs : (regno) rt : (imm16) imm) = Some(ADDIU(rs, rt, imm)) -function clause execute (ADDIU(rs, rt, imm)) = +function clause execute (ADDIU(rs, rt, imm)) = { (bit[64]) opA := rGPR(rs); if NotWordVal(opA) then @@ -195,7 +195,7 @@ function clause execute (ADDIU(rs, rt, imm)) = union ast member regregreg DSUBU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) = Some(DSUBU(rs, rt, rd)) function clause execute (DSUBU (rs, rt, rd)) = @@ -207,7 +207,7 @@ function clause execute (DSUBU (rs, rt, rd)) = union ast member regregreg DSUB -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) = Some(DSUB(rs, rt, rd)) function clause execute (DSUB (rs, rt, rd)) = @@ -248,7 +248,7 @@ union ast member regregreg SUBU function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100011) = Some(SUBU(rs, rt, rd)) -function clause execute (SUBU(rs, rt, rd)) = +function clause execute (SUBU(rs, rt, rd)) = { (bit[64]) opA := rGPR(rs); (bit[64]) opB := rGPR(rt); @@ -265,7 +265,7 @@ function clause execute (SUBU(rs, rt, rd)) = (* AND reg, reg, reg *) union ast member regregreg AND -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) = Some(AND(rs, rt, rd)) function clause execute (AND (rs, rt, rd)) = @@ -276,7 +276,7 @@ function clause execute (AND (rs, rt, rd)) = (* ANDI reg, reg, imm *) union ast member regregimm16 ANDI -function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) = Some(ANDI(rs, rt, imm)) function clause execute (ANDI (rs, rt, imm)) = { @@ -286,7 +286,7 @@ function clause execute (ANDI (rs, rt, imm)) = (* OR reg, reg, reg *) union ast member regregreg OR -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) = Some(OR(rs, rt, rd)) function clause execute (OR (rs, rt, rd)) = { @@ -296,7 +296,7 @@ function clause execute (OR (rs, rt, rd)) = (* ORI reg, reg, imm *) union ast member regregimm16 ORI -function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) = Some(ORI(rs, rt, imm)) function clause execute (ORI (rs, rt, imm)) = { @@ -306,7 +306,7 @@ function clause execute (ORI (rs, rt, imm)) = (* NOR reg, reg, reg *) union ast member regregreg NOR -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) = Some(NOR(rs, rt, rd)) function clause execute (NOR (rs, rt, rd)) = { @@ -316,7 +316,7 @@ function clause execute (NOR (rs, rt, rd)) = (* XOR reg, reg, reg *) union ast member regregreg XOR -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) = Some(XOR(rs, rt, rd)) function clause execute (XOR (rs, rt, rd)) = { @@ -325,7 +325,7 @@ function clause execute (XOR (rs, rt, rd)) = (* XORI reg, reg, imm *) union ast member regregimm16 XORI -function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) = Some(XORI(rs, rt, imm)) function clause execute (XORI (rs, rt, imm)) = { @@ -333,8 +333,8 @@ function clause execute (XORI (rs, rt, imm)) = } (* LUI reg, imm 32-bit load immediate into upper 16 bits *) -union ast member (regno, imm16) LUI -function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) = +union ast member (regno, imm16) LUI +function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) = Some(LUI(rt, imm)) function clause execute (LUI (rt, imm)) = { @@ -348,18 +348,18 @@ function clause execute (LUI (rt, imm)) = (* DSLL reg, reg, imm5 *) union ast member regregreg DSLL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) = Some(DSLL(rt, rd, sa)) function clause execute (DSLL (rt, rd, sa)) = { - + wGPR(rd) := (rGPR(rt) << sa) (* make tuareg mode less blue >> *) } (* DSLL32 reg, reg, imm5 *) union ast member regregreg DSLL32 -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) = Some(DSLL32(rt, rd, sa)) function clause execute (DSLL32 (rt, rd, sa)) = { @@ -369,12 +369,12 @@ function clause execute (DSLL32 (rt, rd, sa)) = (* DSLLV reg, reg, reg *) union ast member regregreg DSLLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) = Some(DSLLV(rs, rt, rd)) function clause execute (DSLLV (rs, rt, rd)) = { wGPR(rd) := (rGPR(rt) << ((rGPR(rs))[5 .. 0])) (* make tuareg mode less blue >> *) - (* alternative slicing based version of above + (* alternative slicing based version of above sa := (rGPR(rt))[5 .. 0]; v := rGPR(rs); wGPR(rd) := v[(63-sa) .. 0] : (0b0 ^^ sa) *) @@ -383,24 +383,24 @@ function clause execute (DSLLV (rs, rt, rd)) = (* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *) union ast member regregreg DSRA -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) = Some(DSRA(rt, rd, sa)) function clause execute (DSRA (rt, rd, sa)) = { temp := rGPR(rt); - wGPR(rd) := EXTS((temp[63] ^^ sa) : (temp[63 .. sa])) + wGPR(rd) := EXTZ((temp[63] ^^ sa) : (temp[63 .. sa])) } (* DSRA32 reg, reg, imm5 *) union ast member regregreg DSRA32 -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) = Some(DSRA32(rt, rd, sa)) function clause execute (DSRA32 (rt, rd, sa)) = { temp := rGPR(rt); sa32 := (0b1 : sa); (* sa+32 *) - wGPR(rd) := EXTS((temp[63] ^^ sa32) : (temp[63 .. sa32])) + wGPR(rd) := EXTZ((temp[63] ^^ sa32) : (temp[63 .. sa32])) } (* DSRAV reg, reg, reg *) @@ -411,42 +411,42 @@ function clause execute (DSRAV (rs, rt, rd)) = { temp := rGPR(rt); sa := (rGPR(rs)) [5..0]; - wGPR(rd) := EXTS((temp[63] ^^ sa) : temp[63 .. sa]) + wGPR(rd) := EXTZ((temp[63] ^^ sa) : temp[63 .. sa]) } (* DSRL shift right logical - reg, reg, imm5 *) union ast member regregreg DSRL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) = Some(DSRL(rt, rd, sa)) function clause execute (DSRL (rt, rd, sa)) = { temp := rGPR(rt); - wGPR(rd) := EXTS((bitzero ^^ sa) : (temp[63 .. sa])) + wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp[63 .. sa])) } (* DSRL32 reg, reg, imm5 *) union ast member regregreg DSRL32 -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) = Some(DSRL32(rt, rd, sa)) function clause execute (DSRL32 (rt, rd, sa)) = { temp := rGPR(rt); sa32 := (0b1 : sa); (* sa+32 *) - wGPR(rd) := EXTS((bitzero ^^ sa32) : (temp[63 .. sa32])) + wGPR(rd) := EXTZ((bitzero ^^ sa32) : (temp[63 .. sa32])) } (* DSRLV reg, reg, reg *) union ast member regregreg DSRLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) = Some(DSRLV(rs, rt, rd)) function clause execute (DSRLV (rs, rt, rd)) = { temp := rGPR(rt); sa := (rGPR(rs)) [5..0]; - wGPR(rd) := EXTS((bitzero ^^ sa) : temp[63 .. sa]) + wGPR(rd) := EXTZ((bitzero ^^ sa) : temp[63 .. sa]) } (**************************************************************************************) @@ -456,28 +456,28 @@ function clause execute (DSRLV (rs, rt, rd)) = (* SLL 32-bit shift left *) union ast member regregreg SLL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) = Some(SLL(rt, rd, sa)) function clause execute (SLL(rt, rd, sa)) = { - wGPR(rd) := EXTS((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) + wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) } (* SLLV 32-bit shift left variable *) union ast member regregreg SLLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) = Some(SLLV(rs, rt, rd)) function clause execute (SLLV(rs, rt, rd)) = { sa := (rGPR(rs))[4..0]; - wGPR(rd) := EXTS((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) + wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa)) } (* SRA 32-bit arithmetic shift right *) union ast member regregreg SRA -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) = Some(SRA(rt, rd, sa)) function clause execute (SRA(rt, rd, sa)) = { @@ -485,13 +485,13 @@ function clause execute (SRA(rt, rd, sa)) = if (NotWordVal(temp)) then wGPR(rd) := undefined else - wGPR(rd) := EXTS((temp[31] ^^ (sa+32)) : temp [31..sa]) + wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa]) } (* SRAV 32-bit arithmetic shift right variable *) union ast member regregreg SRAV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) = Some(SRAV(rs, rt, rd)) function clause execute (SRAV(rs, rt, rd)) = { @@ -500,13 +500,13 @@ function clause execute (SRAV(rs, rt, rd)) = if (NotWordVal(temp)) then wGPR(rd) := undefined else - wGPR(rd) := EXTS((temp[31] ^^ (sa+32)) : temp [31..sa]) + wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa]) } (* SRL 32-bit shift right *) union ast member regregreg SRL -function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) = +function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) = Some(SRL(rt, rd, sa)) function clause execute (SRL(rt, rd, sa)) = { @@ -514,13 +514,13 @@ function clause execute (SRL(rt, rd, sa)) = if (NotWordVal(temp)) then wGPR(rd) := undefined else - wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa])) + wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa])) } (* SRLV 32-bit shift right variable *) union ast member regregreg SRLV -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) = Some(SRLV(rs, rt, rd)) function clause execute (SRLV(rs, rt, rd)) = { @@ -529,7 +529,7 @@ function clause execute (SRLV(rs, rt, rd)) = if (NotWordVal(temp)) then wGPR(rd) := undefined else - wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa])) + wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa])) } (**************************************************************************************) @@ -539,7 +539,7 @@ function clause execute (SRLV(rs, rt, rd)) = (* SLT set if less than (signed) *) union ast member regregreg SLT -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) = Some(SLT(rs, rt, rd)) function clause execute (SLT(rs, rt, rd)) = { @@ -549,7 +549,7 @@ function clause execute (SLT(rs, rt, rd)) = (* SLT set if less than immediate (signed) *) union ast member regregimm16 SLTI -function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) = Some(SLTI(rs, rt, imm)) function clause execute (SLTI(rs, rt, imm)) = { @@ -561,7 +561,7 @@ function clause execute (SLTI(rs, rt, imm)) = (* SLTU set if less than unsigned *) union ast member regregreg SLTU -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) = Some(SLTU(rs, rt, rd)) function clause execute (SLTU(rs, rt, rd)) = { @@ -573,7 +573,7 @@ function clause execute (SLTU(rs, rt, rd)) = (* SLTIU set if less than immediate unsigned *) union ast member regregimm16 SLTIU -function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) = Some(SLTIU(rs, rt, imm)) function clause execute (SLTIU(rs, rt, imm)) = { @@ -585,22 +585,22 @@ function clause execute (SLTIU(rs, rt, imm)) = (* MOVN move if non-zero *) union ast member regregreg MOVN -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) = Some(MOVN(rs, rt, rd)) function clause execute (MOVN(rs, rt, rd)) = { - if (rGPR(rt) != 0x0000000000000000) then + if (rGPR(rt) != 0x0000000000000000) then wGPR(rd) := rGPR(rs) } (* MOVZ move if zero *) union ast member regregreg MOVZ -function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) = Some(MOVZ(rs, rt, rd)) function clause execute (MOVZ(rs, rt, rd)) = { - if (rGPR(rt) == 0x0000000000000000) then + if (rGPR(rt) == 0x0000000000000000) then wGPR(rd) := rGPR(rs) } @@ -610,7 +610,7 @@ function clause execute (MOVZ(rs, rt, rd)) = (* MFHI move from HI register *) union ast member regno MFHI -function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) = +function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) = Some(MFHI(rd)) function clause execute (MFHI(rd)) = { @@ -619,7 +619,7 @@ function clause execute (MFHI(rd)) = (* MFLO move from LO register *) union ast member regno MFLO -function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) = +function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) = Some(MFLO(rd)) function clause execute (MFLO(rd)) = { @@ -628,7 +628,7 @@ function clause execute (MFLO(rd)) = (* MTHI move to HI register *) union ast member regno MTHI -function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) = +function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) = Some(MTHI(rs)) function clause execute (MTHI(rs)) = { @@ -637,7 +637,7 @@ function clause execute (MTHI(rs)) = (* MTLO move to LO register *) union ast member regno MTLO -function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) = +function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) = Some(MTLO(rs)) function clause execute (MTLO(rs)) = { @@ -657,7 +657,7 @@ function clause execute (MUL(rs, rt, rd)) = undefined else EXTS(result[31..0]); - (* HI and LO are technically undefined after MUL, but this causes problems with tests and + (* HI and LO are technically undefined after MUL, but this causes problems with tests and (potentially) context switch so just leave them alone HI := undefined; LO := undefined; @@ -691,7 +691,7 @@ function clause execute (MULTU(rs, rt)) = (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else - (rsVal[31..0]) * (rtVal[31..0]); + EXTS((rsVal[31..0]) * (rtVal[31..0])); HI := EXTS(result[63..32]); LO := EXTS(result[31..0]); } @@ -796,13 +796,13 @@ function clause execute (DIV(rs, rt)) = rtVal := rGPR(rt); let ((bit[32]) q, (bit[32])r) = ( if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0)) then - (undefined, undefined) + ((bit[32]) undefined, (bit[32]) undefined) else let si = (signed((rsVal[31..0]))) in let ti = (signed((rtVal[31..0]))) in let qi = (si quot ti) in let ri = (si - (ti*qi)) in - ((bit[32]) qi, (bit[32]) ri)) + ((bit[32]) (to_svec(qi)), (bit[32]) (to_svec(ri)))) in { HI := EXTS(r); @@ -820,13 +820,13 @@ function clause execute (DIVU(rs, rt)) = rtVal := rGPR(rt); let ((bit[32]) q, (bit[32])r) = ( if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0) then - (undefined, undefined) + ((bit[32]) undefined, (bit[32]) undefined) else let si = unsigned(rsVal[31..0]) in let ti = unsigned(rtVal[31..0]) in let qi = (si quot ti) in let ri = (si mod ti) in - ((bit[32]) qi, (bit[32]) ri)) + ((bit[32]) (to_svec(qi)), (bit[32]) (to_svec(ri)))) in { HI := EXTS(r); @@ -843,11 +843,11 @@ function clause execute (DDIV(rs, rt)) = rsVal := signed(rGPR(rs)); rtVal := signed(rGPR(rt)); let ((bit[64])q, (bit[64])r) = (if (rtVal == 0) - then (undefined, undefined) - else + then ((bit[64]) undefined, (bit[64]) undefined) + else let qi = (rsVal quot rtVal) in let ri = (rsVal - (qi * rtVal)) in - ((bit[64]) qi, (bit[64]) ri)) in + ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in { LO := q; HI := r; @@ -863,10 +863,10 @@ function clause execute (DDIVU(rs, rt)) = (int) rsVal := rGPR(rs); (int) rtVal := rGPR(rt); let ((bit[64])q, (bit[64])r) = (if (rtVal == 0) - then (undefined, undefined) + then ((bit[64]) undefined, (bit[64]) undefined) else let qi = (rsVal quot rtVal) in let ri = (rsVal mod rtVal) in - ((bit[64]) qi, (bit[64]) ri)) in + ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in { LO := q; HI := r; @@ -881,7 +881,7 @@ function clause execute (DDIVU(rs, rt)) = union ast member (bit[26]) J function clause decode (0b000010 : (bit[26]) offset) = Some(J(offset)) -function clause execute (J(offset)) = +function clause execute (J(offset)) = { delayedPC := (PC + 4)[63..28] : offset : 0b00; branchPending := 1 @@ -891,11 +891,11 @@ function clause execute (J(offset)) = union ast member (bit[26]) JAL function clause decode (0b000011 : (bit[26]) offset) = Some(JAL(offset)) -function clause execute (JAL(offset)) = +function clause execute (JAL(offset)) = { delayedPC := (PC + 4)[63..28] : offset : 0b00; branchPending := 1; - wGPR(31) := PC + 8; + wGPR(0b11111) := PC + 8; } (* JR -- jump via register *) @@ -925,13 +925,13 @@ function clause execute (JALR(rs, rd)) = (**************************************************************************************) union ast member (regno, regno, imm16, bool, bool) BEQ -function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) = Some(BEQ(rs, rt, imm, false, false)) (* BEQ *) -function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) = Some(BEQ(rs, rt, imm, false, true)) (* BEQL *) -function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) = Some(BEQ(rs, rt, imm, true , false)) (* BNE *) -function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) = +function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) = Some(BEQ(rs, rt, imm, true , true)) (* BNEL *) function clause execute (BEQ(rs, rd, imm, ne, likely)) = { @@ -948,8 +948,8 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) = } } -(* - +(* + Branches comparing with zero (single register operand, possible link in r31) *) @@ -959,32 +959,32 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) = (**************************************************************************************) union ast member (regno, imm16, Comparison, bool, bool) BCMPZ -function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) = Some(BCMPZ(rs, imm, LT, false, false)) (* BLTZ *) -function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) = Some(BCMPZ(rs, imm, LT, true, false)) (* BLTZAL *) -function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) = Some(BCMPZ(rs, imm, LT, false, true)) (* BLTZL *) -function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) = Some(BCMPZ(rs, imm, LT, true, true)) (* BLTZALL *) -function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) = Some(BCMPZ(rs, imm, GE, false, false)) (* BGEZ *) -function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) = Some(BCMPZ(rs, imm, GE, true, false)) (* BGEZAL *) -function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) = Some(BCMPZ(rs, imm, GE, false, true)) (* BGEZL *) -function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) = Some(BCMPZ(rs, imm, GE, true, true)) (* BGEZALL *) -function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) = +function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) = Some(BCMPZ(rs, imm, GT, false, false)) (* BGTZ *) -function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) = +function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) = Some(BCMPZ(rs, imm, GT, false, true)) (* BGTZL *) -function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) = +function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) = Some(BCMPZ(rs, imm, LE, false, false)) (* BLEZ *) -function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) = +function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) = Some(BCMPZ(rs, imm, LE, false, true)) (* BLEZL *) function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = @@ -1003,7 +1003,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = nextPC := PC + 8 (* skip branch delay *) }; if (link) then - wGPR(31) := linkVal + wGPR(0b11111) := linkVal } (**************************************************************************************) @@ -1051,17 +1051,17 @@ function clause execute (WAIT) = { (* Trap instructions with two register operands *) union ast member (regno, regno, Comparison) TRAPREG -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) = Some(TRAPREG(rs, rt, GE)) (* TGE *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) = Some(TRAPREG(rs, rt, GEU)) (* TGEU *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) = Some(TRAPREG(rs, rt, LT)) (* TLT *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) = Some(TRAPREG(rs, rt, LTU)) (* TLTU *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) = Some(TRAPREG(rs, rt, EQ)) (* TEQ *) -function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = +function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = Some(TRAPREG(rs, rt, NE)) (* TNE *) function clause execute (TRAPREG(rs, rt, cmp)) = { @@ -1075,22 +1075,22 @@ function clause execute (TRAPREG(rs, rt, cmp)) = (* Trap instructions with one register and one immediate operand *) union ast member (regno, imm16, Comparison) TRAPIMM -function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) = Some(TRAPIMM(rs, imm, EQ)) (* TEQI *) -function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = Some(TRAPIMM(rs, imm, NE)) (* TNEI *) -function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = Some(TRAPIMM(rs, imm, GE)) (* TGEI *) -function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *) -function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = Some(TRAPIMM(rs, imm, LT)) (* TLTI *) -function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = +function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = Some(TRAPIMM(rs, imm, LTU)) (* TLTIU *) function clause execute (TRAPIMM(rs, imm, cmp)) = { rs_val := rGPR(rs); - imm_val := EXTS(imm); + (bit[64]) imm_val := EXTS(imm); condition := compare(cmp, rs_val, imm_val); if (condition) then (SignalException(Tr)) @@ -1101,23 +1101,23 @@ function clause execute (TRAPIMM(rs, imm, cmp)) = (**************************************************************************************) union ast member (WordType, bool, bool, regno, regno, imm16) Load -function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(B, true, false, base, rt, offset)) (* LB *) -function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(B, false, false, base, rt, offset)) (* LBU *) -function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(H, true, false, base, rt, offset)) (* LH *) -function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(H, false, false, base, rt, offset)) (* LHU *) -function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(W, true, false, base, rt, offset)) (* LW *) -function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(W, false, false, base, rt, offset)) (* LWU *) -function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(D, false, false, base, rt, offset)) (* LD *) -function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(W, true, true, base, rt, offset)) (* LL *) -function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) = Some(Load(D, false, true, base, rt, offset)) (* LLD *) function clause execute (Load(width, signed, linked, base, rt, offset)) = { @@ -1127,15 +1127,25 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = else let pAddr = (TLBTranslate(vAddr, LoadData)) in { - memResult := if (linked) then + (bit[64]) memResult := if (linked) then { CP0LLBit := 0b1; - CP0LLAddr := pAddr; - MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)); + CP0LLAddr := pAddr; + switch wordWidthBytes(width) { + case ([:1:]) w -> MEMr_reserve_wrapper(pAddr, w) + case ([:2:]) w -> MEMr_reserve_wrapper(pAddr, w) + case ([:4:]) w -> MEMr_reserve_wrapper(pAddr, w) + case ([:8:]) w -> MEMr_reserve_wrapper(pAddr, w) + } } else - MEMr_wrapper(pAddr, wordWidthBytes(width)); - if (signed) then + switch wordWidthBytes(width) { + case ([:1:]) w -> MEMr_reserve_wrapper(pAddr, w) + case ([:2:]) w -> MEMr_reserve_wrapper(pAddr, w) + case ([:4:]) w -> MEMr_reserve_wrapper(pAddr, w) + case ([:8:]) w -> MEMr_reserve_wrapper(pAddr, w) + }; + if (signed) then wGPR(rt) := EXTS(memResult) else wGPR(rt) := EXTZ(memResult) @@ -1147,17 +1157,17 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = (**************************************************************************************) union ast member (WordType, bool, regno, regno, imm16) Store -function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(B, false, base, rt, offset)) (* SB *) -function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(H, false, base, rt, offset)) (* SH *) -function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(W, false, base, rt, offset)) (* SW *) -function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(D, false, base, rt, offset)) (* SD *) -function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(W, true, base, rt, offset)) (* SC *) -function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) = +function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(D, true, base, rt, offset)) (* SCD *) function clause execute (Store(width, conditional, base, rt, offset)) = { @@ -1170,14 +1180,14 @@ function clause execute (Store(width, conditional, base, rt, offset)) = { if (conditional) then { - success := if (CP0LLBit[0]) then switch(width) + success := if (CP0LLBit[0]) then (bool) switch(width) { case B -> MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0]) case H -> MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0]) case W -> MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]) case D -> MEMw_conditional_wrapper(pAddr, 8, rt_val) } else false; - wGPR(rt) := EXTZ([success]) + wGPR(rt) := EXTZ([bool_to_bit(success)]) } else switch(width) @@ -1195,7 +1205,7 @@ function clause execute (Store(width, conditional, base, rt, offset)) = union ast member regregimm16 LWL function clause decode(0b100010 : (regno) base : (regno) rt : (imm16) offset) = Some(LWL(base, rt, offset)) -function clause execute(LWL(base, rt, offset)) = +function clause execute(LWL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); @@ -1203,19 +1213,19 @@ function clause execute(LWL(base, rt, offset)) = { mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) reg_val := rGPR(rt); - wGPR(rt) := EXTS(switch(vAddr[1..0]) + wGPR(rt) := EXTS((bit[32]) switch(vAddr[1..0]) { case 0b00 -> mem_val case 0b01 -> mem_val[23..0] : reg_val[07..0] case 0b10 -> mem_val[15..0] : reg_val[15..0] case 0b11 -> mem_val[07..0] : reg_val[23..0] - }); + }); } } union ast member regregimm16 LWR function clause decode(0b100110 : (regno) base : (regno) rt : (imm16) offset) = Some(LWR(base, rt, offset)) -function clause execute(LWR(base, rt, offset)) = +function clause execute(LWR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); @@ -1223,7 +1233,7 @@ function clause execute(LWR(base, rt, offset)) = { mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) reg_val := rGPR(rt); - wGPR(rt) := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *) + wGPR(rt) := EXTS((bit[32]) switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *) { case 0b00 -> reg_val[31..8] : mem_val[31..24] case 0b01 -> reg_val[31..16] : mem_val[31..16] @@ -1237,7 +1247,7 @@ function clause execute(LWR(base, rt, offset)) = union ast member regregimm16 SWL function clause decode(0b101010 : (regno) base : (regno) rt : (imm16) offset) = Some(SWL(base, rt, offset)) -function clause execute(SWL(base, rt, offset)) = +function clause execute(SWL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); @@ -1257,7 +1267,7 @@ function clause execute(SWL(base, rt, offset)) = union ast member regregimm16 SWR function clause decode(0b101110 : (regno) base : (regno) rt : (imm16) offset) = Some(SWR(base, rt, offset)) -function clause execute(SWR(base, rt, offset)) = +function clause execute(SWR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); @@ -1279,7 +1289,7 @@ function clause execute(SWR(base, rt, offset)) = union ast member regregimm16 LDL function clause decode(0b011010 : (regno) base : (regno) rt : (imm16) offset) = Some(LDL(base, rt, offset)) -function clause execute(LDL(base, rt, offset)) = +function clause execute(LDL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); @@ -1305,7 +1315,7 @@ function clause execute(LDL(base, rt, offset)) = union ast member regregimm16 LDR function clause decode(0b011011 : (regno) base : (regno) rt : (imm16) offset) = Some(LDR(base, rt, offset)) -function clause execute(LDR(base, rt, offset)) = +function clause execute(LDR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); @@ -1331,7 +1341,7 @@ function clause execute(LDR(base, rt, offset)) = union ast member regregimm16 SDL function clause decode(0b101100 : (regno) base : (regno) rt : (imm16) offset) = Some(SDL(base, rt, offset)) -function clause execute(SDL(base, rt, offset)) = +function clause execute(SDL(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); @@ -1357,7 +1367,7 @@ function clause execute(SDL(base, rt, offset)) = union ast member regregimm16 SDR function clause decode(0b101101 : (regno) base : (regno) rt : (imm16) offset) = Some(SDR(base, rt, offset)) -function clause execute(SDR(base, rt, offset)) = +function clause execute(SDR(base, rt, offset)) = { (* XXX length check not quite right, but conservative *) (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); @@ -1384,7 +1394,7 @@ function clause execute(SDR(base, rt, offset)) = union ast member regregimm16 CACHE function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) = Some(CACHE(base, op, imm)) -function clause execute (CACHE(base, op, imm)) = +function clause execute (CACHE(base, op, imm)) = checkCP0Access () (* pretty much a NOP because no caches *) (* PREF - prefetching into (non-existent) caches *) @@ -1398,7 +1408,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) = +function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = Some((ast) SYNC) (* stype is currently ignored *) function clause execute(SYNC) = MEM_sync() @@ -1413,7 +1423,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = { let (bit[64]) result = switch (rd, sel) { case (0b00000,0b000) -> let (bit[31]) idx = EXTZ(TLBIndex) in - (0x00000000 : [TLBProbe] : idx) (* 0, TLB Index *) + (0x00000000 : TLBProbe : idx) (* 0, TLB Index *) case (0b00001,0b000) -> EXTZ(TLBRandom) (* 1, TLB Random *) case (0b00010,0b000) -> TLBEntryLo0 (* 2, TLB EntryLo0 *) case (0b00011,0b000) -> TLBEntryLo1 (* 3, TLB EntryLo1 *) @@ -1433,9 +1443,9 @@ function clause execute (MFC0(rt, rd, sel, double)) = { case (0b01111,0b110) -> 0 (* 15, sel 6: CHERI core ID *) case (0b01111,0b111) -> 0 (* 15, sel 7: CHERI thread ID *) case (0b10000,0b000) -> EXTZ(0b1 (* M *) (* 16, sel 0: Config0 *) - : 0b000000000000000 (* Impl *) - : 0b1 (* BE *) - : 0b10 (* AT *) + : 0b000000000000000 (* Impl *) + : 0b1 (* BE *) + : 0b10 (* AT *) : 0b000 (* AR *) : 0b001 (* MT standard TLB *) : 0b0000 (* zero *) @@ -1449,7 +1459,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = { : 0b000 (* DS dcache sets *) : 0b000 (* DL dcache lines *) : 0b000 (* DA dcache assoc. *) - : [have_cp2] (* C2 CP2 presence *) + : [bool_to_bit(have_cp2)] (* C2 CP2 presence *) : 0b0 (* MD MDMX implemented *) : 0b0 (* PC performance counters *) : 0b0 (* WR watch registers *) @@ -1476,7 +1486,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = { case _ -> (SignalException(ResI)) } in wGPR(rt) := if (double) then result else EXTS(result[31..0]) -} +} (* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *) union ast member unit HCF @@ -1519,7 +1529,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = { (TLBEntryHi.ASID) := (reg_val[7..0]); } case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *) - CP0Compare := reg_val[31..0]; + CP0Compare := reg_val[31..0]; (CP0Cause[15]) := bitzero; } case (0b01100,0b000) -> { (* 12 Status *) @@ -1546,7 +1556,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = { case _ -> (SignalException(ResI)) } } -(* + function unit TLBWriteEntry((TLBIndexT) idx) = { pagemask := (bit[16]) (EXTZ(TLBPageMask)); (* XXX EXTZ here forces register read in ocaml shallow embedding *) switch(pagemask) { @@ -1561,26 +1571,28 @@ function unit TLBWriteEntry((TLBIndexT) idx) = { case 0xffff -> () case _ -> (SignalException(MCheck)) }; - ((TLBEntries[idx]).pagemask) := pagemask; - ((TLBEntries[idx]).r ) := TLBEntryHi.R; - ((TLBEntries[idx]).vpn2 ) := TLBEntryHi.VPN2; - ((TLBEntries[idx]).asid ) := TLBEntryHi.ASID; - ((TLBEntries[idx]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G)); - ((TLBEntries[idx]).valid ) := bitone; - ((TLBEntries[idx]).caps0 ) := TLBEntryLo0.CapS; - ((TLBEntries[idx]).capl0 ) := TLBEntryLo0.CapL; - ((TLBEntries[idx]).pfn0 ) := TLBEntryLo0.PFN; - ((TLBEntries[idx]).c0 ) := TLBEntryLo0.C; - ((TLBEntries[idx]).d0 ) := TLBEntryLo0.D; - ((TLBEntries[idx]).v0 ) := TLBEntryLo0.V; - ((TLBEntries[idx]).caps1 ) := TLBEntryLo1.CapS; - ((TLBEntries[idx]).capl1 ) := TLBEntryLo1.CapL; - ((TLBEntries[idx]).pfn1 ) := TLBEntryLo1.PFN; - ((TLBEntries[idx]).c1 ) := TLBEntryLo1.C; - ((TLBEntries[idx]).d1 ) := TLBEntryLo1.D; - ((TLBEntries[idx]).v1 ) := TLBEntryLo1.V; + let idxr = unsigned(idx) in { + ((TLBEntries[idxr]).pagemask) := pagemask; + ((TLBEntries[idxr]).r ) := TLBEntryHi.R; + ((TLBEntries[idxr]).vpn2 ) := TLBEntryHi.VPN2; + ((TLBEntries[idxr]).asid ) := TLBEntryHi.ASID; + ((TLBEntries[idxr]).g ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G)); + ((TLBEntries[idxr]).valid ) := bitone; + ((TLBEntries[idxr]).caps0 ) := TLBEntryLo0.CapS; + ((TLBEntries[idxr]).capl0 ) := TLBEntryLo0.CapL; + ((TLBEntries[idxr]).pfn0 ) := TLBEntryLo0.PFN; + ((TLBEntries[idxr]).c0 ) := TLBEntryLo0.C; + ((TLBEntries[idxr]).d0 ) := TLBEntryLo0.D; + ((TLBEntries[idxr]).v0 ) := TLBEntryLo0.V; + ((TLBEntries[idxr]).caps1 ) := TLBEntryLo1.CapS; + ((TLBEntries[idxr]).capl1 ) := TLBEntryLo1.CapL; + ((TLBEntries[idxr]).pfn1 ) := TLBEntryLo1.PFN; + ((TLBEntries[idxr]).c1 ) := TLBEntryLo1.C; + ((TLBEntries[idxr]).d1 ) := TLBEntryLo1.D; + ((TLBEntries[idxr]).v1 ) := TLBEntryLo1.V; + } } -*) + union ast member TLBWI function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some((ast) TLBWI) function clause execute (TLBWI) = { @@ -1599,7 +1611,7 @@ union ast member TLBR function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some((ast) TLBR) function clause execute (TLBR) = { checkCP0Access(); - let entry = TLBEntries[TLBIndex] in { + let entry = TLBEntries[unsigned(TLBIndex)] in { TLBPageMask := entry.pagemask; TLBEntryHi.R := entry.r; TLBEntryHi.VPN2 := entry.vpn2; @@ -1633,17 +1645,17 @@ function clause execute ((TLBP)) = { } case None -> { TLBProbe := [bitone]; - TLBIndex := 0; + TLBIndex := 0b000000; } } } union ast member (regno, regno) RDHWR -function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = +function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = Some(RDHWR(rt, rd)) function clause execute (RDHWR(rt, rd)) = { let accessLevel = getAccessLevel() in - if ((accessLevel != Kernel) & (~((CP0Status.CU)[0])) & ~(CP0HWREna[rd])) then + if ((accessLevel != Kernel) & (~((CP0Status.CU)[28])) & ~(CP0HWREna[rd])) then (SignalException(ResI)); let (bit[64]) temp = switch (rd) { case 0b00000 -> EXTZ([bitzero]) (* CPUNum *) diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail index cdb4316c..5b36983d 100644 --- a/mips_new_tc/mips_wrappers.sail +++ b/mips_new_tc/mips_wrappers.sail @@ -35,8 +35,10 @@ (* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility (mostly identity functions here) *) -function unit effect {wmem} MEMw_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) data) = - let ledata = reverse_endianness'(8, data) in +val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper + +function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) = + let ledata = reverse_endianness'(sizeof 'n, data) in if (addr == 0x000000007f000000) then { UART_WDATA := ledata[7..0]; @@ -46,10 +48,12 @@ function unit effect {wmem} MEMw_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) MEMval(addr, size, ledata); } -function bool effect {wmem} MEMw_conditional_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) data) = +val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {eamem, wmv} MEMw_conditional_wrapper + +function bool MEMw_conditional_wrapper(addr, size, data) = { MEMea_conditional(addr, size); - MEMval_conditional(addr, size, reverse_endianness'(8, data)) + MEMval_conditional(addr, size, reverse_endianness'(sizeof 'n, data)) } function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = diff --git a/src/ast_util.ml b/src/ast_util.ml index d41ef180..22746ed1 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -294,6 +294,7 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id + | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")" | _ -> "LEXP" and string_of_letbind (LB_aux (lb, l)) = match lb with diff --git a/src/type_check_new.ml b/src/type_check_new.ml index 5be2cd43..b696e6d2 100644 --- a/src/type_check_new.ml +++ b/src/type_check_new.ml @@ -723,13 +723,13 @@ end = struct then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists") else begin - typ_debug ("Adding type synonym " ^ string_of_id id); + typ_print ("Adding type synonym " ^ string_of_id id); { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms } end let get_typ_synonym id env = Bindings.find id env.typ_synonyms - let rec expand_synonyms env (Typ_aux (typ, l)) = + let rec expand_synonyms env (Typ_aux (typ, l) as t) = match typ with | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l) | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l) @@ -1773,13 +1773,35 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit")), no_effect))) in let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in + let has_typ v env = + match Env.lookup_id v env with + | Local (Mutable, _) | Register _ -> true + | _ -> false + in match lexp_aux with - | LEXP_field (LEXP_aux (LEXP_id v, _), field) -> + | LEXP_field (LEXP_aux (flexp, _), field) -> begin - let regtyp = match Env.lookup_id v env with - | Register typ -> typ - | _ -> typ_error l "l-expression field is not a register" + let infer_flexp = function + | LEXP_id v -> + begin match Env.lookup_id v env with + | Register typ -> typ, LEXP_id v + | _ -> typ_error l "l-expression field is not a register" + end + | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) -> + begin + (* Check: is this ok if the vector is immutable? *) + let is_immutable, vtyp = match Env.lookup_id v env with + | Unbound -> typ_error l "Cannot assign to element of unbound vector" + | Enum _ -> typ_error l "Cannot vector assign to enumeration element" + | Local (Immutable, vtyp) -> true, vtyp + | Local (Mutable, vtyp) | Register vtyp -> false, vtyp + in + let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in + let E_aux (E_app (_, [_; inferred_exp]), _) = access in + typ_of access, LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp) + end in + let regtyp, inferred_flexp = infer_flexp flexp in match Env.expand_synonyms env regtyp with | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env -> let base, top, ranges = Env.get_regtyp regtyp_id env in @@ -1795,7 +1817,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as | _, _ -> typ_error l "Not implemented this register field type yet..." in let checked_exp = crule check_exp env exp vec_typ in - annot_assign (annot_lexp (LEXP_field (annot_lexp_effect (LEXP_id v) regtyp (mk_effect [BE_wreg]), field)) vec_typ) checked_exp, env + annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp 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) -> @@ -1804,6 +1826,14 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let checked_exp = crule check_exp env exp typ_annot in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in annot_assign tlexp checked_exp, env' + | LEXP_id v when has_typ v env -> + begin match Env.lookup_id v env with + | Local (Mutable, vtyp) | Register vtyp -> + let checked_exp = crule check_exp env exp vtyp in + let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in + annot_assign tlexp checked_exp, env' + | _ -> assert false + end | _ -> let inferred_exp = irule infer_exp env exp in let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in @@ -1814,13 +1844,12 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in match lexp_aux with | LEXP_id v -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env - | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env - | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env + begin match Env.lookup_id v env with + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env + | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env + | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env end | LEXP_cast (typ_annot, v) -> begin @@ -2423,11 +2452,16 @@ let check_register env id base top ranges = | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) -> let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in (* FIXME: wrong for default Order inc? *) - let cast_typ = mk_typ (Typ_fn (mk_id_typ id, dvector_typ env base (nconstant ((basec - topc) + 1)) bit_typ, no_effect)) in + let vec_typ = dvector_typ env base (nconstant ((basec - topc) + 1)) bit_typ in + let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in + let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in env |> Env.add_regtyp id basec topc ranges + (* |> Env.add_typ_synonym id (fun _ -> vec_typ) *) |> Env.add_val_spec (mk_id ("cast_" ^ string_of_id id)) (no_typq, cast_typ) |> Env.add_cast (mk_id ("cast_" ^ string_of_id id)) + |> Env.add_val_spec (mk_id ("cast_to_" ^ string_of_id id)) (no_typq, cast_to_typ) + |> Env.add_cast (mk_id ("cast_to_" ^ string_of_id id)) | _, _ -> typ_error (id_loc id) "Num expressions in register type declaration do not evaluate to constants" let kinded_id_arg kind_id = diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index 5172142d..6ce2d5c8 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -15,9 +15,12 @@ mkdir -p $DIR/rtfail rm -f $DIR/tests.xml -cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail > $DIR/pass/mips_prelude.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail $SAILDIR/mips_new_tc/mips_tlb.sail > $DIR/pass/mips_tlb.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail $SAILDIR/mips_new_tc/mips_tlb.sail $SAILDIR/mips_new_tc/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail +MIPS="$SAILDIR/mips_new_tc" + +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail pass=0 fail=0 -- cgit v1.2.3