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.
kolusas · Jun 15, 2023 · 2ede5ef · 2ede5ef
1 parent 33ef4a3
commit 2ede5ef
Show file tree

Hide file tree

Showing 28 changed files with 115 additions and 115 deletions.
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -6,6 +6,12 @@ repos:
     rev: v3.2.0
     hooks:
     -   id: trailing-whitespace
+        # Do not strip trailing whitespace from patches or SVG images.
+        # TODO: the objdump outputs should probably not be part of the repo.
+        exclude: '.*\.(diff|dump|patch|svg)'
     -   id: end-of-file-fixer
+        # Do not strip trailing newlines from patches or SVG images.
+        # TODO: the objdump outputs should probably not be part of the repo.
+        exclude: '.*\.(diff|dump|patch|svg)'
     -   id: check-yaml
     -   id: check-added-large-files
diff --git a/LICENCE b/LICENCE
@@ -16,8 +16,8 @@ Copyright (c) 2017-2023
   Shaked Flur
   Christopher Pulte
   Peter Sewell
-  Alexander Richardson 
-  Hesham Almatary 
+  Alexander Richardson
+  Hesham Almatary
   Jessica Clarke
   Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo
   Peter Rugg

diff --git a/README.md b/README.md
@@ -12,7 +12,7 @@ coverage of the prose RISC-V specification is summarized
 [here](doc/Status.md).
 A [reading guide](doc/ReadingGuide.md) to the model is provided in the
 [doc/](doc/) subdirectory, along with a guide on [how to
-extend](doc/ExtendingGuide.md) the model. 
+extend](doc/ExtendingGuide.md) the model.
 
 
 Latex definitions can be generated from the model that are suitable
