Skip to content

Commit 2ede5ef

Browse files
arichardsonptomsich
arichardson
authored and
ptomsich
committed
Run the pre-commit hook on all files
This strips trailing whitespace and fixes line endings. I had to add the *.dump files to the exclude list to avoid excessive changes, but ideally these would not be part of the repository since they can just be generated by running objdump manually.
1 parent 33ef4a3 commit 2ede5ef

28 files changed

+115
-115
lines changed

‎.pre-commit-config.yaml

+6
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,12 @@ repos:
66
rev: v3.2.0
77
hooks:
88
- id: trailing-whitespace
9+
# Do not strip trailing whitespace from patches or SVG images.
10+
# TODO: the objdump outputs should probably not be part of the repo.
11+
exclude: '.*\.(diff|dump|patch|svg)'
912
- id: end-of-file-fixer
13+
# Do not strip trailing newlines from patches or SVG images.
14+
# TODO: the objdump outputs should probably not be part of the repo.
15+
exclude: '.*\.(diff|dump|patch|svg)'
1016
- id: check-yaml
1117
- id: check-added-large-files

‎LICENCE

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ Copyright (c) 2017-2023
1616
Shaked Flur
1717
Christopher Pulte
1818
Peter Sewell
19-
Alexander Richardson
20-
Hesham Almatary
19+
Alexander Richardson
20+
Hesham Almatary
2121
Jessica Clarke
2222
Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo
2323
Peter Rugg

‎README.md

+8-8
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ coverage of the prose RISC-V specification is summarized
1212
[here](doc/Status.md).
1313
A [reading guide](doc/ReadingGuide.md) to the model is provided in the
1414
[doc/](doc/) subdirectory, along with a guide on [how to
15-
extend](doc/ExtendingGuide.md) the model.
15+
extend](doc/ExtendingGuide.md) the model.
1616

1717

1818
Latex definitions can be generated from the model that are suitable
@@ -23,7 +23,7 @@ specifications that include the Sail formal definitions are available
2323
in the sail branch of this [risc-v-isa-manual repository](https://github.com/rems-project/riscv-isa-manual/tree/sail).
2424
The process to perform this inclusion is explained [here](https://github.com/rems-project/riscv-isa-manual/blob/sail/README.SAIL).
2525

26-
This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_Public_Review/blob/master/comparison_table.md) that were compared within the
26+
This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_Public_Review/blob/master/comparison_table.md) that were compared within the
2727
[RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review).
2828

2929

@@ -35,16 +35,16 @@ What is Sail?
3535
engineer-friendly, vendor-pseudocode-like language for describing
3636
instruction semantics. It is essentially a first-order imperative
3737
language, but with lightweight dependent typing for numeric types and
38-
bitvector lengths, which are automatically checked using Z3.
38+
bitvector lengths, which are automatically checked using Z3.
3939
<p>
4040

4141
Given a Sail definition, the tool will type-check it and generate
4242
LaTeX snippets to use in documentation, executable emulators (in C and OCaml), theorem-prover definitions for
43-
Isabelle, HOL4, and Coq, and definitions to integrate with our
43+
Isabelle, HOL4, and Coq, and definitions to integrate with our
4444
<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a>
4545
and
4646
<a href="isla-axiomatic.cl.cam.ac.uk/">isla-axiomatic</a> tools for
47-
concurrency semantics.
47+
concurrency semantics.
4848
<p>
4949

