Mega commit that introduce massive changes, most notably a Sail versi…

…on upgrade - necessary because the riscv model repo upgraded and no longer compiles with the older sail version - and the generation of compiling assembly (ast->str) code

Additionally, the following were done:

1- Code gen no longer handles indentation, but generates minified C and assumes an external formatting pass

2- As part of making the generated assembly code compile, several hand-written helpers were implemented to simplify the generator and avoid having to understand arbitrary Sail functions and mappings

3- As part of making the generated assembly code compiles, tostr logic clauses identify their arguments by index, not by name (because the name might differ in the assembly clause from the canonical name introduced by the execute function in the ast)

4- The CI was updated to install and run clang-format, but it will still be updated in the coming versions to compare the assembly code (it can't compare now as there is no old committed code to compare against)

.github/workflows/end2end-smoke-test.yml

@@ -33,9 +33,9 @@ jobs:
               run: |
                 cd generator && source ~/.bash_profile
                 export OPAMCONFIRMLEVEL=yes
-
+                opam update
                 opam install . --deps-only
-                opam install sail=0.17.1
+                opam install sail=0.18
                 sudo apt-get install z3
 
             - name: Running the generator
@@ -44,16 +44,25 @@ jobs:
                 mv riscv_disasm old_output
 
                 dune exec --profile release -- riscv_disasm_from_sail -f sail.filepaths.txt
+            
+            - name: Installing clang-format to automatically format the source code
+              run: |
+                python -m pip install clang-format
 
             - name: Checking the generated code compiles and is identical to the committed generated code
               run: |
                 cd generator/riscv_disasm
+                
                 touch test_main.c
                 echo '#include "riscv_decode.gen.inc"' >> test_main.c 
                 echo >> test_main.c
+                echo '#include "riscv_ast2str.gen.inc"' >> test_main.c
+                echo >> test_main.c
                 echo 'void main() {}' >> test_main.c
 
                 gcc test_main.c || { echo "Failure: Trying to compile the tool-generated C code failed."; exit 1; }
+                
+                clang-format -i *
 
                 if diff -q riscv_ast.gen.inc ../old_output/riscv_ast.gen.inc > /dev/null 2>&1; then
                   if diff -q riscv_decode.gen.inc ../old_output/riscv_decode.gen.inc > /dev/null 2>&1; then

bin/main.ml

@@ -17,20 +17,20 @@ let write_c_file ?(additional_includes = []) name code =
   in
   let include_string = mk_include_lines Constants.includes in
   let additional_includes_string = mk_include_lines additional_includes in
+  let name_no_dots = String.map (fun c -> if c = '.' then '_' else c) name in
+  Printf.fprintf oc "%s"
+    ("#ifndef __" ^ String.capitalize_ascii name_no_dots ^ "__\n");
+  Printf.fprintf oc "%s"
+    ("#define __" ^ String.capitalize_ascii name_no_dots ^ "__\n");
   Printf.fprintf oc "%s" include_string;
   Printf.fprintf oc "%s" additional_includes_string;
   Printf.fprintf oc "%s" "\n\n";
   Printf.fprintf oc "%s" code;
+  Printf.fprintf oc "%s" "\n\n #endif\n";
   close_out oc
 
 let sailpath = Unix.getenv "HOME" ^ "/.opam/default/share/sail/"
 
-let () =
-  print_endline
-    ("\n-------------------\n SAIL STDLIB PATH : " ^ sailpath
-   ^ " \n-------------------\n"
-    )
-
 let paths_filename = ref ""
 
 let usage_msg = "Usage: riscv_disasm_from_sail -f <path-to-list-of-input-files>"
@@ -72,7 +72,7 @@ let dummyoptions =
     ("-coq_extern_type", Arg.String (fun _ -> ()), "");
   ]
 
-let ast, types, side_effects =
+let _, ast, types, side_effects =
   try Frontend.load_files sailpath dummyoptions initial_typeenv filepaths
   with Reporting.Fatal_error e as ex ->
     Reporting.print_error e;
@@ -90,7 +90,16 @@ let proc_dec = Gen_decoder.gen_decode_proc dec
 
 let proc_dec_str = Stringify.stringify_decode_procedure proc_dec typdefwalker
 
+let asm = Gen_assembler.gen_asm ast analysis
+
+let asm_str = Stringify.stringify_assembler asm typdefwalker
+
 let () = write_c_file Constants.ast_type_filename ctypedefs_str
 let () =
   write_c_file Constants.decode_logic_filename proc_dec_str
     ~additional_includes:["\"" ^ Constants.ast_type_filename ^ "\""]
+
+let () =
+  write_c_file Constants.assembler_filename asm_str
+    ~additional_includes:
+      ["\"" ^ Constants.ast_type_filename ^ "\""; "\"riscv_helpers_ast2str.h\""]

dune-project

@@ -19,7 +19,7 @@
  (name riscv_disasm_from_sail)
  (synopsis "A short synopsis")
  (description "A longer description")
- (depends ocaml dune (libsail (= 0.17.1)))
+ (depends ocaml dune (libsail (= 0.18.0)))
  (tags
   (topics "to describe" your project)))
 

lib/assembler.ml

@@ -1,15 +1,27 @@
-open Common_types
+open Sail_values
 
-type case_id = string
+type case_name = string
+
+type bv_lit_xor_arg_idx =
+  | Bv_lit of string * int (* bitv size of literal *)
+  | Arg_idx of int * int (* bitv size of arg *)
+
+type intrinsic_logic_arg =
+  | Arg_index of int
+  | Bv_concat of bv_lit_xor_arg_idx list
 
 type tostr_logic =
   | Lit of string
-  | Bitv2Str of string * bv2str_table
-  | Enum2Str of string * enum2str_table
-  | Bool2Str of string * bool2str_table
-  | Struct2str of string * string * struct2str_table
-  | Intrinsic_tostr_logic of string * string list
+  | Bitv2Str of int * bv2str_table
+  | Enum2Str of int * enum2str_table
+  | Bool2Str of int * bool2str_table
+  | Struct2str of int * struct2str_table
+  | Intrinsic_tostr_logic of string * intrinsic_logic_arg list
+
+type subcase_condition = (int * string) option
+
+type subcase = subcase_condition * tostr_logic list
 
-type assembler_clause = case_id * tostr_logic list
+type assembler_clause = case_name * subcase list
 
 type assembler = assembler_clause list

lib/constants.ml

@@ -12,10 +12,14 @@ let ast_c_parameter = "tree"
 
 let binary_stream_c_parameter = "binary_stream"
 
-let includes = ["<stdint.h>"]
+let includes = ["<stdint.h>"; "<stddef.h>"; "<string.h>"]
 
 let ast_type_filename = "riscv_ast.gen.inc"
 
 let decode_logic_filename = "riscv_decode.gen.inc"
 
 let identifier_prefix = "RISCV_"
+
+let ast_assembly_mapping = "assembly"
+
+let assembler_filename = "riscv_ast2str.gen.inc"

lib/decode_procedure.ml

@@ -1,4 +1,4 @@
-open Common_types
+open Sail_values
 open Decoder
 
 type bv_val = string

lib/decoder.ml

@@ -72,7 +72,7 @@
         Each decoder is effectively a little program in a domain-specific declarative language.
         The language is a rule-based one where each program is simply a table of rules describing
         under what condition a certain action should be taken. *)
-open Common_types
+open Sail_values
 
 type len = int