@@ -23,7 +23,7 @@ specifications that include the Sail formal definitions are available
 in the sail branch of this [risc-v-isa-manual repository](https://github.com/rems-project/riscv-isa-manual/tree/sail).
 The process to perform this inclusion is explained [here](https://github.com/rems-project/riscv-isa-manual/blob/sail/README.SAIL).
 
-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 
+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
 [RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review).
 
 
@@ -35,16 +35,16 @@ What is Sail?
 engineer-friendly, vendor-pseudocode-like language for describing
 instruction semantics. It is essentially a first-order imperative
 language, but with lightweight dependent typing for numeric types and
-bitvector lengths, which are automatically checked using Z3. 
+bitvector lengths, which are automatically checked using Z3.
 <p>
 
 Given a Sail definition, the tool will type-check it and generate
 LaTeX snippets to use in documentation, executable emulators (in C and OCaml), theorem-prover definitions for
-Isabelle, HOL4, and Coq, and definitions to integrate with our 
+Isabelle, HOL4, and Coq, and definitions to integrate with our
 <a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a>
 and
 <a href="isla-axiomatic.cl.cam.ac.uk/">isla-axiomatic</a> tools for
-concurrency semantics.  
+concurrency semantics.
 <p>
 
   <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)
                       <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
 ~~~~~~
 
-### SRET 
+### SRET
 
 ~~~~~
 union clause ast = SRET : unit
@@ -357,7 +357,7 @@ For booting operating system images, see the information under the
 ### Using development versions of Sail
 
 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.
-                        
+
 Licence
 -------
 
@@ -368,7 +368,7 @@ Authors
 -------
 
  Prashanth Mundkur, SRI International;
- Rishiyur S. Nikhil (Bluespec Inc.); 
+ Rishiyur S. Nikhil (Bluespec Inc.);
  Jon French, University of Cambridge;
  Brian Campbell, University of Edinburgh;
  Robert Norton-Wright, University of Cambridge and Microsoft;

diff --git a/build_simulators.sh b/build_simulators.sh
@@ -15,4 +15,3 @@ test_build make ARCH=RV64 ocaml_emulator/riscv_ocaml_sim_RV64
 
 test_build make ARCH=RV32 c_emulator/riscv_sim_RV32
 test_build make ARCH=RV64 c_emulator/riscv_sim_RV64
-
diff --git a/doc/Status.md b/doc/Status.md
@@ -19,7 +19,7 @@ The Sail specification currently captures the following ISA features:
 
 - Physical Memory Protection (PMP)
 
-For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the 
+For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the
 RMEM tool](https://github.com/rems-project/rmem).
 
 The Sail specification is parameterized over the following

diff --git a/doc/notes_FD_extensions.md b/doc/notes_FD_extensions.md
@@ -14,7 +14,7 @@ This will be merged back into the main original repo after testing.
 Status (2019-10-24)
 -------------------
 
-1. Complete (almost): SAIL coding [Rishiyur Nikhil, Bluespec, Inc.]  
+1. Complete (almost): SAIL coding [Rishiyur Nikhil, Bluespec, Inc.]
    Remaining: tweaks to handle illegal rounding modes.
 2. In progress: Incorporate Berkeley SoftFloat calls [U.Cambridge]
 3. To do: Testing on all ISA tests

diff --git a/etc/headache_config b/etc/headache_config
@@ -4,4 +4,3 @@
 |  ".*\\.thy"      -> frame open:"(*" line:"=" close:"*)"
 |  ".*\\.sml"      -> frame open:"(*" line:"=" close:"*)"
 |  ".*\\.sail"   -> frame open:"/*" line:"=" close:"*/"
-
diff --git a/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen b/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen
@@ -59,9 +59,9 @@ let translate_amoop op = match op with
   | RISCVAMOMAXU -> AMOMAXU
 
 let translate_wordWidth op = match op with
-  | RISCVBYTE   -> BYTE  
-  | RISCVHALF   -> HALF  
-  | RISCVWORD   -> WORD  
+  | RISCVBYTE   -> BYTE
+  | RISCVHALF   -> HALF
+  | RISCVWORD   -> WORD
   | RISCVDOUBLE -> DOUBLE
 
 let translate_bool name b = b (* function
@@ -70,21 +70,21 @@ let translate_bool name b = b (* function
 
 let translate_imm21 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty21_dict (Nat_big_num.of_int value)
-  
-let translate_imm20 name value = 
+
+let translate_imm20 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty20_dict (Nat_big_num.of_int value)
-  
+
 let translate_imm13 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty13_dict (Nat_big_num.of_int value)
-  
+
 let translate_imm12 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty12_dict (Nat_big_num.of_int value)
-  
+
 let translate_imm6 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty6_dict (Nat_big_num.of_int value)
-  
+
 let translate_imm5 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int value)
-  
+
 let translate_imm4 name value =
   Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty4_dict (Nat_big_num.of_int value)
diff --git a/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen b/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen
@@ -1,7 +1,7 @@
 (* let translate_out_big_bit = Sail_values.unsigned
- * 
+ *
  * let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
- * let translate_out_signed_int inst bits = 
+ * let translate_out_signed_int inst bits =
  *     let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
  *     if (i >= (1 lsl (bits - 1))) then
  *     (i - (1 lsl bits)) else
@@ -68,9 +68,9 @@ let translate_out_amoop op = match op with
   | AMOMAXU -> RISCVAMOMAXU
 
 let translate_out_wordWidth op = match op with
-  | BYTE   -> RISCVBYTE  
-  | HALF   -> RISCVHALF  
-  | WORD   -> RISCVWORD  
+  | BYTE   -> RISCVBYTE
+  | HALF   -> RISCVHALF
+  | WORD   -> RISCVWORD
   | DOUBLE -> RISCVDOUBLE
 
 let translate_out_bool b = b (* function

diff --git a/handwritten_support/hgen/tokens.hgen b/handwritten_support/hgen/tokens.hgen
@@ -1,15 +1,15 @@
-%token <RISCVHGenBase.token_UTYPE>    UTYPE   
-%token <RISCVHGenBase.token_JAL>      JAL     
-%token <RISCVHGenBase.token_JALR>     JALR    
-%token <RISCVHGenBase.token_BType>    BTYPE   
-%token <RISCVHGenBase.token_IType>    ITYPE   
+%token <RISCVHGenBase.token_UTYPE>    UTYPE
+%token <RISCVHGenBase.token_JAL>      JAL
+%token <RISCVHGenBase.token_JALR>     JALR
+%token <RISCVHGenBase.token_BType>    BTYPE
+%token <RISCVHGenBase.token_IType>    ITYPE
 %token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
-%token <RISCVHGenBase.token_RTYPE>    RTYPE   
-%token <RISCVHGenBase.token_Load>     LOAD    
-%token <RISCVHGenBase.token_Store>    STORE   
-%token <RISCVHGenBase.token_ADDIW>    ADDIW   
-%token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
-%token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
+%token <RISCVHGenBase.token_RTYPE>    RTYPE
+%token <RISCVHGenBase.token_Load>     LOAD
+%token <RISCVHGenBase.token_Store>    STORE
+%token <RISCVHGenBase.token_ADDIW>    ADDIW
+%token <RISCVHGenBase.token_SHIFTW>   SHIFTW
+%token <RISCVHGenBase.token_RTYPEW>   RTYPEW
 %token <RISCVHGenBase.token_FENCE>    FENCE
 %token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
 %token <RISCVHGenBase.token_FENCETSO> FENCETSO

diff --git a/handwritten_support/hgen/trans_sail.hgen b/handwritten_support/hgen/trans_sail.hgen
@@ -1,30 +1,30 @@
 | `RISCVStopFetching -> ("StopFetching", [], [])
 | `RISCVThreadStart  -> ("ThreadStart", [], [])
 
-| `RISCVUTYPE(imm, rd, op) -> 
+| `RISCVUTYPE(imm, rd, op) ->
     ("UTYPE",
       [
       translate_imm20 "imm" imm;
       translate_reg "rd" rd;
       translate_uop "op" op;
        ],
       [])
-| `RISCVJAL(imm, rd) -> 
+| `RISCVJAL(imm, rd) ->
    ("JAL",
     [
       translate_imm21 "imm" imm;
       translate_reg "rd" rd;
     ],
     [])
-| `RISCVJALR(imm, rs, rd) -> 
+| `RISCVJALR(imm, rs, rd) ->
    ("JALR",
     [
       translate_imm12 "imm" imm;
       translate_reg "rs" rd;
       translate_reg "rd" rd;
     ],
     [])
-| `RISCVBType(imm, rs2, rs1, op)  -> 
+| `RISCVBType(imm, rs2, rs1, op)  ->
    ("BTYPE",
     [
       translate_imm13 "imm" imm;
@@ -33,7 +33,7 @@
       translate_bop "op" op;
     ],
     [])
-| `RISCVIType(imm, rs1, rd, op)  -> 
+| `RISCVIType(imm, rs1, rd, op)  ->
    ("ITYPE",
     [
       translate_imm12 "imm" imm;
@@ -42,7 +42,7 @@
       translate_iop "op" op;
     ],
     [])
-| `RISCVShiftIop(imm, rs, rd, op) -> 
+| `RISCVShiftIop(imm, rs, rd, op) ->
    ("SHIFTIOP",
     [
       translate_imm6 "imm" imm;
@@ -51,7 +51,7 @@
       translate_sop "op" op;
     ],
     [])
-| `RISCVRType (rs2, rs1, rd, op)  -> 
+| `RISCVRType (rs2, rs1, rd, op)  ->
    ("RTYPE",
     [
       translate_reg "rs2" rs2;
@@ -83,15 +83,15 @@
       translate_bool "rl" rl;
     ],
     [])
-| `RISCVADDIW(imm, rs, rd)        -> 
+| `RISCVADDIW(imm, rs, rd)        ->
    ("ADDIW",
     [
       translate_imm12 "imm" imm;
       translate_reg "rs" rs;
       translate_reg "rd" rd;
     ],
     [])
-| `RISCVSHIFTW(imm, rs, rd, op)   -> 
+| `RISCVSHIFTW(imm, rs, rd, op)   ->
    ("SHIFTW",
     [
       translate_imm5 "imm" imm;
@@ -100,7 +100,7 @@
       translate_sop "op" op;
     ],
     [])
-| `RISCVRTYPEW(rs2, rs1, rd, op)  -> 
+| `RISCVRTYPEW(rs2, rs1, rd, op)  ->
    ("RTYPEW",
     [
       translate_reg "rs2" rs2;
@@ -110,11 +110,11 @@
     ],
     [])
 | `RISCVFENCE(pred, succ) ->
-  ("FENCE", 
+  ("FENCE",
   [
      translate_imm4 "pred" pred;
      translate_imm4 "succ" succ;
-  ], 
+  ],
   [])
 | `RISCVFENCE_TSO(pred, succ) ->
   ("FENCE_TSO",

diff --git a/handwritten_support/hgen/types.hgen b/handwritten_support/hgen/types.hgen
@@ -14,7 +14,7 @@ let pp_riscv_uop = function
 
 
 type riscvBop =  (* branch ops *)
-| RISCVBEQ 
+| RISCVBEQ
 | RISCVBNE
 | RISCVBLT
 | RISCVBGE
@@ -59,7 +59,7 @@ type riscvRop = (* reg-reg ops *)
 | RISCVADD
 | RISCVSUB
 | RISCVSLL
-| RISCVSLT 
+| RISCVSLT
 | RISCVSLTU
 | RISCVXOR
 | RISCVSRL
@@ -93,7 +93,7 @@ let pp_riscv_ropw = function
 | RISCVSRLW -> "srlw"
 | RISCVSRAW -> "sraw"
 
-type wordWidth = 
+type wordWidth =
   | RISCVBYTE
   | RISCVHALF
   | RISCVWORD
Original file line number	Diff line number	Diff line change
Expand Up		@@ -15,4 +15,3 @@ test_build make ARCH=RV64 ocaml_emulator/riscv_ocaml_sim_RV64

		test_build make ARCH=RV32 c_emulator/riscv_sim_RV32
		test_build make ARCH=RV64 c_emulator/riscv_sim_RV64
Original file line number	Diff line number	Diff line change
Expand Up		@@ -4,4 +4,3 @@
		\| ".\\.thy" -> frame open:"(" line:"=" close:"*)"
		\| ".\\.sml" -> frame open:"(" line:"=" close:"*)"
		\| ".\\.sail" -> frame open:"/" line:"=" close:"*/"