[herd,litmus,RISCV] Implement the li pseudo-insrcution

This direct implementation is motivated by the
sise of its argument (64bits).

Author: maranget

herd/RISCVArch_herd.ml

@@ -24,7 +24,7 @@ module Make (C:Arch_herd.Config) (V:Value.S) =
 
     let is_amo = function
       | Amo _ -> true
-      | INop|Ret|J _|Bcc _|Load _|Store _|LoadReserve _
+      | INop|Ret|Li _|J _|Bcc _|Load _|Store _|LoadReserve _
       | OpI _|OpI2 _|OpIW _|Op _|OpW _|OpA _
       |StoreConditional _|FenceIns _
       |AUIPC _| Ext _
@@ -106,7 +106,7 @@ module Make (C:Arch_herd.Config) (V:Value.S) =
     module V = V
 
     let mem_access_size = function
-      | INop | Ret | OpI _ | OpI2 _ | OpIW _ | Op _ | OpW _
+      | INop | Ret | Li _ | OpI _ | OpI2 _ | OpIW _ | Op _ | OpW _
       | J _ | Bcc _ | FenceIns _ | OpA _ | AUIPC _
       | Ext _
         -> None

herd/RISCVSem.ml

@@ -271,6 +271,9 @@ module
           begin match ii.A.inst with
           | RISCV.INop-> B.next1T ()
           | RISCV.Ret when O.variant Variant.Telechat -> M.unitT () >>! B.Exit
+          | RISCV.Li (r,k) ->
+              let v = V.Cst.Scalar.of_int64 k |> V.scalarToV in
+              write_reg r v ii >>= B.next1T
           | RISCV.OpI2 (RISCV.LUI,r1,k) ->
               (* put k into upper half of r1*)
               M.op (Op.ShiftLeft) (V.intToV k)

jingle/RISCVArch_jingle.ml

