Initial support for RISC-V 32 I M

CHANGELOG.md

@@ -36,7 +36,7 @@
   ([PR #948](https://github.com/jasmin-lang/jasmin/pull/948);
   fixes [#931](https://github.com/jasmin-lang/jasmin/issues/931)).
 
-- Correcting shift in location produced by multiline string annotations 
+- Correcting shift in location produced by multiline string annotations
   ([PR #959](https://github.com/jasmin-lang/jasmin/pull/959);
   fixes [#943](https://github.com/jasmin-lang/jasmin/issues/943)).
 

compiler/Makefile

@@ -17,7 +17,8 @@ CHECKCATS ?= \
 	x86-64-stack-zero-loop \
 	x86-64-stack-zero-unrolled \
 	arm-m4-stack-zero-loop \
-	arm-m4-stack-zero-unrolled
+	arm-m4-stack-zero-unrolled \
+	risc-v
 
 # --------------------------------------------------------------------
 DESTDIR  ?=

compiler/config/tests.config

@@ -94,3 +94,9 @@ args    = -stack-zero=unrolled
 okdirs  = examples/**/arm-m4 tests/success/**/arm-m4
 kodirs  = tests/fail/**/arm-m4
 exclude = tests/success/arm-m4/large_stack
+
+[test-risc-v]
+bin = ./scripts/check-risc-v
+okdirs = examples/**/risc-v tests/success/**/risc-v tests/success/**/common
+kodirs = tests/fail/**/risc-v
+exclude = tests/fail/warning

compiler/entry/commonCLI.ml

@@ -3,17 +3,20 @@ open Cmdliner
 
 let get_arch_module arch call_conv : (module Arch_full.Arch) =
   (module Arch_full.Arch_from_Core_arch
-            ((val match arch with
+            (val match arch with
                   | Utils.X86_64 ->
                       (module (val CoreArchFactory.core_arch_x86 ~use_lea:false
                                      ~use_set0:false call_conv)
                       : Arch_full.Core_arch)
                   | Utils.ARM_M4 ->
                       (module CoreArchFactory.Core_arch_ARM
-                      : Arch_full.Core_arch))))
+                      : Arch_full.Core_arch)
+                  | Utils.RISCV ->
+                      (module CoreArchFactory.Core_arch_RISCV
+                      : Arch_full.Core_arch)))
 
 let arch =
-  let alts = [ ("x86-64", Utils.X86_64); ("arm-m4", Utils.ARM_M4) ] in
+  let alts = [ ("x86-64", Utils.X86_64); ("arm-m4", Utils.ARM_M4); ("riscv", Utils.RISCV) ] in
   let doc =
     Format.asprintf "The target architecture (%s)" (Arg.doc_alts_enum alts)
   in

compiler/entry/jasmin2ec.ml

@@ -55,7 +55,7 @@ let parse_and_extract arch call_conv =
         Format.eprintf "%a@." pp_hierror e;
         exit 1
 
-let model = 
+let model =
   let alts = [ ("normal", Normal) ; ("CT", ConstantTime) ] in
   let doc =
     Format.asprintf "Extraction model (determines added annotations (e.g. leakage) (%s)."

compiler/examples/gimli/risc-v/gimli.jazz

@@ -0,0 +1,83 @@
+param int N_ROUND = 24;
+param int N_COLUMN = 4;
+param int ROUND_CONSTANT = 0x9e377900;
+
+inline
+fn swap(reg ptr u32[12] state, inline int i, inline int j) -> reg ptr u32[12] {
+    reg u32 x y;
+
+    x = state[i];
+    y = state[j];
+    state[i] = y;
+    state[j] = x;
+
+    return state;
+}
+
+inline fn ror32(reg u32 in, inline int cnt)  -> reg u32 {
+    reg u32 u l ret;
+    u = in << cnt;
+    l = in >> (32 - cnt);
+    ret = u | l;
+    return ret;
+}
+
+export
+fn gimli(reg ptr u32[12] state) -> reg ptr u32[12] {
+    inline int round, column;
+    reg u32 x, y, z;
+    reg u32 a, b;
+    reg u32 rc;
+    reg u32 tmp;
+
+    rc = ROUND_CONSTANT;
+
+    for round = N_ROUND downto 0 {
+    for column = 0 to N_COLUMN {
+    x = state[0 + column];
+    /* x <<r= 24; */ 
+    x = ror32(x,24);
+    y = state[4 + column];
+    /* y <<r= 9; */
+    y = ror32(y,9);
+    z = state[8 + column];
+
+    tmp = z << 1;
+    a = x ^ tmp;
+    b = y & z;
+    tmp = b << 2;
+    a = a ^ tmp;
+    state[8 + column] = a;
+
+    a = y ^ x;
+    b = x | z;
+    tmp = b << 1;
+    a = a ^ tmp;
+    state[4 + column] = a;
+
+    a = z ^ y;
+    b = x & y;
+    tmp = b << 3;
+    a = a ^ tmp;
+    state[0 + column] = a;
+    }
+
+    if (round % 4 == 0) {
+    state = swap(state, 0, 1);
+    state = swap(state, 2, 3);
+    }
+
+    if (round % 4 == 2) {
+    state = swap(state, 0, 2);
+    state = swap(state, 1, 3);
+    }
+
+    if (round % 4 == 0) {
+    a = state[0];
+    b = rc + round;
+    a ^= b;
+    state[0] = a;
+    }
+    }
+    return state;
+}

compiler/scripts/check-risc-v

@@ -0,0 +1,36 @@
+#!/bin/sh
+
+set -e
+
+DIR=$(mktemp -d jasminXXXXXX)
+ASM=${DIR}/jasmin.s
+OBJ=${DIR}/jasmin.o
+
+trap "rm -r ${DIR}" EXIT
+
+set -x
+
+$(dirname $0)/../jasminc -g -arch risc-v -o ${ASM} "$@"
+
+# Set default ASSEMBLY_CHECKER
+ASSEMBLY_CHECKER=${ASSEMBLY_CHECKER:-llvm-mc}
+ASSEMBLY_CHECKER_OPTIONS=${ASSEMBLY_CHECKER_OPTIONS:---triple=riscv32 --mcpu=generic-rv32 -mattr=+m --filetype=obj}
+# Detect operating system
+UNAME_S=$(uname -s)
+
+# Conditionally set ASSEMBLY_CHECKER for Darwin (macOS)
+if [ "$UNAME_S" == "Darwin" ]; then
+    ASSEMBLY_CHECKER="riscv64-unknown-elf-as"
+    ASSEMBLY_CHECKER_OPTIONS=""
+elif [ "$UNAME_S" == "Linux" ]; then
+    ASSEMBLY_CHECKER="llvm-mc"
+    ASSEMBLY_CHECKER_OPTIONS="--triple=riscv32 --mcpu=generic-rv32 -mattr=+m --filetype=obj"
+fi
+
+# Check if the assembly checker binary exists and is executable
+if ! command -v "$ASSEMBLY_CHECKER" &> /dev/null; then
+    echo "Error: $ASSEMBLY_CHECKER is not installed or not found in PATH."
+    exit 1
+fi
+
+${ASSEMBLY_CHECKER} ${ASSEMBLY_CHECKER_OPTIONS} -o ${OBJ} ${ASM}

compiler/src/CLI_errors.ml

@@ -54,6 +54,10 @@ let check_options () =
     then warning Experimental Location.i_dummy
       "support of the ARMv7 architecture is experimental";
 
+  if !target_arch = RISCV
+    then warning Experimental Location.i_dummy
+      "support of the RISC-V architecture is really experimental";
+
   if !ec_list <> []
     || !ecfile <> ""
     || !ec_array_path <> Filename.current_dir_name

compiler/src/arch_full.ml

@@ -4,9 +4,14 @@ open Arch_extra
 open Prog
 
 type 'a callstyle =
-  | StackDirect           (* call instruction push the return address on top of the stack *)
-  | ByReg of 'a option    (* call instruction store the return address on a register,
-                               (Some r) neams that the register is forced to be r *)
+  | StackDirect
+    (* call instruction push the return address on top of the stack *)
+  | ByReg of { call : 'a option; return : bool }
+    (* call instruction store the return address on a register,
+       - call: (Some r) means that the register is forced to be r
+       - return:
+         + true means that the register is also used for the return
+         + false means that there is no constraint (stack is also ok) *)
 
 (* TODO: check that we cannot use sth already defined on the Coq side *)
 
@@ -191,7 +196,7 @@ module Arch_from_Core_arch (A : Core_arch) :
   let callstyle =
     match A.callstyle with
     | StackDirect -> StackDirect
-    | ByReg o -> ByReg (Option.map var_of_reg o)
+    | ByReg { call; return } -> ByReg { call = Option.map var_of_reg call; return }
 
   let arch_info = Pretyping.{
       pd = reg_size;

compiler/src/arch_full.mli

@@ -3,9 +3,15 @@ open Arch_extra
 open Prog
 
 type 'a callstyle =
-  | StackDirect           (* call instruction push the return address on top of the stack *)
-  | ByReg of 'a option    (* call instruction store the return address on a register, 
-                               (Some r) neams that the register is forced to be r *)
+  | StackDirect
+    (* call instruction push the return address on top of the stack *)
+  | ByReg of { call : 'a option; return : bool }
+    (* call instruction store the return address on a register,
+       - call: (Some r) means that the register is forced to be r
+       - return:
+         + true means that the register is also used for the return
+         + false means that there is no constraint (stack is also ok) *)
+
 (* x86    : StackDirect 
    arm v7 : ByReg (Some ra)
    riscV  : ByReg (can it be StackDirect too ?)

compiler/src/arm_arch_full.ml

@@ -115,5 +115,5 @@ module Arm (Lowering_params : Arm_input) : Arch_full.Core_arch = struct
 
   let pp_asm = Pp_arm_m4.print_prog
 
-  let callstyle = Arch_full.ByReg (Some LR)
+  let callstyle = Arch_full.ByReg { call = Some LR; return = false }
 end

compiler/src/coreArchFactory.ml

@@ -6,6 +6,10 @@ module Core_arch_ARM : Arch_full.Core_arch = Arm_arch_full.Arm (struct
   let call_conv = Arm_decl.arm_linux_call_conv
 end)
 
+module Core_arch_RISCV : Arch_full.Core_arch = Riscv_arch_full.Riscv (struct
+  let call_conv = Riscv_decl.riscv_linux_call_conv
+end)
+
 let core_arch_x86 ~use_lea ~use_set0 call_conv :
     (module Arch_full.Core_arch
        with type reg = register

compiler/src/coreArchFactory.mli

@@ -1,4 +1,5 @@
 module Core_arch_ARM : Arch_full.Core_arch
+module Core_arch_RISCV : Arch_full.Core_arch
 open X86_decl
 
 val core_arch_x86 :

compiler/src/glob_options.ml

@@ -53,6 +53,7 @@ let set_target_arch a =
     match a with
     | "x86-64" -> X86_64
     | "arm-m4" -> ARM_M4
+    | "risc-v" -> RISCV
     | _ -> assert false
   in target_arch := a'
 
@@ -135,9 +136,11 @@ let print_strings = function
   | Compiler.RegArrayExpansion           -> "arrexp"   , "expansion of register arrays"
   | Compiler.RemoveGlobal                -> "rmglobals", "remove globals variables"
   | Compiler.MakeRefArguments            -> "makeref"  , "add assignments before and after call to ensure that arguments and results are ref ptr"
+  | Compiler.LoadConstantsInCond         -> "loadconst", "introduce registers for constants appearing in conditions (RISC-V only)"
   | Compiler.LowerInstruction            -> "lowering" , "lowering of instructions"
   | Compiler.PropagateInline             -> "propagate", "propagate inline variables"
   | Compiler.SLHLowering                 -> "slhlowering" , "lowering of selective load hardening instructions"
+  | Compiler.LowerAddressing             -> "loweraddr", "lowering of complex addressing modes (RISC-V only)"
   | Compiler.StackAllocation             -> "stkalloc" , "stack allocation"
   | Compiler.RemoveReturn                -> "rmreturn" , "remove unused returned values"
   | Compiler.RegAllocation               -> "ralloc"   , "register allocation"
@@ -207,7 +210,7 @@ let options = [
     "-intel", Arg.Unit (set_syntax `Intel), " Use intel syntax (default is AT&T)"; 
     "-ATT", Arg.Unit (set_syntax `ATT), " Use AT&T syntax (default is AT&T)"; 
     "-call-conv", Arg.Symbol (["windows"; "linux"], set_cc), " Select calling convention (default depends on host architecture)";
-    "-arch", Arg.Symbol (["x86-64"; "arm-m4"], set_target_arch), " Select target arch (default is x86-64)";
+    "-arch", Arg.Symbol (["x86-64"; "arm-m4"; "risc-v"], set_target_arch), " Select target arch (default is x86-64)";
     "-stack-zero",
       Arg.Symbol (List.map fst stack_zero_strategies, set_stack_zero_strategy),
       " Select stack zeroization strategy for export functions";

compiler/src/help.ml

@@ -8,7 +8,7 @@ let show_intrinsics asmOp fmt =
       begin match sfx with
       | [] -> 0
       | PVp _ :: _ -> 1
-      | PVx _ :: _ -> 2
+      | (PVs _ | PVx _) :: _ -> 2
       | (PVv _ | PVsv _) :: _ -> 3
       | PVvv _ :: _ -> 4
       end
@@ -17,7 +17,7 @@ let show_intrinsics asmOp fmt =
   let headers = [|
       "no size suffix";
       "one optional size suffix, e.g., “_64”";
-      "a zero/sign extend suffix, e.g., “_u32u16”";
+      "a zero/sign extend suffix, e.g., “_s16” or “_u32u16”";
       "one vector description suffix, e.g., “_4u64”";
       "two vector description suffixes, e.g., “_2u16_2u64”";
       "a flag setting suffix (i.e. “S”) and a condition suffix (i.e. “cc”)"

compiler/src/lexer.mll

@@ -6,7 +6,7 @@
   module S = Syntax
 
   let increment_newline s lexbuf =
-    let newlines = String.count_char s '\n' in 
+    let newlines = String.count_char s '\n' in
     for _ = 1 to newlines do
       Lexing.new_line lexbuf
     done
@@ -35,8 +35,8 @@
 
     "bool"  , T_BOOL ;
     "int"   , T_INT  ;
-    
-    "const" , CONSTANT; 
+
+    "const" , CONSTANT;
     "downto", DOWNTO ;
     "else"  , ELSE   ;
     "exec"  , EXEC   ;
@@ -74,7 +74,7 @@
   let mk_sign : char option -> S.sign =
   function
   | Some c -> sign_of_char c
-  | None   -> `Unsigned 
+  | None   -> `Unsigned
 
   let size_of_string =
   function
@@ -89,7 +89,7 @@
   let mksizesign sw s = size_of_string sw, sign_of_char s
 
   let mk_gensize = function
-    | "1"   -> `W1 
+    | "1"   -> `W1
     | "2"   -> `W2
     | "4"   -> `W4
     | "8"   -> `W8
@@ -101,13 +101,13 @@
 
 
   let mk_vsize   = function
-    | "2"  -> `V2  
+    | "2"  -> `V2
     | "4"  -> `V4
     | "8"  -> `V8
-    | "16" -> `V16 
+    | "16" -> `V16
     | "32" -> `V32
-    | _    ->  assert false 
- 
+    | _    ->  assert false
+
   let mkvsizesign r s g = mk_vsize r, sign_of_char s, mk_gensize g
 
 }
@@ -127,8 +127,8 @@ let ident    = idletter (idletter | digit)*
 
 let size = "8" | "16" | "32" | "64" | "128" | "256"
 let signletter = ['s' 'u']
-let gensize = "1" | "2" | "4" | "8" | "16" | "32" | "64" | "128" 
-let vsize   = "2" | "4" | "8" | "16" | "32" 
+let gensize = "1" | "2" | "4" | "8" | "16" | "32" | "64" | "128"
+let vsize   = "2" | "4" | "8" | "16" | "32"
 
 
 (* -------------------------------------------------------------------- *)

compiler/src/main_compiler.ml

@@ -88,6 +88,11 @@ let main () =
             module C = CoreArchFactory.Core_arch_ARM
             let analyze _ _ _ _ _ = failwith "TODO_ARM: analyze"
           end)
+      | RISCV ->
+         (module struct
+            module C = CoreArchFactory.Core_arch_RISCV
+            let analyze _ _ _ _ _ = failwith "TODO_RISCV: analyze"
+          end)
     in
     let module Arch = Arch_full.Arch_from_Core_arch (P.C) in