5050
<img width="800" src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png?">
@@ -116,7 +116,7 @@ mapping clause assembly = ITYPE(imm, rs1, rd, op)
116116
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
117117
~~~~~~
118118
119-
### SRET
119+
### SRET
120120
121121
~~~~~
122122
union clause ast = SRET : unit
@@ -357,7 +357,7 @@ For booting operating system images, see the information under the
357357
### Using development versions of Sail
358358
359359
Rarely, the version of Sail packaged in opam may not meet your needs. This could happen if you need a bug fix or new feature not yet in the released Sail version, or you are actively working on Sail. In this case you can tell the `sail-riscv` `Makefile` to use a local copy of Sail by setting `SAIL_DIR` to the root of a checkout of the Sail repo when you invoke `make`. Alternatively, you can use `opam pin` to install Sail from a local checkout of the Sail repo as described in the Sail installation instructions.
360-
360+
361361
Licence
362362
-------
363363
@@ -368,7 +368,7 @@ Authors
368368
-------
369369
370370
Prashanth Mundkur, SRI International;
371-
Rishiyur S. Nikhil (Bluespec Inc.);
371+
Rishiyur S. Nikhil (Bluespec Inc.);
372372
Jon French, University of Cambridge;
373373
Brian Campbell, University of Edinburgh;
374374
Robert Norton-Wright, University of Cambridge and Microsoft;

‎build_simulators.sh

-1
Original file line numberDiff line numberDiff line change
@@ -15,4 +15,3 @@ test_build make ARCH=RV64 ocaml_emulator/riscv_ocaml_sim_RV64
1515

1616
test_build make ARCH=RV32 c_emulator/riscv_sim_RV32
1717
test_build make ARCH=RV64 c_emulator/riscv_sim_RV64
18-

‎doc/Status.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ The Sail specification currently captures the following ISA features:
1919

2020
- Physical Memory Protection (PMP)
2121

