tightened the interface of the analysis pass via an mli file to 4 loo…

…kup functions, and refactored some general utils out of sail_ast_utils into their own file

lib/gen_clike_typedef.ml

@@ -1,6 +1,7 @@
 open Sail_ast_processor
 open Sail_ast_foreach
 open Sail_ast_utils
+open Utils
 
 open Libsail
 open Ast

lib/gen_decoder.ml

@@ -1,6 +1,7 @@
 open Sail_ast_foreach
 open Sail_ast_processor
 open Sail_ast_utils
+open Utils
 open Constants
 open Common_types
 open Decoder
@@ -58,22 +59,6 @@ let bind_args_and_create_consequences state l =
       match pat with
       | MP_app (union_case_id, union_case_args) ->
           let case_name = id_to_str union_case_id in
-          let arg_types =
-            Hashtbl.find state.analysis.type_ctx.union_case_to_arg_types
-              case_name
-          in
-          let arg_sizes =
-            List.map
-              (fun arg ->
-                match arg with
-                | Named_type name -> (
-                    try Hashtbl.find state.analysis.type_ctx.bitv_synonyms name
-                    with Not_found -> -1
-                  )
-                | Bitvec size -> size
-              )
-              arg_types
-          in
           let bodies =
             match union_case_args with
             | [MP_aux (MP_lit (L_aux (L_unit, _)), _)] -> []
@@ -85,7 +70,9 @@ let bind_args_and_create_consequences state l =
                     | MP_lit lit -> lit_to_consequence_body lit
                     | MP_id id ->
                         let n = id_to_str id in
-                        let bitv_size = List.nth arg_sizes i in
+                        let bitv_size =
+                          get_case_arg_size state.analysis case_name i
+                        in
                         Hashtbl.add bindings n bitv_size;
                         idstr_to_consequence_body n
                     | MP_vector_concat slices ->
@@ -119,7 +106,8 @@ let create_conditions state r arg_bindings =
               match pat with
               | MP_id id ->
                   let idstr = id_to_str id in
-                  let size = Hashtbl.find arg_bindings idstr in
+                  let maybe_size = Hashtbl.find arg_bindings idstr in
+                  let size = get_some_or_failwith maybe_size "UNREACHABLE" in
                   Bind (size, idstr)
               | MP_typ (pat, typ) ->
                   let size =
@@ -128,15 +116,13 @@ let create_conditions state r arg_bindings =
                       when id_to_str id = "bitvector" || id_to_str id = "bits"
                       ->
                         sail_bitv_size_to_int (List.nth args 0)
-                    | Typ_aux (Typ_id id, _) -> (
-                        try
-                          Hashtbl.find state.analysis.type_ctx.bitv_synonyms
-                            (id_to_str id)
-                        with Not_found ->
-                          failwith
-                            "Type annotation is a named type not synonymous \
-                             with bitvec "
-                      )
+                    | Typ_aux (Typ_id id, _) ->
+                        let sz =
+                          get_size_of_bv_synonym state.analysis (id_to_str id)
+                        in
+                        get_some_or_failwith sz
+                          "Type annotation is a named type not synonymous with \
+                           bitvec "
                     | _ ->
                         failwith
                           ("Type annotation cant be non-bitvec @ "
@@ -163,22 +149,33 @@ let create_conditions state r arg_bindings =
                           "Unsupported mapping pattern, multiple arguments are \
                            not supported"
                   in
-                  try
-                    let bv_to_enum =
-                      Hashtbl.find
-                        state.analysis.mapping_ctx.enum_bitv_mappings_registery
-                        mapping_name
-                    in
-                    let size = Hashtbl.find arg_bindings arg_name in
-                    Map_bind (size, bv_to_enum, arg_name)
-                  with Not_found ->
-                    let struct_name, bv_to_struct =
-                      Hashtbl.find
-                        state.analysis.mapping_ctx
-                          .struct_bitv_mappings_registery mapping_name
-                    in
-                    let size = Hashtbl.find arg_bindings arg_name in
-                    Struct_map_bind (size, struct_name, bv_to_struct, arg_name)
+                  let bv_to_enum =
+                    get_bv2enum_mapping state.analysis mapping_name
+                  in
+                  match bv_to_enum with
+                  | Some bv2enum ->
+                      let maybe_size = Hashtbl.find arg_bindings arg_name in
+                      let size =
+                        get_some_or_failwith maybe_size "UNREACHABLE"
+                      in
+                      Map_bind (size, bv2enum, arg_name)
+                  | None -> (
+                      match
+                        get_bv2struct_mapping state.analysis mapping_name
+                      with
+                      | Some (struct_name, bv_to_struct) ->
+                          let maybe_size = Hashtbl.find arg_bindings arg_name in
+                          let size =
+                            get_some_or_failwith maybe_size "UNREACHABLE"
+                          in
+                          Struct_map_bind
+                            (size, struct_name, bv_to_struct, arg_name)
+                      | None ->
+                          failwith
+                            ("Mapping " ^ mapping_name
+                           ^ " is neither a bv<->enum nor a bv<->struct mapping"
+                            )
+                    )
                 )
               | _ -> failwith ""
             )

lib/sail_analysis.ml

@@ -18,7 +18,7 @@ type sail_types_context = {
      e.g. MY_UNION_CASE(bits(32), (bits(16), (bits(8), bits(8))))
      is a valid union clause definition in Sail, but it's too
      complicated to record in this table *)
-  union_case_to_arg_types : (string, union_case_type list) Hashtbl.t;
+  union_cases_type_signature : (string, union_case_type list) Hashtbl.t;
   (* Records the names of all enum types *)
   enum_names : string set;
   (* Records the names of all struct types *)
@@ -69,13 +69,13 @@ let assoc_clause_with_args state _ union_id clause_id typ =
             )
             args_typ
         in
-        Hashtbl.add state.type_ctx.union_case_to_arg_types name args
+        Hashtbl.add state.type_ctx.union_cases_type_signature name args
     | Typ_id id ->
-        Hashtbl.add state.type_ctx.union_case_to_arg_types name
+        Hashtbl.add state.type_ctx.union_cases_type_signature name
           [Named_type (id_to_str id)]
     | Typ_app (id, args)
       when id_to_str id = "bits" || id_to_str id = "bitvector" ->
-        Hashtbl.add state.type_ctx.union_case_to_arg_types name
+        Hashtbl.add state.type_ctx.union_cases_type_signature name
           [Bitvec (sail_bitv_size_to_int (List.nth args 0))]
     | _ -> failwith ("Unsupported type expression after the union case " ^ name)
   )
@@ -258,7 +258,7 @@ let analyze ast =
     {
       type_ctx =
         {
-          union_case_to_arg_types = Hashtbl.create 50;
+          union_cases_type_signature = Hashtbl.create 50;
           enum_names = Hashtbl.create 100;
           struct_names = Hashtbl.create 100;
           bitv_synonyms = Hashtbl.create 50;
@@ -283,3 +283,27 @@ let analyze ast =
   in
   foreach_node ast analyzer_processor analysis_result;
   analysis_result
+
+let get_bv2enum_mapping ana map_name =
+  let bv2enum_mappings = ana.mapping_ctx.enum_bitv_mappings_registery in
+  try Some (Hashtbl.find bv2enum_mappings map_name) with Not_found -> None
+
+let get_bv2struct_mapping ana map_name =
+  let bv2struct_mappings = ana.mapping_ctx.struct_bitv_mappings_registery in
+  try Some (Hashtbl.find bv2struct_mappings map_name) with Not_found -> None
+
+let get_size_of_bv_synonym ana name =
+  try Some (Hashtbl.find ana.type_ctx.bitv_synonyms name)
+  with Not_found -> None
+
+let get_case_arg_size ana case_name arg_idx =
+  try
+    let typsig =
+      Hashtbl.find ana.type_ctx.union_cases_type_signature case_name
+    in
+    let case_typ = List.nth typsig arg_idx in
+    match case_typ with
+    | Named_type typ_name ->
+        Some (Hashtbl.find ana.type_ctx.bitv_synonyms typ_name)
+    | Bitvec size -> Some size
+  with Not_found -> None

lib/sail_analysis.mli

@@ -0,0 +1,18 @@
+open Libsail
+open Ast_defs
+open Type_check
+
+open Common_types
+
+type sail_analysis_result
+
+val analyze : tannot ast -> sail_analysis_result
+
+val get_bv2enum_mapping : sail_analysis_result -> string -> bv2enum_table option
+
+val get_bv2struct_mapping :
+  sail_analysis_result -> string -> (string * bv2struct_table) option
+
+val get_size_of_bv_synonym : sail_analysis_result -> string -> int option
+
+val get_case_arg_size : sail_analysis_result -> string -> int -> int option

lib/sail_ast_utils.ml

@@ -2,6 +2,8 @@ open Libsail
 open Ast
 open Lexing
 
+open Utils
+
 let stringify_lex_pos start ending =
   if start.pos_fname = ending.pos_fname then
     "file " ^ start.pos_fname ^ " @ [line: "
@@ -57,49 +59,6 @@ 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"
-  | _ -> failwith "UNREACHABLE"
-
-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 padlen = String.length s_padded_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
-    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
@@ -113,15 +72,3 @@ let bitv_literal_size bitv_lit =
   | 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"
-
-let str_starts_with prefix str =
-  let plen = String.length prefix in
-  let slen = String.length str in
-  if plen > slen then false
-  else (
-    let str_prefix = String.sub str 0 plen in
-    str_prefix = prefix
-  )
-
-let add_prefix_unless_exists prefix str =
-  if str_starts_with prefix str then str else prefix ^ str

lib/stringify.ml

@@ -5,6 +5,7 @@ open Decode_procedure
 open Constants
 open Gen_clike_typedef
 open Sail_ast_utils
+open Utils
 
 let mk_indentation lvl =
   if lvl = 0 then ""
@@ -84,7 +85,7 @@ let rec stringify_bv vars e =
       let mask =
         0 :: List.init 63 (fun x -> x + 1)
         |> List.map (fun i -> if i >= i1 && i < i2 then "1" else "0")
-        |> List.rev |> String.concat "" |> Sail_ast_utils.binary_str_to_hex_str
+        |> List.rev |> String.concat "" |> binary_str_to_hex_str
       in
       let masking_expr = binary_stream_c_parameter ^ " & 0x" ^ mask in
       if i1 <> 0 then "(" ^ masking_expr ^ ")" ^ ">>" ^ string_of_int i1

lib/utils.ml

@@ -0,0 +1,57 @@
+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 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 padlen = String.length s_padded_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
+    Buffer.add_string hexstr hex_digit;
+    i := !i + 4
+  done;
+  Buffer.contents hexstr
+
+let str_starts_with prefix str =
+  let plen = String.length prefix in
+  let slen = String.length str in
+  if plen > slen then false
+  else (
+    let str_prefix = String.sub str 0 plen in
+    str_prefix = prefix
+  )
+
+let add_prefix_unless_exists prefix str =
+  if str_starts_with prefix str then str else prefix ^ str
+
+let get_some_or_failwith opt msg =
+  match opt with Some thing -> thing | None -> failwith msg