From 6e42757415ececd16355f14a7f7d3f751037364c Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Wed, 17 Jan 2024 15:08:13 +0100 Subject: [PATCH] [litmus] Basic type checking for RISCV Reject programs that use a register as an address and a scalar of size <= sizeof(int32_t). --- lib/CType.ml | 2 ++ lib/CType.mli | 2 ++ litmus/RISCVArch_litmus.ml | 26 +++++++++++++++++-- litmus/RISCVCompile_litmus.ml | 49 +++++++++++++++++++++++++---------- 4 files changed, 63 insertions(+), 16 deletions(-) diff --git a/lib/CType.ml b/lib/CType.ml index 6f57fe8fb..108f23b9c 100644 --- a/lib/CType.ml +++ b/lib/CType.ml @@ -29,6 +29,8 @@ type t = let void = Base "void" let voidstar = Pointer void +let byte = Base "int8_t" +let half = Base "int16_t" let word = Base "int" let quad = Base "int64_t" let int32x4_t = Base "int32x4_t" diff --git a/lib/CType.mli b/lib/CType.mli index c34200ce1..1b424aad7 100644 --- a/lib/CType.mli +++ b/lib/CType.mli @@ -29,6 +29,8 @@ type t = val void : t val voidstar : t +val byte : t +val half : t val word : t val quad : t val int32x4_t : t diff --git a/litmus/RISCVArch_litmus.ml b/litmus/RISCVArch_litmus.ml index ba360f8b4..789105f9d 100644 --- a/litmus/RISCVArch_litmus.ml +++ b/litmus/RISCVArch_litmus.ml @@ -42,8 +42,30 @@ module Make(O:Arch_litmus.Config)(V:Constant.S) = struct let reg_class _ = "=&r" let reg_class_stable _ = "=&r" let comment = comment - let error _t1 _t2 = false - and warn _t1 _t2 = false + + let error t1 t2 = + let open CType in +(* Printf.eprintf "Error %s and %s\n" (debug t1) (debug t2) ; *) + match t1,t2 with + | (Base + ("int"|"ins_t"|"int16_t"|"uint16_t"|"int8_t"|"uint8_t"), + Pointer _) + | (Pointer _, + Base ("int"|"ins_t"|"int16_t"|"uint16_t"|"int8_t"|"uint8_t")) -> + true + + | _ -> false + + let warn t1 t2 = + let open CType in + match t1,t2 with + | Base ("ins_t"|"int"|"int32_t"|"uint32_t" + |"int16_t"|"uint16_t" + |"int8_t"|"uint8_t"), + Base ("ins_t"|"int"|"int32_t"|"uint32_t") -> false + | (Base "int",_)|(_,Base "int") -> true + | _ -> false + end) let features = [] let nop = INop diff --git a/litmus/RISCVCompile_litmus.ml b/litmus/RISCVCompile_litmus.ml index 17b9067dc..b446a2c4e 100644 --- a/litmus/RISCVCompile_litmus.ml +++ b/litmus/RISCVCompile_litmus.ml @@ -44,15 +44,25 @@ module Make(V:Constant.S)(C:Arch_litmus.Config) = let tr_2regs fmt1 fmt2 r1 r2 = match r1 with | A.Ireg X0 -> let fmt2,r2 = tr_reg fmt1 r2 in - "x0",fmt2,r2 + "x0",fmt2,[],r2 | r -> let fmt2,r2 = tr_reg fmt2 r2 in - fmt1,fmt2,r::r2 + fmt1,fmt2,[r],r2 let tr_1i = tr_reg "^i0" let tr_1o = tr_reg "^o0" let tr_2i = tr_2regs "^i0" "^i1" + open CType + + let w2type = function + | A.Byte -> byte + | A.Half -> half + | A.Word -> word + | A.Double -> quad + + let add_type t = List.map (fun x -> x,t) + let op2regsI memo r1 r2 k = let fmt1,r1 = tr_1o r1 and fmt2,r2 = tr_1i r2 in @@ -74,10 +84,10 @@ module Make(V:Constant.S)(C:Arch_litmus.Config) = let op3regs memo r1 r2 r3 = let fmt1,r1 = tr_1o r1 - and fmt2,fmt3,r2r3 = tr_2i r2 r3 in + and fmt2,fmt3,r2,r3 = tr_2i r2 r3 in { empty_ins with memo = sprintf "%s %s,%s,%s" memo fmt1 fmt2 fmt3; - inputs=r2r3; outputs=r1; } + inputs=r2@r3; outputs=r1; } let ext memo r1 r2 = let fmt1,r1 = tr_1o r1 @@ -90,6 +100,7 @@ module Make(V:Constant.S)(C:Arch_litmus.Config) = include Handler.No(struct type ins = A.Out.ins end) + let compile_ins tr_lab ins k = match ins with | A.INop -> { empty_ins with memo="nop"; }::k | A.Ret -> { empty_ins with memo="ret"; }::k @@ -112,41 +123,51 @@ module Make(V:Constant.S)(C:Arch_litmus.Config) = memo = sprintf "j %s" (A.Out.dump_label (tr_lab lbl)); branch=[Branch lbl;] }::k | Bcc (cond,r1,r2,lbl) -> - let fmt1,fmt2,r1r2 = tr_2i r1 r2 in + let fmt1,fmt2,r1,r2 = tr_2i r1 r2 in { empty_ins with memo = sprintf "%s %s,%s,%s" (A.pp_bcc cond) fmt1 fmt2 (A.Out.dump_label (tr_lab lbl)) ; - inputs=r1r2; branch=[Next;Branch lbl;]; }::k + inputs=r1@r2; branch=[Next;Branch lbl;]; }::k | Load (w,s,mo,r1,o,r2) -> let fmt1,r1 = tr_1o r1 and fmt2,r2 = tr_1i r2 in + let t = w2type w in { empty_ins with memo = sprintf "%s %s,%i(%s)" (A.pp_load w s mo) fmt1 o fmt2; - inputs=r2; outputs=r1; }::k + inputs=r2; outputs=r1; + reg_env=add_type t r1@add_type voidstar r2; }::k | Store (w,mo,r1,o,r2) -> - let fmt1,fmt2,r1r2 = tr_2i r1 r2 in + let fmt1,fmt2,r1,r2 = tr_2i r1 r2 in + let t = w2type w in { empty_ins with memo = sprintf "%s %s,%i(%s)" (A.pp_store w mo) fmt1 o fmt2; - inputs=r1r2; }::k + inputs=r1@r2; + reg_env=add_type t r1@add_type voidstar r2; }::k | LoadReserve (w,mo,r1,r2) -> let fmt1,r1 = tr_1o r1 and fmt2,r2 = tr_1i r2 in + let t = w2type w in { empty_ins with memo = sprintf "%s %s,0(%s)" (A.pp_lr w mo) fmt1 fmt2; - inputs=r2; outputs=r1; }::k + inputs=r2; outputs=r1; + reg_env=add_type t r1@add_type voidstar r2}::k | StoreConditional (w,mo,r1,r2,r3) -> let fmt1,r1 = tr_1o r1 - and fmt2,fmt3,r2r3 = tr_2i r2 r3 in + and fmt2,fmt3,r2,r3 = tr_2i r2 r3 in { empty_ins with memo = sprintf "%s %s,%s,0(%s)" (A.pp_sc w mo) fmt1 fmt2 fmt3; - outputs=r1; inputs=r2r3; }::k + outputs=r1; inputs=r2@r3; + reg_env=add_type word r1@add_type (w2type w) r2@add_type voidstar r3; + }::k | AUIPC (_,_) -> Warn.fatal "auipc not Supported in litmus" | Amo (op,w,mo,r1,r2,r3) -> let fmt1,r1 = tr_1o r1 - and fmt2,fmt3,r2r3 = tr_2i r2 r3 in + and fmt2,fmt3,r2,r3 = tr_2i r2 r3 in + let t = w2type w in { empty_ins with memo = sprintf "%s %s,%s,(%s)" (A.pp_amo op w mo) fmt1 fmt2 fmt3; - outputs=r1; inputs=r2r3; }::k + outputs=r1; inputs=r2@r3; + reg_env = add_type t (r1@r2@r2);}::k | FenceIns f -> { empty_ins with memo = pp_barrier f;}::k