diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/jib_compile.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 17 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 8 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 12 |
4 files changed, 15 insertions, 24 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index b178f0e2..0efac940 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1243,8 +1243,6 @@ let compile_funcl ctx id pat guard exp = (** Compile a Sail toplevel definition into an IR definition **) let rec compile_def n total ctx def = - reset_anf_counter (); - reset_gensym_counter (); match def with | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), _)) when !opt_memo_cache -> diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index e9ec8260..fbaf8d3f 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -64,7 +64,7 @@ let zencode_id id = Util.zencode_string (string_of_id id) let zencode_name id = string_of_name ~deref_current_exception:false ~zencode:true id let zencode_uid (id, ctyps) = Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) - + let opt_ignore_overflow = ref false let opt_auto = ref false @@ -254,13 +254,6 @@ let smt_value ctx vl ctyp = Real_lit str | vl, _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl) -let zencode_ctor ctor_id unifiers = - match unifiers with - | [] -> - zencode_id ctor_id - | _ -> - Util.zencode_string (string_of_id ctor_id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers) - let rec smt_cval ctx cval = match cval_ctyp cval with | CT_constant n -> @@ -289,9 +282,9 @@ let rec smt_cval ctx cval = | V_call (Bor, cvals) -> smt_disj (List.map (smt_cval ctx) cvals) | V_ctor_kind (union, ctor_id, unifiers, _) -> - Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)]) + Fn ("not", [Tester (zencode_uid (ctor_id, unifiers), smt_cval ctx union)]) | V_ctor_unwrap (ctor_id, union, unifiers, _) -> - Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_cval ctx union]) + Fn ("un" ^ zencode_uid (ctor_id, unifiers), [smt_cval ctx union]) | V_field (union, field) -> begin match cval_ctyp union with | CT_struct (struct_id, _) -> @@ -1642,9 +1635,9 @@ let smt_instr ctx = end else if not extern then let smt_args = List.map (smt_cval ctx) args in - [define_const ctx id ret_ctyp (Ctor (zencode_id (fst function_id), smt_args))] + [define_const ctx id ret_ctyp (Ctor (zencode_uid function_id, smt_args))] else - failwith ("Unrecognised function " ^ string_of_id (fst function_id)) + failwith ("Unrecognised function " ^ string_of_uid function_id) | I_aux (I_copy (CL_addr (CL_id (_, _)), _), (_, l)) -> Reporting.unreachable l __POS__ "Register reference write should be re-written by now" diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index ba4337b0..9c405a48 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -78,7 +78,7 @@ let get_cond graph n = IntMap.find n graph.conds else V_call (Bnot, [IntMap.find (abs n) graph.conds]) - + let get_vertex graph n = graph.nodes.(n) let iter_graph f graph = @@ -309,7 +309,7 @@ let immediate_dominators graph root = let idom = Array.make (cardinal graph) none in let samedom = Array.make (cardinal graph) none in let best = Array.make (cardinal graph) none in - let dfnum = Array.make (cardinal graph) 0 in + let dfnum = Array.make (cardinal graph) (-1) in let bucket = Array.make (cardinal graph) IntSet.empty in let rec ancestor_with_lowest_semi v = @@ -332,7 +332,7 @@ let immediate_dominators graph root = let count = ref 0 in let rec dfs p n = - if dfnum.(n) = 0 then + if dfnum.(n) = -1 then begin dfnum.(n) <- !count; vertex.(!count) <- n; @@ -372,7 +372,7 @@ let immediate_dominators graph root = if semi.(y) = semi.(v) then idom.(v) <- p else - samedom.(n) <- y + samedom.(v) <- y ) bucket.(p); done; for i = 1 to !count - 1 do diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index caef7ecb..13438208 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -331,7 +331,7 @@ and string_of_uid (id, ctyps) = match ctyps with | [] -> Util.zencode_string (string_of_id id) | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) - + (** This function is like string_of_ctyp, but recursively prints all constructors in variants and structs. Used for debug output. *) and full_string_of_ctyp = function @@ -391,7 +391,7 @@ let rec string_of_cval = function Printf.sprintf "{%s}" (Util.string_of_list ", " (fun (field, cval) -> string_of_uid field ^ " = " ^ string_of_cval cval) fields) | V_poly (f, _) -> string_of_cval f - + let rec map_ctyp f = function | (CT_lint | CT_fint _ | CT_constant _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp @@ -503,7 +503,7 @@ module CTSet = Set.Make(CT) module CTMap = Map.Make(CT) module UId = struct - type t = uid + type t = (id * ctyp list) let lex_ord c1 c2 = if c1 = 0 then c2 else c1 let rec compare_ctyps ctyps1 ctyps2 = match ctyps1, ctyps2 with @@ -516,9 +516,9 @@ module UId = struct let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in lex_ord (Id.compare id1 id2) (compare_ctyps ctyps1 ctyps2) end - + module UBindings = Map.Make(UId) - + let rec ctyp_unify ctyp1 ctyp2 = match ctyp1, ctyp2 with | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 -> @@ -771,7 +771,7 @@ let cdef_concatmap_instr f = function CDEF_finish (id, List.concat (List.map (concatmap_instr f) instrs)) | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp) | CDEF_type tdef -> CDEF_type tdef - + let ctype_def_map_ctyp f = function | CTD_enum (id, ids) -> CTD_enum (id, ids) | CTD_struct (id, ctors) -> CTD_struct (id, List.map (fun ((id, ctyps), ctyp) -> ((id, List.map f ctyps), f ctyp)) ctors) |