Initial support for RISC-V 32 I M

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,8 @@ 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

compiler/entry/jasmin2ec.ml

@@ -54,7 +54,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/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

@@ -49,13 +49,15 @@ let set_stack_zero_size s = stack_zero_size := Some (Annot.ws_of_string s)
 type architecture =
   | X86_64
   | ARM_M4
+  | RISCV
 let target_arch = ref X86_64
 
 let set_target_arch a =
   let a' =
     match a with
     | "x86-64" -> X86_64
     | "arm-m4" -> ARM_M4
+    | "risc-v" -> RISCV
     | _ -> assert false
   in target_arch := a'
 
@@ -141,6 +143,7 @@ let print_strings = function
   | 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"
@@ -210,7 +213,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/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
 

compiler/src/parser.mly

@@ -3,7 +3,7 @@
   open Syntax
   open Annotations
 
-  let setsign c s = 
+  let setsign c s =
     match c with
     | None -> Some (Location.mk_loc (Location.loc s) (CSS(None, Location.unloc s)))
     | _    -> c
@@ -20,7 +20,7 @@
 %token RPAREN
 
 %token T_BOOL
-%token T_U8 T_U16 T_U32 T_U64 T_U128 T_U256 T_INT 
+%token T_U8 T_U16 T_U32 T_U64 T_U128 T_U256 T_INT
 
 %token SHARP
 %token ALIGNED
@@ -95,7 +95,7 @@
 %left LTLT GTGT ROR ROL
 %left PLUS MINUS
 %left STAR SLASH PERCENT
-%nonassoc BANG 
+%nonassoc BANG
 
 %type <Syntax.pprogram> module_
 
@@ -126,9 +126,9 @@ annotationlabel:
   | id=loc(keyword) { id }
   | s=loc(STRING) { s }
 
-int: 
+int:
   | i=INT       { Syntax.parse_int i }
-  | MINUS i=INT { Z.neg (Syntax.parse_int i ) } 
+  | MINUS i=INT { Z.neg (Syntax.parse_int i ) }
 
 simple_attribute:
   | i=int          { Aint i    }
@@ -146,14 +146,14 @@ annotation:
 
 struct_annot:
   | a=separated_list(COMMA, annotation) { a }
-  
+
 top_annotation:
   | SHARP a=annotation    { [a] }
   | SHARP LBRACKET a=struct_annot RBRACKET { a }
 
 annotations:
   | l=list(top_annotation) { List.concat l }
-  
+
 
 (* ** Type expressions
  * -------------------------------------------------------------------- *)
@@ -195,7 +195,7 @@ castop1:
 castop:
 | c=loc(castop1)? { c }
 
-cast: 
+cast:
 | T_INT    { `ToInt }
 | s=swsize { `ToWord s }
 
@@ -216,7 +216,7 @@ cast:
 | AMP         c=castop { `BAnd c}
 | PIPE        c=castop { `BOr  c}
 | HAT         c=castop { `BXOr c}
-| LTLT        c=castop { `ShL  c} 
+| LTLT        c=castop { `ShL  c}
 | s=loc(GTGT) c=castop { `ShR (setsign c s)}
 | ROR         c=castop { `ROR  c}
 | ROL         c=castop { `ROL  c}
@@ -241,8 +241,8 @@ prim:
 %inline mem_access:
 | ct=parens(utype)? LBRACKET al=unaligned? v=var e=mem_ofs? RBRACKET
   { al, ct, v, e }
-  
-arr_access_len: 
+
+arr_access_len:
 | COLON e=pexpr { e }
 
 arr_access_i:
@@ -367,7 +367,7 @@ pinstr_r:
 | WHILE is1=pblock? LPAREN b=pexpr RPAREN is2=pblock?
     { PIWhile (is1, b, is2) }
 
-| vd=postfix(pvardecl(COMMA?), SEMICOLON) 
+| vd=postfix(pvardecl(COMMA?), SEMICOLON)
     { PIdecl vd }
 
 pif:
@@ -404,17 +404,17 @@ annot_stor_type:
 
 writable:
 | CONSTANT    {`Constant }
-| MUTABLE     {`Writable } 
+| MUTABLE     {`Writable }
 
 pointer:
 | o=writable? POINTER { o }
 
 ptr:
-| o=pointer? { 
-   match o with 
+| o=pointer? {
+   match o with
    | Some w -> `Pointer w
-   | None   -> `Direct 
-   } 
+   | None   -> `Direct
+   }
 
 storage:
 | REG    ptr=ptr { `Reg ptr }
@@ -430,7 +430,7 @@ storage:
 %inline pvardecl(S):
 | ty=stor_type vs=separated_nonempty_list(S, loc(decl)) { (ty, vs) }
 
-pparamdecl(S): 
+pparamdecl(S):
     ty=stor_type vs=separated_nonempty_list(S, var) { (ty, vs) }
 
 annot_pparamdecl:
@@ -472,7 +472,7 @@ pparam:
 (* -------------------------------------------------------------------- *)
 pgexpr:
 | e=pexpr { GEword e }
-| LBRACE es = rtuple1(pexpr) RBRACE { GEarray es } 
+| LBRACE es = rtuple1(pexpr) RBRACE { GEarray es }
 | e=loc(STRING) { GEstring e }
 
 pglobal: