Skip to content

Commit

Permalink
adding CI 32
Browse files Browse the repository at this point in the history
  • Loading branch information
moste00 committed Aug 24, 2024
1 parent 8413f2d commit 4742079
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 42 deletions.
12 changes: 9 additions & 3 deletions bin/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ open Type_check
open Ast
open Riscv_disasm_from_sail
open Constants
open Printexc

let write_c_file ?(optional_includes = []) name code =
let oc = open_out name in
Expand All @@ -17,9 +18,11 @@ let write_c_file ?(optional_includes = []) name code =
Printf.fprintf oc "%s" code;
close_out oc

let sailpath = (Unix.getenv "HOME") ^ "/.opam/default/share/sail/"
let sailpath = Unix.getenv "HOME" ^ "/.opam/default/share/sail/"

let () = print_endline ("\n\n SAIL STDLIB PATH : " ^ sailpath ^ " \n-------------------\n")
let () =
print_endline
("\n\n SAIL STDLIB PATH : " ^ sailpath ^ " \n-------------------\n")

let paths_filename = ref ""

Expand Down Expand Up @@ -63,7 +66,10 @@ let dummyoptions =
]

let ast, types, side_effects =
Frontend.load_files sailpath dummyoptions initial_typeenv filepaths
try Frontend.load_files sailpath dummyoptions initial_typeenv filepaths
with Reporting.Fatal_error e as ex ->
Reporting.print_error e;
raise ex

let ctypedefs, typdefwalker = Gen_clike_typedef.gen_def ast

Expand Down
13 changes: 10 additions & 3 deletions lib/gen_clike_typedef.ml
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,8 @@ let set_walker_case walker case =
walker.curr_case <- String.lowercase_ascii case;
walker.curr_case_remaining_member <-
Hashtbl.find walker.case_names_to_member_names walker.curr_case;
walker.curr_case_is_primitive <- set_contains walker.primitive_cases walker.curr_case;
walker.curr_case_is_primitive <-
set_contains walker.primitive_cases walker.curr_case;
walker.curr_primitive_case_already_walked <- false;
ast_sail_def_name ^ generated_ast_enum_suffix

Expand All @@ -213,14 +214,20 @@ let walk walker =
if walker.curr_primitive_case_already_walked then None
else (
walker.curr_primitive_case_already_walked <- true;
Some (ast_sail_def_name ^ generated_ast_payload_suffix ^ "." ^ walker.curr_case)
Some
(ast_sail_def_name ^ generated_ast_payload_suffix ^ "."
^ walker.curr_case
)
)
else (
match walker.curr_case_remaining_member with
| [] -> None
| next :: rest ->
walker.curr_case_remaining_member <- rest;
Some (ast_sail_def_name ^ generated_ast_payload_suffix ^ "." ^ walker.curr_case ^ "." ^ next)
Some
(ast_sail_def_name ^ generated_ast_payload_suffix ^ "."
^ walker.curr_case ^ "." ^ next
)
)

let gen_def ast =
Expand Down
3 changes: 1 addition & 2 deletions lib/gen_decoder.ml
Original file line number Diff line number Diff line change
Expand Up @@ -387,8 +387,7 @@ let create_conditions state r arg_bindings =
Bind (size, idstr)
| MP_lit lit ->
let const = bitv_literal_to_str lit in
let size = bitv_literal_size lit
in
let size = bitv_literal_size lit in
Assert (size, const)
| MP_app (id, args) -> (
let mapping_name = id_to_str id in
Expand Down
64 changes: 36 additions & 28 deletions lib/sail_ast_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -57,51 +57,59 @@ let sail_bitv_size_to_int =
let sail_bitv_size_to_int_noexn =
convert_bitv_size_to_int ~throw_on_unsupported_size_exprs:false

let binary_chars_to_hex_digit b3 b2 b1 b0 =
match (b3, b2, b1, b0) with
| ('0', '0', '0', '0') -> "0"
| ('0', '0', '0', '1') -> "1"
| ('0', '0', '1', '0') -> "2"
| ('0', '0', '1', '1') -> "3"
| ('0', '1', '0', '0') -> "4"
| ('0', '1', '0', '1') -> "5"
| ('0', '1', '1', '0') -> "6"
| ('0', '1', '1', '1') -> "7"
| ('1', '0', '0', '0') -> "8"
| ('1', '0', '0', '1') -> "9"
| ('1', '0', '1', '0') -> "A"
| ('1', '0', '1', '1') -> "B"
| ('1', '1', '0', '0') -> "C"
| ('1', '1', '0', '1') -> "D"
| ('1', '1', '1', '0') -> "E"
| ('1', '1', '1', '1') -> "F"
let binary_chars_to_hex_digit b3 b2 b1 b0 =
match (b3, b2, b1, b0) with
| '0', '0', '0', '0' -> "0"
| '0', '0', '0', '1' -> "1"
| '0', '0', '1', '0' -> "2"
| '0', '0', '1', '1' -> "3"
| '0', '1', '0', '0' -> "4"
| '0', '1', '0', '1' -> "5"
| '0', '1', '1', '0' -> "6"
| '0', '1', '1', '1' -> "7"
| '1', '0', '0', '0' -> "8"
| '1', '0', '0', '1' -> "9"
| '1', '0', '1', '0' -> "A"
| '1', '0', '1', '1' -> "B"
| '1', '1', '0', '0' -> "C"
| '1', '1', '0', '1' -> "D"
| '1', '1', '1', '0' -> "E"
| '1', '1', '1', '1' -> "F"
| _ -> failwith "UNREACHABLE"

let binary_str_to_hex_str s =
let binary_str_to_hex_str s =
let slen = String.length s in
let slen_mod4 = slen mod 4 in
let padding = if slen_mod4 = 0 then "" else List.init (4 - slen_mod4) (fun _ -> "0") |> String.concat "" in
let s_padded_4 = padding ^ s in
let padding =
if slen_mod4 = 0 then ""
else List.init (4 - slen_mod4) (fun _ -> "0") |> String.concat ""
in
let s_padded_4 = padding ^ s in
let padlen = String.length s_padded_4 in
let hexstr = Buffer.create (padlen/4) in
let hexstr = Buffer.create (padlen / 4) in
let i = ref 0 in
while !i < padlen do
let hex_digit = binary_chars_to_hex_digit s_padded_4.[!i] s_padded_4.[!i+1] s_padded_4.[!i+2] s_padded_4.[!i+3] in
let hex_digit =
binary_chars_to_hex_digit s_padded_4.[!i]
s_padded_4.[!i + 1]
s_padded_4.[!i + 2]
s_padded_4.[!i + 3]
in
Buffer.add_string hexstr hex_digit;
i := !i + 4
done;
Buffer.contents hexstr

let bitv_literal_to_str bitv_lit =
let (L_aux (lit, _)) = bitv_lit in
match lit with
| L_hex lit_str -> "0x" ^ lit_str
| L_bin lit_str -> "0x" ^ (binary_str_to_hex_str lit_str)
| L_bin lit_str -> "0x" ^ binary_str_to_hex_str lit_str
| _ -> failwith "Expected a bitvec literal, found neither L_hex nor L_bin"

let bitv_literal_size bitv_lit =
let bitv_literal_size bitv_lit =
let (L_aux (lit, _)) = bitv_lit in
match lit with
| L_hex lit_str -> (String.length lit_str) * 4
| L_hex lit_str -> String.length lit_str * 4
| L_bin lit_str -> String.length lit_str
| _ -> failwith "Expected a bitvec literal, found neither L_hex nor L_bin"
| _ -> failwith "Expected a bitvec literal, found neither L_hex nor L_bin"
13 changes: 7 additions & 6 deletions lib/stringify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ let rec stringify_stmt ?(indentation_lvl = 0) str_state stmt =
| Set_ast_case case ->
let case_setter_path = set_walker_case str_state.typedef_walker case in
ind ^ ast_c_parameter ^ "->" ^ case_setter_path ^ " = " ^ case ^ " ;\n"
| Set_ast_next_case_member member_rhs ->
| Set_ast_next_case_member member_rhs -> (
let rhs_string =
match member_rhs with
| Val v -> (
Expand All @@ -190,11 +190,12 @@ let rec stringify_stmt ?(indentation_lvl = 0) str_state stmt =
)
| Exp bv_expr -> stringify_bv str_state bv_expr
in
(match (walk str_state.typedef_walker) with
| Some (setter_path) -> ind ^ ast_c_parameter ^ "->"
^ setter_path
^ " = " ^ rhs_string ^ ";\n"
| None -> failwith "Error assigning to an ast member")
match walk str_state.typedef_walker with
| Some setter_path ->
ind ^ ast_c_parameter ^ "->" ^ setter_path ^ " = " ^ rhs_string
^ ";\n"
| None -> failwith "Error assigning to an ast member"
)
| Ret_ast -> ind ^ "return " ^ ";\n"
| Block stmts ->
String.concat ""
Expand Down

0 comments on commit 4742079

Please sign in to comment.