Update isla-sail

rems-project · Mar 20, 2024 · 66d11a4 · 66d11a4
1 parent cfcc2ef
commit 66d11a4
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/isla-sail/jib_ir.ml b/isla-sail/jib_ir.ml
@@ -197,7 +197,7 @@ module Ir_formatter = struct
     let id_ctyp (id, ctyp) =
       sprintf "%s: %s" (zencode_id id) (C.typ ctyp)
 
-    let output_def buf = function
+    let output_def_aux buf = function
       | CDEF_register (id, ctyp, []) ->
          Buffer.add_string buf (sprintf "%s %s : %s" (C.keyword "register") (zencode_id id) (C.typ ctyp))
       | CDEF_register (id, ctyp, instrs) ->
@@ -240,6 +240,8 @@ module Ir_formatter = struct
       | CDEF_startup _ | CDEF_finish _ ->
          Reporting.unreachable Parse_ast.Unknown __POS__ "Unexpected startup / finish"
 
+    let output_def buf (CDEF_aux (aux, _)) = output_def_aux buf aux
+
     let rec output_defs' buf = function
       | def :: defs ->
          output_def buf def;

diff --git a/isla-sail/sail_plugin_isla.ml b/isla-sail/sail_plugin_isla.ml
@@ -289,7 +289,7 @@ let remove_casts cdefs =
   let cdefs = List.map (fun cdef -> cdef_concatmap_instr remove_instr_casts cdef) cdefs in
   let vals =
     List.map (fun (fid, (ctyp_from, ctyp_to)) ->
-        CDEF_val (mk_id fid, Some fid, [ctyp_from], ctyp_to)
+        CDEF_aux (CDEF_val (mk_id fid, Some fid, [ctyp_from], ctyp_to), mk_def_annot Parse_ast.Unknown)
       ) (StringMap.bindings !conversions)
   in
   vals @ cdefs
@@ -302,12 +302,12 @@ let remove_extern_impls cdefs =
   let exts = ref IdSet.empty in
   List.iter
     (function
-     | CDEF_val (id, Some _, _, _) -> exts := IdSet.add id !exts
+     | CDEF_aux (CDEF_val (id, Some _, _, _), _) -> exts := IdSet.add id !exts
      | _ -> ()
     ) cdefs;
   List.filter
     (function
-     | CDEF_fundef (id, _, _, _) when IdSet.mem id !exts -> false
+     | CDEF_aux (CDEF_fundef (id, _, _, _), _) when IdSet.mem id !exts -> false
      | _ -> true
     ) cdefs
 
@@ -330,7 +330,7 @@ let fix_cons cdefs =
       let cdef = cdef_map_instr (collect_cons_ctyps list_ctyps) cdef in
       let vals =
         List.map (fun ctyp ->
-            CDEF_val (cons_name ctyp, Some "cons", [ctyp; CT_list ctyp], CT_list ctyp)
+            CDEF_aux (CDEF_val (cons_name ctyp, Some "cons", [ctyp; CT_list ctyp], CT_list ctyp), mk_def_annot Parse_ast.Unknown)
           ) (CTSet.elements (CTSet.diff !list_ctyps !all_list_ctyps)) in
       vals @ [cdef]
     ) cdefs