diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 4 | ||||
| -rw-r--r-- | src/jib.lem | 140 | ||||
| -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 |
6 files changed, 19 insertions, 164 deletions
diff --git a/src/Makefile b/src/Makefile index 020d6813..a002d4f3 100644 --- a/src/Makefile +++ b/src/Makefile @@ -74,6 +74,9 @@ full: sail lib doc ast.lem: ../language/sail.ott ott -sort false -generate_aux_rules true -o ast.lem -picky_multiple_parses true ../language/sail.ott +jib.lem: ../language/jib.ott ast.lem + ott -sort false -generate_aux_rules true -o jib.lem -picky_multiple_parses true ../language/jib.ott + ast.ml: ast.lem lem -ocaml ast.lem sed -i.bak -f ast.sed ast.ml @@ -134,6 +137,7 @@ clean: -rm -f ast.lem -rm -f ast.ml.bak -rm -f jib.ml + -rm -f jib.lem -rm -f jib.ml.bak -rm -f manifest.ml diff --git a/src/jib.lem b/src/jib.lem deleted file mode 100644 index c8959d10..00000000 --- a/src/jib.lem +++ /dev/null @@ -1,140 +0,0 @@ -(* generated by Ott 0.29 from: ../language/jib.ott *) -open import Pervasives - - -open import Ast -open import Value2 - - - -type name = - | Name of id * nat - | Have_exception of nat - | Current_exception of nat - | Return of nat - - -type ctyp = (* C type *) - | CT_lint - | CT_fint of nat - | CT_constant of integer - | CT_lbits of bool - | CT_sbits of nat * bool - | CT_fbits of nat * bool - | CT_unit - | CT_bool - | CT_bit - | CT_string - | CT_real - | CT_tup of list ctyp - | CT_enum of id * list id - | CT_struct of id * list (uid * ctyp) - | CT_variant of id * list (uid * ctyp) - | CT_vector of bool * ctyp - | CT_list of ctyp - | CT_ref of ctyp - | CT_poly - -and uid = id * list ctyp - -type op = - | Bnot - | Bor - | Band - | List_hd - | List_tl - | Bit_to_bool - | Eq - | Neq - | Ilt - | Ilteq - | Igt - | Igteq - | Iadd - | Isub - | Unsigned of nat - | Signed of nat - | Bvnot - | Bvor - | Bvand - | Bvxor - | Bvadd - | Bvsub - | Bvaccess - | Concat - | Zero_extend of nat - | Sign_extend of nat - | Slice of nat - | Sslice of nat - | Set_slice - | Replicate of nat - - -type clexp = - | CL_id of name * ctyp - | CL_rmw of name * name * ctyp - | CL_field of clexp * uid - | CL_addr of clexp - | CL_tuple of clexp * nat - | CL_void - - -type cval = - | V_id of name * ctyp - | V_ref of name * ctyp - | V_lit of vl * ctyp - | V_struct of list (uid * cval) * ctyp - | V_ctor_kind of cval * id * list ctyp * ctyp - | V_ctor_unwrap of id * cval * list ctyp * ctyp - | V_tuple_member of cval * nat * nat - | V_call of op * list cval - | V_field of cval * uid - | V_poly of cval * ctyp - - -type iannot = nat * nat * nat - - -type instr_aux = - | I_decl of ctyp * name - | I_init of ctyp * name * cval - | I_jump of cval * string - | I_goto of string - | I_label of string - | I_funcall of clexp * bool * uid * list cval - | I_copy of clexp * cval - | I_clear of ctyp * name - | I_undefined of ctyp - | I_match_failure - | I_end of name - | I_if of cval * list instr * list instr * ctyp - | I_block of list instr - | I_try_block of list instr - | I_throw of cval - | I_comment of string - | I_raw of string - | I_return of cval - | I_reset of ctyp * name - | I_reinit of ctyp * name * cval - -and instr = - | I_aux of instr_aux * iannot - - -type ctype_def = (* C type definition *) - | CTD_enum of id * list id - | CTD_struct of id * list (uid * ctyp) - | CTD_variant of id * list (uid * ctyp) - - -type cdef = - | CDEF_reg_dec of id * ctyp * list instr - | CDEF_type of ctype_def - | CDEF_let of nat * list (id * ctyp) * list instr - | CDEF_spec of id * list ctyp * ctyp - | CDEF_fundef of id * maybe id * list id * list instr - | CDEF_startup of id * list instr - | CDEF_finish of id * list instr - - - 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) |