@@ -79,6 +79,9 @@ include Arch.MakeArch(struct
     and find_lab = find_lab subs
     and find_cst = find_cst subs in
     function
+      | Li (r1,k) ->
+          conv_reg r1 >! fun r1 ->
+          Li (r1,k)
       | OpI (op,r1,r2,k) ->
           conv_reg r1 >> fun r1 ->
           conv_reg r2 >> fun r2 ->

lib/RISCVBase.ml

@@ -314,6 +314,7 @@ type signed = Sign.t
 type 'k kinstruction =
   | INop
   | Ret
+  | Li of reg * Int64.t
   | OpI of opi * reg * reg * 'k
   | OpI2 of opi2 * reg * 'k
   | OpA of opa * reg * lbl
@@ -348,6 +349,7 @@ type 'k basic_pp = { pp_k : 'k -> string; is_zero : 'k -> bool }
 let do_pp_instruction m = function
   | INop -> "nop"
   | Ret -> "ret"
+  | Li (r,k) -> sprintf "li %s,%Li" (pp_reg r) k
   (* MV is a pseudoinstruction - special case of ADDI*)
   | OpI (ADDI, r1,r2,k) when m.is_zero k ->
       sprintf "mv %s,%s" (pp_reg r1) (pp_reg r2)
@@ -430,6 +432,7 @@ let fold_regs (f_reg,f_sreg) =
 
   fun c ins -> match ins with
   | INop|Ret|J _ | FenceIns _ -> c
+  | Li (r1,_)
   | OpA (_,r1,_) | AUIPC (r1,_) | OpI2 (_,r1,_) -> fold_reg r1 c
   | OpI (_,r1,r2,_) | OpIW (_,r1,r2,_)
   | Bcc (_,r1,r2,_)
@@ -451,6 +454,7 @@ let map_regs f_reg f_symb =
 
   function ins -> match ins with
   | INop|Ret|J _ | FenceIns _ -> ins
+  | Li (r,k) -> Li (map_reg r,k)
   | OpI (op,r1,r2,k) ->
       OpI (op,map_reg r1,map_reg r2,k)
   | OpI2 (op,r1,k) ->
@@ -488,7 +492,7 @@ let map_addrs _f ins = ins
 let get_next = function
   | J lbl -> [Label.To lbl;]
   | Bcc (_,_,_,lbl) -> [Label.Next; Label.To lbl;]
-  | INop|Ret|OpI (_, _, _, _)|OpIW (_, _, _, _)|Op (_, _, _, _)|OpW (_, _, _, _) | OpA (_,_,_) | AUIPC (_,_)
+  | INop|Ret|Li _|OpI (_, _, _, _)|OpIW (_, _, _, _)|Op (_, _, _, _)|OpW (_, _, _, _) | OpA (_,_,_) | AUIPC (_,_)
   | OpI2 (_,_,_)
   | Load (_,_, _, _, _, _)|Store (_,_, _, _, _)|LoadReserve (_, _, _, _)
   | StoreConditional (_, _, _, _, _)|FenceIns _|Amo _|Ext (_,_,_,_)
@@ -510,7 +514,7 @@ include Pseudo.Make
       | OpIW (op,r1,r2,k) -> OpIW (op,r1,r2,k_tr k)
       |AUIPC (r1, k) -> AUIPC (r1,k_tr k)
       | Op (_, _, _, _)|OpW (_, _, _, _)|J _|Bcc (_, _, _, _)
-      |INop | Ret | OpA (_,_,_)
+      |INop | Ret | Li _ | OpA (_,_,_)
       |Load (_, _, _, _, _, _)|Store (_, _ ,_ , _, _)
       | Ext (_,_,_,_)
       |LoadReserve (_, _, _, _)|StoreConditional (_, _, _, _, _)|Amo _|FenceIns _
@@ -524,6 +528,7 @@ include Pseudo.Make
         | Amo _ -> 2
         | INop
         | Ret
+        | Li _
         | OpI (_, _, _, _)|OpIW (_, _, _, _)|Op (_, _, _, _)
         | OpI2 (_,_,_)
         | OpA (_,_,_) | AUIPC (_,_) | Ext (_,_,_,_)
@@ -538,6 +543,7 @@ include Pseudo.Make
           -> f k lbl
         | INop
         | Ret
+        | Li _
         |OpI (_, _, _, _)|OpIW (_, _, _, _)|Op (_, _, _, _) | AUIPC (_,_)
         | OpI2 (_,_,_)
         |OpW (_, _, _, _)|Load (_, _, _, _, _, _)|Store (_, _, _, _, _)
@@ -550,6 +556,7 @@ include Pseudo.Make
         | OpA (op,r1,lbl) -> OpA (op,r1,BranchTarget.as_string_fun f lbl)
         |INop
         |Ret
+        |Li _
         |OpI (_, _, _, _)|OpIW (_, _, _, _)|Op (_, _, _, _)
         | OpI2 (_,_,_)
         |OpW (_, _, _, _)|Load _|Store _| AUIPC (_,_)

lib/RISCVLexer.mll

@@ -219,7 +219,7 @@ rule token = parse
 | [' ''\t''\r'] { token lexbuf }
 | '\n'      { incr_lineno lexbuf; token lexbuf }
 | "(*"      { LU.skip_comment lexbuf ; token lexbuf }
-| '-' ? num as x { NUM (int_of_string x) }
+| '-' ? num as x { NUM x }
 | 'P' (num as x)
     { PROC (int_of_string x) }
 | '&' (name as x) { META x }

lib/RISCVParser.mly

@@ -31,7 +31,7 @@ let tr_rw = function
 %token EOF
 %token <RISCVBase.reg> ARCH_REG
 %token <string> SYMB_REG
-%token <int> NUM
+%token <string> NUM
 %token <string> NAME
 %token <int> PROC
 
@@ -96,18 +96,18 @@ reg:
 | ARCH_REG { $1 }
 
 k:
-| NUM  { MetaConst.Int $1 }
+| NUM  { MetaConst.Int (int_of_string $1) }
 | META { MetaConst.Meta $1 }
 
 addr:
 | NUM LPAR reg RPAR
-    { $1,$3 }
+    { int_of_string $1,$3 }
 | LPAR reg RPAR
     { 0,$2 }
 
 addr0:
 | NUM LPAR reg RPAR
-    { if $1 <> 0 then raise Parsing.Parse_error;
+    { if $1 <> "0" then raise Parsing.Parse_error;
       $3 }
 | LPAR reg RPAR
     { $2 }
@@ -118,8 +118,8 @@ instr:
 | RET
   { A.Ret }
 /* OPs */
-| LI reg COMMA k
-  { A.OpI (A.ORI,$2,A.Ireg A.X0,$4) }
+| LI reg COMMA NUM
+   { A.Li ($2,Int64.of_string $4) }
 | LA reg COMMA NAME
   { A.OpA (A.LA,$2,$4) }
 | LUI reg COMMA k

lib/genParserUtils.ml

@@ -37,10 +37,10 @@ let call_parser name lexbuf lex parse =
   | Misc.Timeout as e -> raise e
   | e ->
       Printf.eprintf
-        "%a: Uncaught exception %s (in %s)\n"
+        "%a: Exception raised in parser %s (in %s)\n"
         Pos.pp_pos lexbuf.lex_curr_p
         (Printexc.to_string e) name ;
-      assert false
+      raise e
 
 
 (************************)

litmus/RISCVCompile_litmus.ml

@@ -57,6 +57,12 @@ module Make(V:Constant.S)(C:Arch_litmus.Config) =
         memo = sprintf "%s %s,%s,%i" memo fmt1 fmt2 k ;
         inputs=r2; outputs=r1; }
 
+    let li r k =
+      let fmt,r = tr_1o r in
+      { empty_ins with
+        memo = sprintf "li %s,%Li" fmt k ;
+        outputs=r; }
+
     let lui r1 k =
       let fmt1,r1 = tr_1o r1 in
       { empty_ins with
@@ -90,6 +96,8 @@ module Make(V:Constant.S)(C:Arch_litmus.Config) =
     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
+    | A.Li (r,i) ->
+        li r i::k
     | A.OpI2 (A.LUI,r1,i) ->
         lui r1 i::k
     | A.OpI (op,r1,r2,i) ->