From b5c738a143f4b8f202bcd00618faa462a1e8ba07 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Wed, 30 Oct 2024 14:55:27 +0300 Subject: [PATCH 01/12] Parse pseudoinstructions from AST and add to Hashtbl Each entry in the `base_instructions` Hashtbl uses the pseudoinstruction AST key as the key, with the value being a tuple that contains: 1. The base instruction's type. 2. The base instruction's argument list. Each base instruction is stored as its own entry. ``` Adding to hashtable with key: LA, id_inner: UTYPE, args_inner_list: [subrange_bits(imm, 31, 12), rd, RISCV_AUIPC] Adding to hashtable with key: LA, id_inner: ITYPE, args_inner_list: [subrange_bits(imm, 11, 0), reg_name_backwards("x0"), rd, RISCV_ADDI] ``` --- src/sail_json_backend/json.ml | 46 +++++++++++++++++++++++++++++++++-- 1 file changed, 44 insertions(+), 2 deletions(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index ce5cc77e9..d110b5ff3 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -91,6 +91,7 @@ let formats = Hashtbl.create 997 let extensions = Hashtbl.create 997 let mappings = Hashtbl.create 997 let registers = Hashtbl.create 997 +let base_instructions = Hashtbl.create 997 let debug_print ?(printer = prerr_endline) message = if debug_enabled then printer message else () @@ -433,10 +434,51 @@ let parse_funcl fcl = debug_print ("id_of_dependent: " ^ id); let source_code = extract_source_code (Ast_util.exp_loc e) in Hashtbl.add functions id source_code - | Pat_exp (P_aux (P_app (i, pl), _), e) | Pat_when (P_aux (P_app (i, pl), _), e, _) -> + | Pat_exp (P_aux (P_app (i, pl), _), e) | Pat_when (P_aux (P_app (i, pl), _), e, _) -> ( debug_print ("FCL_funcl execute " ^ string_of_id i); let source_code = extract_source_code (Ast_util.exp_loc e) in - Hashtbl.add executes (string_of_id i) source_code + match id with + | "pseudo_of" -> ( + debug_print ("FCL funcl pseudoinstruction " ^ string_of_id i); + match e with + | E_aux (E_list exp_list, _) -> + debug_print ("Exp el: " ^ String.concat ", " (List.map string_of_exp exp_list)); + List.iter + (fun exp -> + match exp with + | E_aux (E_app (id, el), _) -> + List.iter + (fun inner_exp -> + match inner_exp with + | E_aux (E_app (id_inner, el_inner), _) -> + List.iteri + (fun index inner_value -> + match inner_value with + | E_aux (E_tuple tuple_list, _) -> + let args_inner_list = List.map string_of_exp tuple_list in + debug_print + ("Adding to hashtable with key: " ^ string_of_id i ^ ", id_inner: " + ^ string_of_id id_inner ^ ", args_inner_list: [" + ^ String.concat ", " args_inner_list ^ "]" + ); + Hashtbl.add base_instructions (string_of_id i) + (string_of_id id_inner, args_inner_list) + | _ -> () + ) + el_inner + | _ -> () + ) + el + | _ -> () + ) + exp_list + | _ -> () + ) + | "execute" | "pseudo_execute" -> + debug_print ("FCL_funcl execute " ^ string_of_id i); + Hashtbl.add executes (string_of_id i) source_code + | _ -> () + ) | _ -> () end | _ -> debug_print "FCL_funcl other" From 783185ac109113dda605a39f8ce288e6118cd7be Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Tue, 5 Nov 2024 15:08:45 +0300 Subject: [PATCH 02/12] Add function to process base instructions `process_base_instruction` iterates over `base_instructions` Hashtbl and calls `get_mnemonic` for each entry to retrieve its mnemonic. --- src/sail_json_backend/json.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index d110b5ff3..5e61d13ac 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -483,6 +483,18 @@ let parse_funcl fcl = end | _ -> debug_print "FCL_funcl other" +let get_mnemonic id args_list = None + +let process_base_instruction () = + let mnemonics = + Hashtbl.fold + (fun k (id, args_list) acc -> + match get_mnemonic id args_list with Some mnemonic -> mnemonic :: acc | None -> acc + ) + base_instructions [] + in + mnemonics + let json_of_key_operand key op t = "\n{\n" ^ " \"name\": \"" ^ op ^ "\", \"type\": \"" ^ t ^ "\"\n" ^ "}" let json_of_mnemonic m = "\"" ^ m ^ "\"" @@ -833,6 +845,8 @@ let defs { defs; _ } = ) defs; + let mnemonics = process_base_instruction () in + debug_print "TYPES"; Hashtbl.iter (fun k v -> debug_print (k ^ ":" ^ v)) types; debug_print "SIGS"; From 9c62811d7499d08ce0fd9442ff2b5a5652be916e Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Wed, 6 Nov 2024 15:35:40 +0300 Subject: [PATCH 03/12] Add function for mnemonic retrieval `get_mnemonic` retrieves a mnemonic in one of two ways: 1. Parameter extraction: If a parameter exists in the assembly string, it is extracted and mapped to an argument using `map_param_to_arg`. The result is then processed by `map_arg_to_mnemonic` to get the final mnemonic. For example in the assembly string: ``` ITYPE:itype_mnemonic(op), spc, reg_name(rd), sep, reg_name(rs1), sep, hex_bits_signed_12(imm) ``` `op` is mapped to `RISCV_ADDI`, which results in `addi`. 2. Direct mnemonic: If no parameter is found, the mnemonic is directly retrieved from the assembly string and cross-checked against `assembly_clean` Hashtbl for accuracy. Example: ``` C_ZEXT_W:c.zext.w, spc, creg_name(rsdc) ``` Returns: ``` c.zext.w ``` Returns `None` if no mnemonic is found in either path. --- src/sail_json_backend/json.ml | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 5e61d13ac..2ccb2fed7 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -483,7 +483,28 @@ let parse_funcl fcl = end | _ -> debug_print "FCL_funcl other" -let get_mnemonic id args_list = None +let map_arg_to_mnemonic arg id = None + +let map_param_to_arg id param args_list = None + +let get_mnemonic id args_list = + match Hashtbl.find_opt assembly id with + | Some (str :: _) -> + if Str.string_match (Str.regexp ".+(\\(.*\\))") str 0 then ( + let param = Str.matched_group 1 str in + debug_print ("param: " ^ param); + match map_param_to_arg id param args_list with Some arg -> map_arg_to_mnemonic arg id | None -> None + ) + else ( + match Hashtbl.find_opt assembly_clean id with + | Some (mnemonic :: _) when mnemonic = str -> + debug_print ("Mnemonic matched: " ^ str); + Some str + | Some _ -> None + | None -> None + ) + | Some [] -> None + | None -> None let process_base_instruction () = let mnemonics = From dd68065d4413a6a4a1e404bd5314715144cbf2e8 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Mon, 11 Nov 2024 16:27:42 +0300 Subject: [PATCH 04/12] Add function to return matched argument `map_param_to_arg` gets the input list from `inputs` Hashtbl: ``` ITYPE: imm, rs1, rd, op ``` It then finds the index of the parameter (`op` at index 3) and returns the corresponding argument at that index. For example, with `op` at index 3, the function returns `RISCV_ADDI` from the argument list `[subrange_bits(imm, 11, 0), reg_name("x0"), rd, RISCV_ADDI]`. --- src/sail_json_backend/json.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 2ccb2fed7..f78495a3e 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -485,7 +485,14 @@ let parse_funcl fcl = let map_arg_to_mnemonic arg id = None -let map_param_to_arg id param args_list = None +let get_index elem lst = None + +let map_param_to_arg id param args_list = + match Hashtbl.find_opt inputs id with + | Some inputl -> ( + match get_index param inputl with Some index -> List.nth_opt args_list index | None -> None + ) + | None -> None let get_mnemonic id args_list = match Hashtbl.find_opt assembly id with From a81da7f6d5f2d5ddbab7b80af0272e80e60bcf36 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Mon, 11 Nov 2024 17:56:28 +0300 Subject: [PATCH 05/12] Add function to return index of an element in a list --- src/sail_json_backend/json.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index f78495a3e..01b277f8f 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -485,7 +485,8 @@ let parse_funcl fcl = let map_arg_to_mnemonic arg id = None -let get_index elem lst = None +let get_index elem lst = + List.find_map (fun (i, x) -> if x = elem then Some i else None) (List.mapi (fun i x -> (i, x)) lst) let map_param_to_arg id param args_list = match Hashtbl.find_opt inputs id with From 49dd15f22263b0bbee08423d0af4bbf55f4cab0b Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Tue, 12 Nov 2024 14:55:05 +0300 Subject: [PATCH 06/12] Add function to retrieve mnemonic for a given argument `map_arg_to_mnemonic` looks up a list of enum_mnemonic pairs in the `mappings` Hashtbl. It then matches the provided `arg` with the enum and returns the corresponding mnemonic. ``` Matched RISCV_ADDI with mnemonic: addi ``` --- src/sail_json_backend/json.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 01b277f8f..345dc7d1a 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -483,7 +483,16 @@ let parse_funcl fcl = end | _ -> debug_print "FCL_funcl other" -let map_arg_to_mnemonic arg id = None +let map_arg_to_mnemonic arg id = + List.find_map + (fun (enum, mnemonic) -> + if List.hd enum = arg then ( + debug_print ("Matched " ^ List.hd enum ^ " with mnemonic: " ^ List.hd mnemonic); + Some (List.hd mnemonic) + ) + else None + ) + (Hashtbl.find_all mappings (String.lowercase_ascii (id ^ "_mnemonic"))) let get_index elem lst = List.find_map (fun (i, x) -> if x = elem then Some i else None) (List.mapi (fun i x -> (i, x)) lst) From 20cd11cd3303173b4fa690a37d884b77f042022a Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Wed, 20 Nov 2024 13:19:02 +0300 Subject: [PATCH 07/12] Fix misplaced line and adjust list iteration function Move a misplaced line in `parse_funcl` for logical flow. Replace `List.iteri` with `List.iter` for function appropriateness, as index is not used. --- src/sail_json_backend/json.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 345dc7d1a..034a95f56 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -435,8 +435,6 @@ let parse_funcl fcl = let source_code = extract_source_code (Ast_util.exp_loc e) in Hashtbl.add functions id source_code | Pat_exp (P_aux (P_app (i, pl), _), e) | Pat_when (P_aux (P_app (i, pl), _), e, _) -> ( - debug_print ("FCL_funcl execute " ^ string_of_id i); - let source_code = extract_source_code (Ast_util.exp_loc e) in match id with | "pseudo_of" -> ( debug_print ("FCL funcl pseudoinstruction " ^ string_of_id i); @@ -451,8 +449,8 @@ let parse_funcl fcl = (fun inner_exp -> match inner_exp with | E_aux (E_app (id_inner, el_inner), _) -> - List.iteri - (fun index inner_value -> + List.iter + (fun inner_value -> match inner_value with | E_aux (E_tuple tuple_list, _) -> let args_inner_list = List.map string_of_exp tuple_list in @@ -475,6 +473,7 @@ let parse_funcl fcl = | _ -> () ) | "execute" | "pseudo_execute" -> + let source_code = extract_source_code (Ast_util.exp_loc e) in debug_print ("FCL_funcl execute " ^ string_of_id i); Hashtbl.add executes (string_of_id i) source_code | _ -> () From eb4611cbe5183e4ccb2cabc9669fecaf5afb8cf4 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Wed, 20 Nov 2024 13:46:52 +0300 Subject: [PATCH 08/12] Add variable for regex pattern matching the string in parentheses --- src/sail_json_backend/json.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 034a95f56..9ffb661eb 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -504,9 +504,10 @@ let map_param_to_arg id param args_list = | None -> None let get_mnemonic id args_list = + let str_in_parens = Str.regexp ".+(\\(.*\\))" in match Hashtbl.find_opt assembly id with | Some (str :: _) -> - if Str.string_match (Str.regexp ".+(\\(.*\\))") str 0 then ( + if Str.string_match str_in_parens str 0 then ( let param = Str.matched_group 1 str in debug_print ("param: " ^ param); match map_param_to_arg id param args_list with Some arg -> map_arg_to_mnemonic arg id | None -> None From 35af3fda1eb03028a580e76929462ab24128266f Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Wed, 20 Nov 2024 14:24:00 +0300 Subject: [PATCH 09/12] Refactor match expressions to use a catch-all case --- src/sail_json_backend/json.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 9ffb661eb..66147494a 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -517,11 +517,9 @@ let get_mnemonic id args_list = | Some (mnemonic :: _) when mnemonic = str -> debug_print ("Mnemonic matched: " ^ str); Some str - | Some _ -> None - | None -> None + | _ -> None ) - | Some [] -> None - | None -> None + | _ -> None let process_base_instruction () = let mnemonics = From b95e0f23fe8f0484e832267a3141c9b20041f18c Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Thu, 21 Nov 2024 15:31:06 +0300 Subject: [PATCH 10/12] Refactor index search function Update `get_index` to use `List.find_index`, simplifying the implementation while maintaining functionality. --- src/sail_json_backend/json.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 66147494a..3b1bed55d 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -493,8 +493,7 @@ let map_arg_to_mnemonic arg id = ) (Hashtbl.find_all mappings (String.lowercase_ascii (id ^ "_mnemonic"))) -let get_index elem lst = - List.find_map (fun (i, x) -> if x = elem then Some i else None) (List.mapi (fun i x -> (i, x)) lst) +let get_index elem lst = List.find_index (fun x -> x = elem) lst let map_param_to_arg id param args_list = match Hashtbl.find_opt inputs id with From 67fa077c9e988285e7efe075fe26d95fc68984d3 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Thu, 21 Nov 2024 15:50:37 +0300 Subject: [PATCH 11/12] Refactor `map_arg_to_mnemonic` to use direct iteration Replace the key concatenation assumption with a fold over the entire `mappings` Hashtbl, ensuring correctness across all cases. --- src/sail_json_backend/json.ml | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/sail_json_backend/json.ml b/src/sail_json_backend/json.ml index 3b1bed55d..94c4a9e1a 100644 --- a/src/sail_json_backend/json.ml +++ b/src/sail_json_backend/json.ml @@ -482,16 +482,19 @@ let parse_funcl fcl = end | _ -> debug_print "FCL_funcl other" -let map_arg_to_mnemonic arg id = - List.find_map - (fun (enum, mnemonic) -> - if List.hd enum = arg then ( - debug_print ("Matched " ^ List.hd enum ^ " with mnemonic: " ^ List.hd mnemonic); - Some (List.hd mnemonic) - ) - else None +let map_arg_to_mnemonic arg = + Hashtbl.fold + (fun _ (enum, mnemonic) acc -> + match acc with + | Some _ -> acc + | None -> + if List.hd enum = arg then ( + debug_print ("Matched " ^ List.hd enum ^ " with mnemonic: " ^ List.hd mnemonic); + Some (List.hd mnemonic) + ) + else None ) - (Hashtbl.find_all mappings (String.lowercase_ascii (id ^ "_mnemonic"))) + mappings None let get_index elem lst = List.find_index (fun x -> x = elem) lst @@ -509,7 +512,7 @@ let get_mnemonic id args_list = if Str.string_match str_in_parens str 0 then ( let param = Str.matched_group 1 str in debug_print ("param: " ^ param); - match map_param_to_arg id param args_list with Some arg -> map_arg_to_mnemonic arg id | None -> None + match map_param_to_arg id param args_list with Some arg -> map_arg_to_mnemonic arg | None -> None ) else ( match Hashtbl.find_opt assembly_clean id with From e2799d927835d9fbef9d72ef3f6d0abc70b83c17 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Tue, 26 Nov 2024 15:40:43 +0300 Subject: [PATCH 12/12] Remove pkg-config from macOS dependencies --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index b82b4d36d..631773581 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -28,7 +28,7 @@ jobs: - name: System dependencies (macOS) if: startsWith(matrix.os, 'macOS') run: | - brew install gpatch gmp z3 pkg-config lzlib zlib opam + brew install gpatch gmp z3 lzlib zlib opam - name: Restore cached opam id: cache-opam-restore