22-
For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the
22+
For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the
2323
RMEM tool](https://github.com/rems-project/rmem).
2424

2525
The Sail specification is parameterized over the following

‎doc/notes_FD_extensions.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ This will be merged back into the main original repo after testing.
1414
Status (2019-10-24)
1515
-------------------
1616

17-
1. Complete (almost): SAIL coding [Rishiyur Nikhil, Bluespec, Inc.]
17+
1. Complete (almost): SAIL coding [Rishiyur Nikhil, Bluespec, Inc.]
1818
Remaining: tweaks to handle illegal rounding modes.
1919
2. In progress: Incorporate Berkeley SoftFloat calls [U.Cambridge]
2020
3. To do: Testing on all ISA tests

‎etc/headache_config

-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,3 @@
44
| ".*\\.thy" -> frame open:"(*" line:"=" close:"*)"
55
| ".*\\.sml" -> frame open:"(*" line:"=" close:"*)"
66
| ".*\\.sail" -> frame open:"/*" line:"=" close:"*/"
7-

‎handwritten_support/hgen/herdtools_types_to_shallow_types.hgen

+10-10
Original file line numberDiff line numberDiff line change
@@ -59,9 +59,9 @@ let translate_amoop op = match op with
5959
| RISCVAMOMAXU -> AMOMAXU
6060

6161
let translate_wordWidth op = match op with
62-
| RISCVBYTE -> BYTE
63-
| RISCVHALF -> HALF
64-
| RISCVWORD -> WORD
62+
| RISCVBYTE -> BYTE
63+
| RISCVHALF -> HALF
64+
| RISCVWORD -> WORD
6565
| RISCVDOUBLE -> DOUBLE
6666

6767
let translate_bool name b = b (* function
@@ -70,21 +70,21 @@ let translate_bool name b = b (* function
7070

7171
let translate_imm21 name value =
7272
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty21_dict (Nat_big_num.of_int value)
73-
74-
let translate_imm20 name value =
73+
74+
let translate_imm20 name value =
7575
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty20_dict (Nat_big_num.of_int value)
76-
76+
7777
let translate_imm13 name value =
7878
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty13_dict (Nat_big_num.of_int value)
79-
79+
8080
let translate_imm12 name value =
8181
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty12_dict (Nat_big_num.of_int value)
82-
82+
8383
let translate_imm6 name value =
8484
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty6_dict (Nat_big_num.of_int value)
85-
85+
8686
let translate_imm5 name value =
8787
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int value)
88-
88+
8989
let translate_imm4 name value =
9090
Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty4_dict (Nat_big_num.of_int value)

‎handwritten_support/hgen/shallow_types_to_herdtools_types.hgen

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(* let translate_out_big_bit = Sail_values.unsigned
2-
*
2+
*
33
* let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
4-
* let translate_out_signed_int inst bits =
4+
* let translate_out_signed_int inst bits =
55
* let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
66
* if (i >= (1 lsl (bits - 1))) then
77
* (i - (1 lsl bits)) else
@@ -68,9 +68,9 @@ let translate_out_amoop op = match op with
6868
| AMOMAXU -> RISCVAMOMAXU
6969

7070
let translate_out_wordWidth op = match op with
71-
| BYTE -> RISCVBYTE
72-
| HALF -> RISCVHALF
73-
| WORD -> RISCVWORD
71+
| BYTE -> RISCVBYTE
72+
| HALF -> RISCVHALF
73+
| WORD -> RISCVWORD
7474
| DOUBLE -> RISCVDOUBLE
7575

7676
let translate_out_bool b = b (* function

‎handwritten_support/hgen/tokens.hgen

+11-11
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
%token <RISCVHGenBase.token_UTYPE> UTYPE
2-
%token <RISCVHGenBase.token_JAL> JAL
3-
%token <RISCVHGenBase.token_JALR> JALR
4-
%token <RISCVHGenBase.token_BType> BTYPE
5-
%token <RISCVHGenBase.token_IType> ITYPE
1+
%token <RISCVHGenBase.token_UTYPE> UTYPE
2+
%token <RISCVHGenBase.token_JAL> JAL
3+
%token <RISCVHGenBase.token_JALR> JALR
4+
%token <RISCVHGenBase.token_BType> BTYPE
5+
%token <RISCVHGenBase.token_IType> ITYPE
66
%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
7-
%token <RISCVHGenBase.token_RTYPE> RTYPE
8-
%token <RISCVHGenBase.token_Load> LOAD
9-
%token <RISCVHGenBase.token_Store> STORE
10-
%token <RISCVHGenBase.token_ADDIW> ADDIW
11-
%token <RISCVHGenBase.token_SHIFTW> SHIFTW
12-
%token <RISCVHGenBase.token_RTYPEW> RTYPEW
7+
%token <RISCVHGenBase.token_RTYPE> RTYPE
8+
%token <RISCVHGenBase.token_Load> LOAD
9+
%token <RISCVHGenBase.token_Store> STORE
10+
%token <RISCVHGenBase.token_ADDIW> ADDIW
11+
%token <RISCVHGenBase.token_SHIFTW> SHIFTW
12+
%token <RISCVHGenBase.token_RTYPEW> RTYPEW
1313
%token <RISCVHGenBase.token_FENCE> FENCE
1414
%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
1515
%token <RISCVHGenBase.token_FENCETSO> FENCETSO

‎handwritten_support/hgen/trans_sail.hgen

+12-12
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,30 @@
11
| `RISCVStopFetching -> ("StopFetching", [], [])
22
| `RISCVThreadStart -> ("ThreadStart", [], [])
33

4-
| `RISCVUTYPE(imm, rd, op) ->
4+
| `RISCVUTYPE(imm, rd, op) ->
55
("UTYPE",
66
[
77
translate_imm20 "imm" imm;
88
translate_reg "rd" rd;
99
translate_uop "op" op;
1010
],
1111
[])
12-
| `RISCVJAL(imm, rd) ->
12+
| `RISCVJAL(imm, rd) ->
1313
("JAL",
1414
[
1515
translate_imm21 "imm" imm;
1616
translate_reg "rd" rd;
1717
],
1818
[])
19-
| `RISCVJALR(imm, rs, rd) ->
19+
| `RISCVJALR(imm, rs, rd) ->
2020
("JALR",
2121
[
2222
translate_imm12 "imm" imm;
2323
translate_reg "rs" rd;
2424
translate_reg "rd" rd;
2525
],
2626
[])
27-
| `RISCVBType(imm, rs2, rs1, op) ->
27+
| `RISCVBType(imm, rs2, rs1, op) ->
2828
("BTYPE",
2929
[
3030
translate_imm13 "imm" imm;
@@ -33,7 +33,7 @@
3333
translate_bop "op" op;
3434
],
3535
[])
36-
| `RISCVIType(imm, rs1, rd, op) ->
36+
| `RISCVIType(imm, rs1, rd, op) ->
3737
("ITYPE",
3838
[
3939
translate_imm12 "imm" imm;
@@ -42,7 +42,7 @@
4242
translate_iop "op" op;
4343
],
4444
[])
45-
| `RISCVShiftIop(imm, rs, rd, op) ->
45+
| `RISCVShiftIop(imm, rs, rd, op) ->
4646
("SHIFTIOP",
4747
[
4848
translate_imm6 "imm" imm;
@@ -51,7 +51,7 @@
5151
translate_sop "op" op;
5252
],
5353
[])
54-
| `RISCVRType (rs2, rs1, rd, op) ->
54+
| `RISCVRType (rs2, rs1, rd, op) ->
5555
("RTYPE",
5656
[
5757
translate_reg "rs2" rs2;
@@ -83,15 +83,15 @@
8383
translate_bool "rl" rl;
8484
],
8585
[])
86-
| `RISCVADDIW(imm, rs, rd) ->
86+
| `RISCVADDIW(imm, rs, rd) ->
8787
("ADDIW",
8888
[
8989
translate_imm12 "imm" imm;
9090
translate_reg "rs" rs;
9191
translate_reg "rd" rd;
9292
],
9393
[])
94-
| `RISCVSHIFTW(imm, rs, rd, op) ->
94+
| `RISCVSHIFTW(imm, rs, rd, op) ->
9595
("SHIFTW",
9696
[
9797
translate_imm5 "imm" imm;
@@ -100,7 +100,7 @@
100100
translate_sop "op" op;
101101
],
102102
[])
103-
| `RISCVRTYPEW(rs2, rs1, rd, op) ->
103+
| `RISCVRTYPEW(rs2, rs1, rd, op) ->
104104
("RTYPEW",
105105
[
106106
translate_reg "rs2" rs2;
@@ -110,11 +110,11 @@
110110
],
111111
[])
112112
| `RISCVFENCE(pred, succ) ->
113-
("FENCE",
113+
("FENCE",
114114
[
115115
translate_imm4 "pred" pred;
116116
translate_imm4 "succ" succ;
117-
],
117+
],
118118
[])
119119
| `RISCVFENCE_TSO(pred, succ) ->
120120
("FENCE_TSO",

‎handwritten_support/hgen/types.hgen

+3-3
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ let pp_riscv_uop = function
1414

1515

1616
type riscvBop = (* branch ops *)
17-
| RISCVBEQ
17+
| RISCVBEQ
1818
| RISCVBNE
1919
| RISCVBLT
2020
| RISCVBGE
@@ -59,7 +59,7 @@ type riscvRop = (* reg-reg ops *)
5959
| RISCVADD
6060
| RISCVSUB
6161
| RISCVSLL
62-
| RISCVSLT
62+
| RISCVSLT
6363
| RISCVSLTU
6464
| RISCVXOR
6565
| RISCVSRL
@@ -93,7 +93,7 @@ let pp_riscv_ropw = function
9393
| RISCVSRLW -> "srlw"
9494
| RISCVSRAW -> "sraw"
9595

96-
type wordWidth =
96+
type wordWidth =
9797
| RISCVBYTE
9898
| RISCVHALF
9999
| RISCVWORD

0 commit comments

Comments
 (0)