Initial support for RISC-V 32 I M #781

clebreto · 2024-04-08T08:18:16Z

…s (ADD / ADDI). (#706) * Provides RISCV initial architecture description and first instructions (ADD / ADDI). Co-authored-by: Benjamin Gregoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr> --------- Co-authored-by: Benjamin Gregoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Co-authored-by: LE BRETON Come <come.le-breton@inria.fr>

Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>

Add XOR and OR to compiler/riscv_instr_decl.v --------- Co-authored-by: Julian Wälde <julian.waelde@hs-rm.de> Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Renames registers. Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Riscv compiler skeleton

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Co-authored-by: Jean-Christophe Léchenet<jean-christophe.lechenet@inria.fr>

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

+ Fix push / pop ra to stack

It looks like gp may be used to access globals. I don't know for tp, but to be safe I added both of them into the list of callee-saved registers.

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Otherwise they are tested alone.

and select a different default on MacOS (We probably don't want to integrate this as is in main)

This pass compiles, on RISC-V, complex loads and stores into 3 equivalent instructions for which assembly can be generated. This is kind of a hack for now. Ideally, we would support subarrays with non-constant offset and a way to do pointer arithmetic.

for arm. Proof still required. Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Proof missing in params_core. Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

…ctions-in-a-same-fashion-as-it-was-done-for-arm-1 789 risc v test every instructions in a same fashion as it was done for arm 1 Bug fixes to main risc-v branch have been added, as well as compiler pass. It notably adds a lowering compiler pass for complex addresses.

vbgl

Thanks for this hard work. My comments are mostly cosmetic.

vbgl · 2024-09-23T09:10:09Z

compiler/src/help.ml

@@ -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”";


This is surprising: does it mean that it is now possible to write MOVSX_s16?

vbgl · 2024-09-23T09:12:35Z

default.nix

+         ppxlib
+         ppx_import
+         ppx_sexp_conv
+         ppx_yojson_conv
+         ppx_deriving
+         sel
+         lsp
+         sexplib


Is this change really meant to be included in this PR?

vbgl · 2024-09-23T09:14:01Z

proofs/compiler/riscv_instr_decl.v

+(*CHECKME*)
+Definition riscv_sra_semi (wn : ty_r) (wm : word U8) : exec ty_r := ok (wsar wn (wunsigned (wand wm (wrepr U8 31)))).
+


Should this be checked before merging?

vbgl · 2024-09-23T09:14:49Z

proofs/compiler/riscv_lower_addressing_proof.v

+(* TODO: move *)
+Lemma write_lval_eq_ex wdb gd X x v s1 s2 vm1 :


This can be addressed before merging.

vbgl · 2024-09-23T09:15:09Z

proofs/compiler/riscv_lower_addressing_proof.v

+(* TODO: move *)
+Lemma sem_sopn_eq_ex X gd o xs es s1 s2 vm1 :


vbgl · 2024-09-23T09:16:31Z

proofs/compiler/riscv_lowering_proof.v

+  riscv_decl
+  riscv_extra
+  riscv_instr_decl
+  (* riscv_instr_decl_lemmas *)


Should this comment be removed?

vbgl · 2024-09-23T09:17:43Z

proofs/compiler/riscv_params.v

+Definition riscv_loparams : lowering_params lowering_options :=
+  {|
+    lop_lower_i _ _ _ := lower_i;
+    lop_fvars_correct := fun _ _ _ => true; (* FIXME RISCV: is this correct? *)


Please fix this.

vbgl · 2024-09-23T09:18:37Z

proofs/compiler/riscv_params_common_proof.v

+(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
+Lemma align_eval_instr {lp ls ii xname vi y al} {wy : word Uptr} :


Is this really a FIXME? If it is the case, then please fix it. Otherwise please change to TODO.

vbgl · 2024-09-23T09:18:46Z

proofs/compiler/riscv_params_common_proof.v

+(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
+Lemma sub_eval_instr {lp ls ii xname vi y z} {wy wz : word Uptr} :


vbgl · 2024-09-23T09:19:30Z

proofs/compiler/riscv_params_core_proof.v

+(* Lemma li_lsem_1 s xname vi imm :
+  let: (xi, x) := mkv xname vi in


This comment might be removed.

The passes between stack_alloc and reg_alloc are called twice, first in OCaml and then in Coq. Pass LowerAddressing was inserted between stack_alloc and reg_alloc, but was only called in Coq, creating a discrepancy between the two calls (in OCaml and in Coq). The pass is now called also in OCaml. Due to the way complex Coq types are extracted in OCaml, we had to make some types simpler on the Coq side to be able to call the pass in OCaml.

RA is not used as the return address storage AND the return value in the same function.

rtetley and others added 27 commits February 5, 2024 09:14

Add dependencies to build vscoq-language-server (temp fix).

0be66c6

Adds SUB, AND, MV

bfafb60

Co-authored-by: LE BRETON Come <come.le-breton@inria.fr>

Adds LOAD and STORE

881bfc8

Co-authored-by: LE BRETON Come <come.le-breton@inria.fr>

Refactor cond

121aad6

Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>

Add XOR and OR to compiler/riscv_instr_decl.v (#747)

65371a0

Add XOR and OR to compiler/riscv_instr_decl.v --------- Co-authored-by: Julian Wälde <julian.waelde@hs-rm.de> Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Adds the very minimal bits for dummy compilation.

35faf94

Renames registers. Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

WIP : bug-499.

602bee6

Adds li to implement more functionalities.

8055c6d

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Merge pull request #754 from jasmin-lang/riscv-compiler-skeleton

254fd06

Riscv compiler skeleton

Merge branch 'main' into risc-v

218dc38

Adds XOR lowering.

b0b4453

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Fix adressing assembly syntax.

3a80c10

Intrepret "subi" as ADDI.

f9fc5db

Factorize instructions by encodings.

9778be6

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Adds swap and subi as extra ops.

7a00b90

Co-authored-by: Jean-Christophe Léchenet<jean-christophe.lechenet@inria.fr>

Condition lowering implementation.

84b5d1b

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Provides JAL instruction to match calling convention

12e88bc

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Provides tests for branching conditions.

9309743

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Hack to compare with imm.

2f9c8c8

+ Fix push / pop ra to stack

X1 -> X2

ff7977e

X1 -> X2 again

33f5b14

Push and pop ok

50e48b8

assemble_cond: correctly detects 0

6f1cc0e

Fixes program crash

6d84586

It looks like gp may be used to access globals. I don't know for tp, but to be safe I added both of them into the list of callee-saved registers.

Allows to execute at least once each test.

8e2aa91

Merge branch 'main' into risc-v

922c98c

eponier force-pushed the risc-v branch from abaad88 to 922c98c Compare April 10, 2024 09:10

clebreto added 2 commits April 10, 2024 11:35

Check execution of tests.

ff82fa2

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Adds MUL MULH instructions declaration.

7de90ac

clebreto and others added 16 commits September 16, 2024 18:01

WIP large stack

df758a9

printing

02174a6

multiple fixes

cca80c3

Adds load and fix test.

f0667d0

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Adds sra instruction and associated proof.

6313772

FIX typo.

c20b1a9

Adds shift basic tests.

4545b4a

Template test files must be .jinc (again)

914d965

Otherwise they are tested alone.

Use an env var for assembly checker on risc-v

7ce49f6

and select a different default on MacOS (We probably don't want to integrate this as is in main)

Prove riscv_lower_addressing

26fe70b

This pass compiles, on RISC-V, complex loads and stores into 3 equivalent instructions for which assembly can be generated. This is kind of a hack for now. Ideally, we would support subarrays with non-constant offset and a way to do pointer arithmetic.

Fix macos / linux assembly checker option handling

03dab30

Use jasmin shift semantic properly.

11d9268

Introduce smart_addi to stack alloc as done

013919d

for arm. Proof still required. Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Moves subi from ext op to lowering.

a2473d9

Proof missing in params_core. Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

End of the proofs

df36861

clebreto marked this pull request as ready for review September 18, 2024 08:03

vbgl reviewed Sep 23, 2024

View reviewed changes

clebreto and others added 9 commits September 30, 2024 16:22

Clear out unused Lemma.

72d4742

FIXME -> TODO.

7212a26

x28 x29 are FP temporaries -> OK

1b6f96f

FIXME -> Comment

2296f15

Fix typo.

9ddd343

Remove comment

9008aad

move write_lval_eq to psem_facts.

eba00c4

Add RA to the list of callee_saved registers.

7a14e76

RA is not used as the return address storage AND the return value in the same function.

clebreto force-pushed the risc-v branch from 86effc3 to 7a14e76 Compare October 8, 2024 12:37

bgregoir added 2 commits October 17, 2024 13:53

Merge branch 'main' into risc-v

b74ebeb

adapte 4fc6626 to risc-v

f286134

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Initial support for RISC-V 32 I M #781

Initial support for RISC-V 32 I M #781

clebreto commented Apr 8, 2024 •

edited

Loading

vbgl left a comment

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

vbgl Sep 23, 2024

		(CHECKME)
		Definition riscv_sra_semi (wn : ty_r) (wm : word U8) : exec ty_r := ok (wsar wn (wunsigned (wand wm (wrepr U8 31)))).

		(* TODO: move *)
		Lemma write_lval_eq_ex wdb gd X x v s1 s2 vm1 :

		(* TODO: move *)
		Lemma sem_sopn_eq_ex X gd o xs es s1 s2 vm1 :

		(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
		Lemma align_eval_instr {lp ls ii xname vi y al} {wy : word Uptr} :

		(* FIXME try to remove the usage of this lemma, use sem_fopn_args version instead *)
		Lemma sub_eval_instr {lp ls ii xname vi y z} {wy wz : word Uptr} :

		(* Lemma li_lsem_1 s xname vi imm :
		let: (xi, x) := mkv xname vi in

Initial support for RISC-V 32 I M #781

Are you sure you want to change the base?

Initial support for RISC-V 32 I M #781

Conversation

clebreto commented Apr 8, 2024 • edited Loading

vbgl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

clebreto commented Apr 8, 2024 •

edited

Loading