From 4fdc2f6c76920882b48bd024a63e6fb8ed0a1819 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 10 Jun 2020 07:05:16 -0700 Subject: [PATCH] [sledge] Build: Wrap Llair library Summary: Refer to Llair modules using `Llair.` qualifier, except for in `Frontend`, which makes so much use of `Llair` that it is now opened (`Llair` only contains types and modules, so `open` is safe). Reviewed By: jvillard Differential Revision: D21720979 fbshipit-source-id: dd42075d9 --- sledge/bin/domain_itv.ml | 44 ++++++---- sledge/bin/frontend.ml | 134 ++++++++++++++--------------- sledge/bin/sledge_cli.ml | 9 +- sledge/dune | 1 - sledge/src/control.ml | 48 ++++++----- sledge/src/control.mli | 2 +- sledge/src/domain_intf.ml | 34 ++++---- sledge/src/domain_relation.ml | 12 +-- sledge/src/domain_relation.mli | 4 +- sledge/src/domain_sh.ml | 28 +++--- sledge/src/domain_sh.mli | 4 +- sledge/src/domain_unit.ml | 4 +- sledge/src/domain_used_globals.ml | 40 +++++---- sledge/src/domain_used_globals.mli | 8 +- sledge/src/exec.ml | 4 +- sledge/src/llair/llair.ml | 6 ++ sledge/src/llair/llair.mli | 6 ++ sledge/src/report.ml | 10 +-- sledge/src/term.ml | 25 +++--- sledge/src/term.mli | 10 +-- sledge/src/term_test.ml | 32 +++---- 21 files changed, 250 insertions(+), 215 deletions(-) diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml index 153f4b2a4..ecf033500 100644 --- a/sledge/bin/domain_itv.ml +++ b/sledge/bin/domain_itv.ml @@ -49,17 +49,18 @@ let pp fs = let report_fmt_thunk = Fn.flip pp let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||]) let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string -let apron_var_of_reg = Reg.name >> apron_var_of_name +let apron_var_of_reg = Llair.Reg.name >> apron_var_of_name -let rec apron_typ_of_llair_typ : Typ.t -> Texpr1.typ option = function - | Pointer {elt= _} -> apron_typ_of_llair_typ Typ.siz +let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function + | Pointer {elt= _} -> apron_typ_of_llair_typ Llair.Typ.siz | Integer {bits= _} -> Some Texpr1.Int | Float {bits= 32; enc= `IEEE} -> Some Texpr1.Single | Float {bits= 64; enc= `IEEE} -> Some Texpr1.Double | Float {bits= 80; enc= `Extended} -> Some Texpr1.Extended | Float {bits= 128; enc= `IEEE} -> Some Texpr1.Quad | t -> - warn "No corresponding apron type for llair type %a " Typ.pp t () ; + warn "No corresponding apron type for llair type %a " Llair.Typ.pp t + () ; None let apron_of_q = Q.to_float >> fun fp -> Texpr1.Cst (Coeff.s_of_float fp) @@ -168,20 +169,21 @@ and mk_bool_binop typ q op te1 te2 = else Texpr1.Cst (Coeff.i_of_int (-1) 0) let assign reg exp q = - [%Trace.call fun {pf} -> pf "{%a}@\n%a := %a" pp q Reg.pp reg Exp.pp exp] + [%Trace.call fun {pf} -> + pf "{%a}@\n%a := %a" pp q Llair.Reg.pp reg Llair.Exp.pp exp] ; let lval = apron_var_of_reg reg in ( match Option.bind ~f:(apron_texpr_of_llair_term (Term.of_exp exp) q) - (apron_typ_of_llair_typ (Reg.typ reg)) + (apron_typ_of_llair_typ (Llair.Reg.typ reg)) with | Some e -> let env = Abstract1.env q in let new_env = match ( Environment.mem_var env lval - , apron_typ_of_llair_typ (Reg.typ reg) ) + , apron_typ_of_llair_typ (Llair.Reg.typ reg) ) with | true, _ -> env | false, Some Texpr1.Int -> Environment.add env [|lval|] [||] @@ -214,18 +216,19 @@ let exec_kill q r = (** perform a series [move_vec] of reg:=exp moves at state [q] *) let exec_move q move_vec = let defs, uses = - IArray.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty) + IArray.fold move_vec ~init:(Llair.Reg.Set.empty, Llair.Reg.Set.empty) ~f:(fun (defs, uses) (r, e) -> - (Reg.Set.add defs r, Exp.fold_regs e ~init:uses ~f:Reg.Set.add) ) + ( Llair.Reg.Set.add defs r + , Llair.Exp.fold_regs e ~init:uses ~f:Llair.Reg.Set.add ) ) in - assert (Reg.Set.disjoint defs uses) ; + assert (Llair.Reg.Set.disjoint defs uses) ; IArray.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a) let exec_inst q i = match (i : Llair.inst) with | Move {reg_exps; loc= _} -> Some (exec_move q reg_exps) | Store {ptr; exp; len= _; loc= _} -> ( - match Reg.of_exp ptr with + match Llair.Reg.of_exp ptr with | Some reg -> Some (assign reg exp q) | None -> Some q ) | Load {reg; ptr; len= _; loc= _} -> Some (assign reg ptr q) @@ -237,7 +240,7 @@ let exec_inst q i = (** Treat any intrinsic function as havoc on the return register [aret] *) let exec_intrinsic ~skip_throw:_ pre aret i _ = - let name = Reg.name i in + let name = Llair.Reg.name i in if List.exists [ "malloc" @@ -264,14 +267,15 @@ let exec_intrinsic ~skip_throw:_ pre aret i _ = then Option.map ~f:(Option.some << exec_kill pre) aret else None -type from_call = {areturn: Reg.t option; caller_q: t} [@@deriving sexp_of] +type from_call = {areturn: Llair.Reg.t option; caller_q: t} +[@@deriving sexp_of] let recursion_beyond_bound = `prune (** existentially quantify locals *) let post locals _ (q : t) = let locals = - Reg.Set.fold locals ~init:[] ~f:(fun a r -> + Llair.Reg.Set.fold locals ~init:[] ~f:(fun a r -> let v = apron_var_of_reg r in if Environment.mem_var q.env v then v :: a else a ) |> Array.of_list @@ -283,7 +287,7 @@ let retn _ freturn {areturn; caller_q} callee_q = match (areturn, freturn) with | Some aret, Some fret -> let env_fret_only = - match apron_typ_of_llair_typ (Reg.typ fret) with + match apron_typ_of_llair_typ (Llair.Reg.typ fret) with | None -> Environment.make [||] [||] | Some Texpr1.Int -> Environment.make [|apron_var_of_reg fret|] [||] | _ -> Environment.make [||] [|apron_var_of_reg fret|] @@ -312,14 +316,16 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_ if summaries then todo "Summaries not yet implemented for interval analysis" () else - let mangle r = Reg.program (Reg.typ r) ("__tmp__" ^ Reg.name r) in + let mangle r = + Llair.Reg.program (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r) + in let args = List.zip_exn formals actuals in let q' = List.fold args ~init:q ~f:(fun q (f, a) -> assign (mangle f) a q) in let callee_env = List.fold formals ~init:([], []) ~f:(fun (is, fs) f -> - match apron_typ_of_llair_typ (Reg.typ f) with + match apron_typ_of_llair_typ (Llair.Reg.typ f) with | None -> (is, fs) | Some Texpr1.Int -> (apron_var_of_reg (mangle f) :: is, fs) | _ -> (is, apron_var_of_reg (mangle f) :: fs) ) @@ -338,8 +344,8 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_ let dnf q = [q] let resolve_callee lookup ptr q = - match Reg.of_exp ptr with - | Some callee -> (lookup (Reg.name callee), q) + match Llair.Reg.of_exp ptr with + | Some callee -> (lookup (Llair.Reg.name callee), q) | None -> ([], q) type summary = t diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index 03db39ed8..1f65f6c53 100644 --- a/sledge/bin/frontend.ml +++ b/sledge/bin/frontend.ml @@ -7,6 +7,8 @@ (** Translate LLVM to LLAIR *) +open Llair + let pp_lltype fs t = Format.pp_print_string fs (Llvm.string_of_lltype t) (* WARNING: SLOW on instructions and functions *) @@ -722,7 +724,7 @@ let pop_stack_frame_of_function : func ; let pop retn_loc = List.map entry_regs ~f:(fun reg -> - Llair.Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc ) + Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc ) in pop @@ -792,27 +794,25 @@ let xlate_jump : | At_end blk -> fail "xlate_jump: %a" pp_llblock blk () in let dst_lbl = label_of_block dst in - let jmp = Llair.Jump.mk dst_lbl in + let jmp = Jump.mk dst_lbl in match xlate_jump_ reg_exps (Llvm.instr_begin dst) with | [] -> (jmp, blocks) | reg_exps -> - let mov = - Llair.Inst.move ~reg_exps:(IArray.of_list_rev reg_exps) ~loc - in + let mov = Inst.move ~reg_exps:(IArray.of_list_rev reg_exps) ~loc in let lbl = find_name instr ^ ".jmp." ^ dst_lbl in let blk = - Llair.Block.mk ~lbl + Block.mk ~lbl ~cmnd:(IArray.of_array [|mov|]) - ~term:(Llair.Term.goto ~dst:jmp ~loc) + ~term:(Term.goto ~dst:jmp ~loc) in let blocks = match List.find blocks ~f:(fun b -> String.equal lbl b.lbl) with | None -> blk :: blocks | Some blk0 -> - assert (Llair.Block.equal blk0 blk) ; + assert (Block.equal blk0 blk) ; blocks in - (Llair.Jump.mk lbl, blocks) + (Jump.mk lbl, blocks) (** An LLVM instruction is translated to a sequence of LLAIR instructions and a terminator, plus some additional blocks to which it may refer @@ -821,20 +821,18 @@ let xlate_jump : type code = Llair.inst list * Llair.term * Llair.block list let pp_code fs (insts, term, blocks) = - Format.fprintf fs "@[@,@[%a%t@]%t@[%a@]@]" - (List.pp "@ " Llair.Inst.pp) + Format.fprintf fs "@[@,@[%a%t@]%t@[%a@]@]" (List.pp "@ " Inst.pp) insts (fun fs -> match term with - | Llair.Unreachable -> () + | Unreachable -> () | _ -> Format.fprintf fs "%t%a" (fun fs -> if List.is_empty insts then () else Format.fprintf fs "@ " ) - Llair.Term.pp term ) + Term.pp term ) (fun fs -> if List.is_empty blocks then () else Format.fprintf fs "@\n") - (List.pp "@ " Llair.Block.pp) - blocks + (List.pp "@ " Block.pp) blocks let rec xlate_func_name x llv = match Llvm.classify_value llv with @@ -864,7 +862,7 @@ let xlate_instr : let continue insts_term_to_code = [%Trace.retn fun {pf} () -> - pf "%a" pp_code (insts_term_to_code ([], Llair.Term.unreachable))] + pf "%a" pp_code (insts_term_to_code ([], Term.unreachable))] () ; continue insts_term_to_code in @@ -884,7 +882,7 @@ let xlate_instr : let reg = xlate_name x instr in let exp = xlate instr in let reg_exps = IArray.of_array [|(reg, exp)|] in - emit_inst (Llair.Inst.move ~reg_exps ~loc) + emit_inst (Inst.move ~reg_exps ~loc) in let opcode = Llvm.instr_opcode instr in match opcode with @@ -892,13 +890,13 @@ let xlate_instr : let reg = xlate_name x instr in let len = xlate_size_of x instr in let ptr = xlate_value x (Llvm.operand instr 0) in - emit_inst (Llair.Inst.load ~reg ~ptr ~len ~loc) + emit_inst (Inst.load ~reg ~ptr ~len ~loc) | Store -> let rand0 = Llvm.operand instr 0 in let exp = xlate_value x rand0 in let len = xlate_size_of x rand0 in let ptr = xlate_value x (Llvm.operand instr 1) in - emit_inst (Llair.Inst.store ~ptr ~exp ~len ~loc) + emit_inst (Inst.store ~ptr ~exp ~len ~loc) | Alloca -> let reg = xlate_name x instr in let rand = Llvm.operand instr 0 in @@ -909,7 +907,7 @@ let xlate_instr : in assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ; let len = xlate_size_of x instr in - emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc) + emit_inst (Inst.alloc ~reg ~num ~len ~loc) | Call -> ( let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in let lltyp = Llvm.type_of maybe_llfunc in @@ -934,7 +932,7 @@ let xlate_instr : | Ok () -> warn "ignoring uninterpreted %s %s" msg fname () | Error _ -> () ) ; let reg = xlate_name_opt x instr in - emit_inst (Llair.Inst.nondet ~reg ~msg:fname ~loc) + emit_inst (Inst.nondet ~reg ~msg:fname ~loc) in (* intrinsics *) match xlate_intrinsic_exp fname with @@ -943,7 +941,7 @@ let xlate_instr : match String.split fname ~on:'.' with | ["__llair_throw"] -> let exc = xlate_value x (Llvm.operand instr 0) in - emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc) + emit_term ~prefix:(pop loc) (Term.throw ~exc ~loc) | ["__llair_alloc" (* void* __llair_alloc(unsigned size) *)] -> let reg = xlate_name x instr in let num_operand = Llvm.operand instr 0 in @@ -953,14 +951,14 @@ let xlate_instr : (xlate_value x num_operand) in let len = Exp.integer Typ.siz (Z.of_int 1) in - emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc) + emit_inst (Inst.alloc ~reg ~num ~len ~loc) | ["_Znwm" (* operator new(size_t num) *)] |[ "_ZnwmSt11align_val_t" (* operator new(unsigned long, std::align_val_t) *) ] -> let reg = xlate_name x instr in let num = xlate_value x (Llvm.operand instr 0) in let len = xlate_size_of x instr in - emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc) + emit_inst (Inst.alloc ~reg ~num ~len ~loc) | ["_ZdlPv" (* operator delete(void* ptr) *)] |[ "_ZdlPvSt11align_val_t" (* operator delete(void* ptr, std::align_val_t) *) ] @@ -969,23 +967,23 @@ let xlate_instr : ] |["free" (* void free(void* ptr) *)] -> let ptr = xlate_value x (Llvm.operand instr 0) in - emit_inst (Llair.Inst.free ~ptr ~loc) + emit_inst (Inst.free ~ptr ~loc) | "llvm" :: "memset" :: _ -> let dst = xlate_value x (Llvm.operand instr 0) in let byt = xlate_value x (Llvm.operand instr 1) in let len = xlate_value x (Llvm.operand instr 2) in - emit_inst (Llair.Inst.memset ~dst ~byt ~len ~loc) + emit_inst (Inst.memset ~dst ~byt ~len ~loc) | "llvm" :: "memcpy" :: _ -> let dst = xlate_value x (Llvm.operand instr 0) in let src = xlate_value x (Llvm.operand instr 1) in let len = xlate_value x (Llvm.operand instr 2) in - emit_inst (Llair.Inst.memcpy ~dst ~src ~len ~loc) + emit_inst (Inst.memcpy ~dst ~src ~len ~loc) | "llvm" :: "memmove" :: _ -> let dst = xlate_value x (Llvm.operand instr 0) in let src = xlate_value x (Llvm.operand instr 1) in let len = xlate_value x (Llvm.operand instr 2) in - emit_inst (Llair.Inst.memmov ~dst ~src ~len ~loc) - | ["abort"] | ["llvm"; "trap"] -> emit_inst (Llair.Inst.abort ~loc) + emit_inst (Inst.memmov ~dst ~src ~len ~loc) + | ["abort"] | ["llvm"; "trap"] -> emit_inst (Inst.abort ~loc) (* dropped / handled elsewhere *) | ["llvm"; "dbg"; ("declare" | "value")] |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _ -> @@ -1033,13 +1031,13 @@ let xlate_instr : xlate_value x (Llvm.operand instr i) ) in let areturn = xlate_name_opt x instr in - let return = Llair.Jump.mk lbl in - Llair.Term.call ~callee ~typ ~actuals ~areturn ~return - ~throw:None ~loc + let return = Jump.mk lbl in + Term.call ~callee ~typ ~actuals ~areturn ~return ~throw:None + ~loc in continue (fun (insts, term) -> let cmnd = IArray.of_list insts in - ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) ) ) + ([], call, [Block.mk ~lbl ~cmnd ~term]) ) ) ) | Invoke -> ( let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in let lltyp = Llvm.type_of llfunc in @@ -1063,12 +1061,11 @@ let xlate_instr : match String.split fname ~on:'.' with | _ when Option.is_some (xlate_intrinsic_exp fname) -> let dst, blocks = xlate_jump x instr return_blk loc [] in - emit_term (Llair.Term.goto ~dst ~loc) ~blocks + emit_term (Term.goto ~dst ~loc) ~blocks | ["__llair_throw"] -> let dst, blocks = xlate_jump x instr unwind_blk loc [] in - emit_term (Llair.Term.goto ~dst ~loc) ~blocks - | ["abort"] -> - emit_term ~prefix:[Llair.Inst.abort ~loc] Llair.Term.unreachable + emit_term (Term.goto ~dst ~loc) ~blocks + | ["abort"] -> emit_term ~prefix:[Inst.abort ~loc] Term.unreachable | ["_Znwm" (* operator new(size_t num) *)] |[ "_ZnwmSt11align_val_t" (* operator new(unsigned long num, std::align_val_t) *) ] @@ -1078,9 +1075,8 @@ let xlate_instr : let len = xlate_size_of x instr in let dst, blocks = xlate_jump x instr return_blk loc [] in emit_term - ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc] - (Llair.Term.goto ~dst ~loc) - ~blocks + ~prefix:[Inst.alloc ~reg ~num ~len ~loc] + (Term.goto ~dst ~loc) ~blocks (* unimplemented *) | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ -> todo "statepoints:@ %a" pp_llvalue instr () @@ -1097,26 +1093,24 @@ let xlate_instr : let throw, blocks = xlate_jump x instr unwind_blk loc blocks in let throw = Some throw in emit_term - (Llair.Term.call ~callee ~typ ~actuals ~areturn ~return ~throw - ~loc) + (Term.call ~callee ~typ ~actuals ~areturn ~return ~throw ~loc) ~blocks ) | Ret -> let exp = if Llvm.num_operands instr = 0 then None else Some (xlate_value x (Llvm.operand instr 0)) in - emit_term ~prefix:(pop loc) (Llair.Term.return ~exp ~loc) + emit_term ~prefix:(pop loc) (Term.return ~exp ~loc) | Br -> ( match Option.value_exn (Llvm.get_branch instr) with | `Unconditional blk -> let dst, blocks = xlate_jump x instr blk loc [] in - emit_term (Llair.Term.goto ~dst ~loc) ~blocks + emit_term (Term.goto ~dst ~loc) ~blocks | `Conditional (cnd, thn, els) -> let key = xlate_value x cnd in let thn, blocks = xlate_jump x instr thn loc [] in let els, blocks = xlate_jump x instr els loc blocks in - emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks - ) + emit_term (Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks ) | Switch -> let key = xlate_value x (Llvm.operand instr 0) in let cases, blocks = @@ -1138,7 +1132,7 @@ let xlate_instr : let tbl = IArray.of_list cases in let blk = Llvm.block_of_value (Llvm.operand instr 1) in let els, blocks = xlate_jump x instr blk loc blocks in - emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) ~blocks + emit_term (Term.switch ~key ~tbl ~els ~loc) ~blocks | IndirectBr -> let ptr = xlate_value x (Llvm.operand instr 0) in let num_dests = Llvm.num_operands instr - 1 in @@ -1155,7 +1149,7 @@ let xlate_instr : dests 1 [] in let tbl = IArray.of_list lldests in - emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) ~blocks + emit_term (Term.iswitch ~ptr ~tbl ~loc) ~blocks | LandingPad -> (* Translate the landingpad clauses to code to load the type_info from the thrown exception, and test the type_info against the clauses, @@ -1179,7 +1173,7 @@ let xlate_instr : ~fld ~lltyp:typ in let len = Exp.integer Typ.siz (Z.of_int (size_of x typ)) in - Llair.Inst.load ~reg:ti ~ptr ~len ~loc + Inst.load ~reg:ti ~ptr ~len ~loc in let ti = Exp.reg ti in let typeid = xlate_llvm_eh_typeid_for x tip ti in @@ -1188,19 +1182,19 @@ let xlate_instr : let jump_unwind i sel rev_blocks = let exp = Exp.record exc_typ (IArray.of_array [|exc; sel|]) in let mov = - Llair.Inst.move ~reg_exps:(IArray.of_array [|(reg, exp)|]) ~loc + Inst.move ~reg_exps:(IArray.of_array [|(reg, exp)|]) ~loc in let lbl_i = lbl ^ "." ^ Int.to_string i in let blk = - Llair.Block.mk ~lbl:lbl_i + Block.mk ~lbl:lbl_i ~cmnd:(IArray.of_array [|mov|]) - ~term:(Llair.Term.goto ~dst:(Llair.Jump.mk lbl) ~loc) + ~term:(Term.goto ~dst:(Jump.mk lbl) ~loc) in - (Llair.Jump.mk lbl_i, blk :: rev_blocks) + (Jump.mk lbl_i, blk :: rev_blocks) in let goto_unwind i sel blocks = let dst, blocks = jump_unwind i sel blocks in - (Llair.Term.goto ~dst ~loc, blocks) + (Term.goto ~dst ~loc, blocks) in let term_unwind, rev_blocks = if Llvm.is_cleanup instr then @@ -1208,9 +1202,9 @@ let xlate_instr : else let num_clauses = Llvm.num_operands instr in let lbl i = name ^ "." ^ Int.to_string i in - let jump i = Llair.Jump.mk (lbl i) in + let jump i = Jump.mk (lbl i) in let block i term = - Llair.Block.mk ~lbl:(lbl i) ~cmnd:IArray.empty ~term + Block.mk ~lbl:(lbl i) ~cmnd:IArray.empty ~term in let match_filter i rev_blocks = jump_unwind i @@ -1222,7 +1216,7 @@ let xlate_instr : let num_tis = Llvm.num_operands clause in if num_tis = 0 then let dst, rev_blocks = match_filter i rev_blocks in - (Llair.Term.goto ~dst ~loc, rev_blocks) + (Term.goto ~dst ~loc, rev_blocks) else match Llvm.classify_type (Llvm.type_of clause) with | Array (* filter *) -> ( @@ -1237,7 +1231,7 @@ let xlate_instr : in let key = xlate_filter 0 in let nzero, rev_blocks = match_filter i rev_blocks in - ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) + ( Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) , rev_blocks ) | _ -> fail "xlate_instr: %a" pp_llvalue instr () ) | _ (* catch *) -> @@ -1249,14 +1243,14 @@ let xlate_instr : (Exp.eq ~typ clause ti) in let nzero, rev_blocks = jump_unwind i typeid rev_blocks in - ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) + ( Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) , rev_blocks ) in let rec rev_blocks i z = if i < num_clauses then let term, z = xlate_clause i z in rev_blocks (i + 1) (block i term :: z) - else block i Llair.Term.unreachable :: z + else block i Term.unreachable :: z in xlate_clause 0 (rev_blocks 1 []) in @@ -1264,14 +1258,14 @@ let xlate_instr : ( [load_ti] , term_unwind , List.rev_append rev_blocks - [Llair.Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term] ) ) + [Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term] ) ) | Resume -> let llrcd = Llvm.operand instr 0 in let typ = xlate_type x (Llvm.type_of llrcd) in let rcd = xlate_value x llrcd in let exc = Exp.select typ rcd 0 in - emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc) - | Unreachable -> emit_term Llair.Term.unreachable + emit_term ~prefix:(pop loc) (Term.throw ~exc ~loc) + | Unreachable -> emit_term Term.unreachable | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast | Add | FAdd |Sub | FSub | Mul | FMul | UDiv | SDiv | FDiv | URem | SRem | FRem @@ -1282,7 +1276,7 @@ let xlate_instr : | VAArg -> let reg = xlate_name_opt x instr in warn "variadic function argument: %a" Loc.pp loc () ; - emit_inst (Llair.Inst.nondet ~reg ~msg:"vaarg" ~loc) + emit_inst (Inst.nondet ~reg ~msg:"vaarg" ~loc) | CleanupRet | CatchRet | CatchPad | CleanupPad | CatchSwitch -> todo "windows exception handling: %a" pp_llvalue instr () | Fence | AtomicCmpXchg | AtomicRMW -> @@ -1318,9 +1312,9 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list = let lbl = label_of_block blk in let pos = skip_phis blk in let insts, term, blocks = xlate_instrs pop x pos in - Llair.Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term :: blocks + Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term :: blocks |> - [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl] + [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).lbl] let report_undefined func name = if Option.is_some (Llvm.use_begin func) then @@ -1352,7 +1346,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func = in let entry = let {Llair.lbl; cmnd; term} = entry_block in - Llair.Block.mk ~lbl ~cmnd ~term + Block.mk ~lbl ~cmnd ~term in let cfg = let rec trav_blocks rev_cfg prev = @@ -1365,12 +1359,12 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func = in trav_blocks (List.rev entry_blocks) entry_blk in - Llair.Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg + Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg | At_end _ -> report_undefined llf name ; - Llair.Func.mk_undefined ~name ~formals ~freturn ~fthrow ) + Func.mk_undefined ~name ~formals ~freturn ~fthrow ) |> - [%Trace.retn fun {pf} -> pf "@\n%a" Llair.Func.pp] + [%Trace.retn fun {pf} -> pf "@\n%a" Func.pp] let transform ~internalize : Llvm.llmodule -> unit = fun llmodule -> diff --git a/sledge/bin/sledge_cli.ml b/sledge/bin/sledge_cli.ml index 65a41bc27..9621e2300 100644 --- a/sledge/bin/sledge_cli.ml +++ b/sledge/bin/sledge_cli.ml @@ -77,14 +77,15 @@ let used_globals pgm preanalyze : Domain_used_globals.r = ; skip_throw= false ; function_summaries= true ; entry_points= Config.find_list "entry-points" - ; globals= Declared Reg.Set.empty } + ; globals= Declared Llair.Reg.Set.empty } pgm in - Per_function (Reg.Map.map summary_table ~f:Reg.Set.union_list) + Per_function + (Llair.Reg.Map.map summary_table ~f:Llair.Reg.Set.union_list) else Declared - (IArray.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g -> - Reg.Set.add acc g.reg )) + (IArray.fold pgm.globals ~init:Llair.Reg.Set.empty ~f:(fun acc g -> + Llair.Reg.Set.add acc g.reg )) let analyze = let%map_open bound = diff --git a/sledge/dune b/sledge/dune index e2bcab535..d8dbae304 100644 --- a/sledge/dune +++ b/sledge/dune @@ -38,7 +38,6 @@ (library (name llair) (public_name sledge.llair) - (wrapped false) (libraries nonstdlib) (flags (:standard -open NS)) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 7d078711c..05f92828c 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -31,15 +31,20 @@ module Make (Dom : Domain_intf.Dom) = struct val pop_throw : t -> init:'a - -> unwind:(Reg.t list -> Reg.Set.t -> Dom.from_call -> 'a -> 'a) + -> unwind: + ( Llair.Reg.t list + -> Llair.Reg.Set.t + -> Dom.from_call + -> 'a + -> 'a) -> (Dom.from_call * Llair.jump * t * 'a) option end = struct type t = | Return of { recursive: bool (** return from a possibly-recursive call *) ; dst: Llair.Jump.t - ; formals: Reg.t list - ; locals: Reg.Set.t + ; formals: Llair.Reg.t list + ; locals: Llair.Reg.Set.t ; from_call: Dom.from_call ; stk: t } | Throw of Llair.Jump.t * t @@ -253,13 +258,13 @@ module Make (Dom : Domain_intf.Dom) = struct let exec_jump stk state block Llair.{dst; retreating} = Work.add ~prev:block ~retreating stk state dst - let summary_table = Hashtbl.create (module Reg) + let summary_table = Hashtbl.create (module Llair.Reg) let exec_call opts stk state block call globals = let Llair.{callee; actuals; areturn; return; recursive} = call in let Llair.{name; formals; freturn; locals; entry} = callee in [%Trace.call fun {pf} -> - pf "%a from %a with state@ %a" Reg.pp name.reg Reg.pp + pf "%a from %a with state@ %a" Llair.Reg.pp name.reg Llair.Reg.pp return.dst.parent.name.reg Dom.pp state] ; let dnf_states = @@ -304,13 +309,13 @@ module Make (Dom : Domain_intf.Dom) = struct [%Trace.printf "@[%t@]" (fun fs -> Hashtbl.iteri summary_table ~f:(fun ~key ~data -> - Format.fprintf fs "@[%a:@ @[%a@]@]@ " Reg.pp key + Format.fprintf fs "@[%a:@ @[%a@]@]@ " Llair.Reg.pp key (List.pp "@," Dom.pp_summary) data ) )] let exec_return ~opts stk pre_state (block : Llair.block) exp = let Llair.{name; formals; freturn; locals} = block.parent in - [%Trace.call fun {pf} -> pf "from: %a" Reg.pp name.reg] + [%Trace.call fun {pf} -> pf "from: %a" Llair.Reg.pp name.reg] ; let summarize post_state = if not opts.function_summaries then post_state @@ -320,7 +325,8 @@ module Make (Dom : Domain_intf.Dom) = struct in let function_summary, post_state = Dom.create_summary ~locals post_state - ~formals:(Reg.Set.union (Reg.Set.of_list formals) globals) + ~formals: + (Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals) in Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ; pp_st () ; @@ -343,7 +349,7 @@ module Make (Dom : Domain_intf.Dom) = struct if opts.function_summaries && List.exists opts.entry_points - ~f:(String.equal (Reg.name name.reg)) + ~f:(String.equal (Llair.Reg.name name.reg)) then summarize exit_state |> (ignore : Dom.t -> unit) ; Work.skip ) |> @@ -351,7 +357,7 @@ module Make (Dom : Domain_intf.Dom) = struct let exec_throw stk pre_state (block : Llair.block) exc = let func = block.parent in - [%Trace.call fun {pf} -> pf "from %a" Reg.pp func.name.reg] + [%Trace.call fun {pf} -> pf "from %a" Llair.Reg.pp func.name.reg] ; let unwind formals scope from_call state = Dom.retn formals (Some func.fthrow) from_call @@ -376,7 +382,7 @@ module Make (Dom : Domain_intf.Dom) = struct Stack.t -> Dom.t -> Llair.block - -> Reg.t option + -> Llair.Reg.t option -> Llair.jump -> Work.x = fun stk state block areturn return -> @@ -398,14 +404,15 @@ module Make (Dom : Domain_intf.Dom) = struct | Switch {key; tbl; els} -> IArray.fold tbl ~f:(fun x (case, jump) -> - match Dom.exec_assume state (Exp.eq key case) with + match Dom.exec_assume state (Llair.Exp.eq key case) with | Some state -> exec_jump stk state block jump |> Work.seq x | None -> x ) ~init: ( match Dom.exec_assume state - (IArray.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) -> - Exp.and_ (Exp.dq key case) b )) + (IArray.fold tbl ~init:Llair.Exp.true_ + ~f:(fun b (case, _) -> + Llair.Exp.and_ (Llair.Exp.dq key case) b )) with | Some state -> exec_jump stk state block els | None -> Work.skip ) @@ -413,9 +420,9 @@ module Make (Dom : Domain_intf.Dom) = struct IArray.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) -> match Dom.exec_assume state - (Exp.eq ptr - (Exp.label - ~parent:(Reg.name jump.dst.parent.name.reg) + (Llair.Exp.eq ptr + (Llair.Exp.label + ~parent:(Llair.Reg.name jump.dst.parent.name.reg) ~name:jump.dst.lbl)) with | Some state -> exec_jump stk state block jump |> Work.seq x @@ -497,9 +504,10 @@ module Make (Dom : Domain_intf.Dom) = struct | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound) | None -> fail "no applicable harness" () - let compute_summaries opts pgm : Dom.summary list Reg.Map.t = + let compute_summaries opts pgm : Dom.summary list Llair.Reg.Map.t = assert opts.function_summaries ; exec_pgm opts pgm ; - Hashtbl.fold summary_table ~init:Reg.Map.empty ~f:(fun ~key ~data map -> - match data with [] -> map | _ -> Reg.Map.set map ~key ~data ) + Hashtbl.fold summary_table ~init:Llair.Reg.Map.empty + ~f:(fun ~key ~data map -> + match data with [] -> map | _ -> Llair.Reg.Map.set map ~key ~data ) end diff --git a/sledge/src/control.mli b/sledge/src/control.mli index 5b6500cac..a528e59e0 100644 --- a/sledge/src/control.mli +++ b/sledge/src/control.mli @@ -18,5 +18,5 @@ module Make (Dom : Domain_intf.Dom) : sig val exec_pgm : exec_opts -> Llair.program -> unit val compute_summaries : - exec_opts -> Llair.program -> Dom.summary list Reg.Map.t + exec_opts -> Llair.program -> Dom.summary list Llair.Reg.Map.t end diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index c141175be..b2e01a488 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -11,41 +11,41 @@ module type Dom = sig val pp : t pp val report_fmt_thunk : t -> Formatter.t -> unit - val init : Global.t iarray -> t + val init : Llair.Global.t iarray -> t val join : t -> t -> t option val is_false : t -> bool val dnf : t -> t list - val exec_assume : t -> Exp.t -> t option - val exec_kill : t -> Reg.t -> t - val exec_move : t -> (Reg.t * Exp.t) iarray -> t + val exec_assume : t -> Llair.Exp.t -> t option + val exec_kill : t -> Llair.Reg.t -> t + val exec_move : t -> (Llair.Reg.t * Llair.Exp.t) iarray -> t val exec_inst : t -> Llair.inst -> t option val exec_intrinsic : skip_throw:bool -> t - -> Reg.t option - -> Reg.t - -> Exp.t list + -> Llair.Reg.t option + -> Llair.Reg.t + -> Llair.Exp.t list -> t option option type from_call [@@deriving sexp_of] val call : summaries:bool - -> globals:Reg.Set.t - -> actuals:Exp.t list - -> areturn:Reg.t option - -> formals:Reg.t list - -> freturn:Reg.t option - -> locals:Reg.Set.t + -> globals:Llair.Reg.Set.t + -> actuals:Llair.Exp.t list + -> areturn:Llair.Reg.t option + -> formals:Llair.Reg.t list + -> freturn:Llair.Reg.t option + -> locals:Llair.Reg.Set.t -> t -> t * from_call - val post : Reg.Set.t -> from_call -> t -> t - val retn : Reg.t list -> Reg.t option -> from_call -> t -> t + val post : Llair.Reg.Set.t -> from_call -> t -> t + val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t val resolve_callee : - (string -> Llair.func list) -> Exp.t -> t -> Llair.func list * t + (string -> Llair.func list) -> Llair.Exp.t -> t -> Llair.func list * t val recursion_beyond_bound : [`skip | `prune] @@ -54,7 +54,7 @@ module type Dom = sig val pp_summary : summary pp val create_summary : - locals:Reg.Set.t -> formals:Reg.Set.t -> t -> summary * t + locals:Llair.Reg.Set.t -> formals:Llair.Reg.Set.t -> t -> summary * t val apply_summary : t -> summary -> t option end diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml index a582a663b..3f5069cb1 100644 --- a/sledge/src/domain_relation.ml +++ b/sledge/src/domain_relation.ml @@ -12,8 +12,8 @@ module type State_domain_sig = sig include Domain_intf.Dom val create_summary : - locals:Reg.Set.t - -> formals:Reg.Set.t + locals:Llair.Reg.Set.t + -> formals:Llair.Reg.Set.t -> entry:t -> current:t -> summary * t @@ -76,8 +76,10 @@ module Make (State_domain : State_domain_sig) = struct pf "@[@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \ globals: {@[%a@]}@ current: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp) - (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals + (List.pp ",@ " Llair.Exp.pp) + (List.rev actuals) + (List.pp ",@ " Llair.Reg.pp) + (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals State_domain.pp current] ; let caller_current, state_from_call = @@ -90,7 +92,7 @@ module Make (State_domain : State_domain_sig) = struct [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln] let post locals {state_from_call; caller_entry} (_, current) = - [%Trace.call fun {pf} -> pf "locals: %a" Reg.Set.pp locals] + [%Trace.call fun {pf} -> pf "locals: %a" Llair.Reg.Set.pp locals] ; (caller_entry, State_domain.post locals state_from_call current) |> diff --git a/sledge/src/domain_relation.mli b/sledge/src/domain_relation.mli index f12bc9bd9..957abc1ae 100644 --- a/sledge/src/domain_relation.mli +++ b/sledge/src/domain_relation.mli @@ -12,8 +12,8 @@ module type State_domain_sig = sig include Domain_intf.Dom val create_summary : - locals:Reg.Set.t - -> formals:Reg.Set.t + locals:Llair.Reg.Set.t + -> formals:Llair.Reg.Set.t -> entry:t -> current:t -> summary * t diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index f7fcfdd6e..e7ff3872d 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -18,7 +18,7 @@ let simplify q = if !simplify_states then Sh.simplify q else q let init globals = IArray.fold globals ~init:Sh.emp ~f:(fun q -> function - | {Global.reg; init= Some (arr, siz)} -> + | {Llair.Global.reg; init= Some (arr, siz)} -> let loc = Term.var (Var.of_reg reg) in let len = Term.integer (Z.of_int siz) in let arr = Term.of_exp arr in @@ -129,7 +129,7 @@ let localize_entry globals actuals formals freturn locals subst pre entry = (* Add the formals here to do garbage collection and then get rid of them *) let formals_set = Var.Set.of_list formals in let freturn_locals = - Var.Set.of_regs (Reg.Set.add_option freturn locals) + Var.Set.of_regs (Llair.Reg.Set.add_option freturn locals) in let function_summary_pre = garbage_collect entry @@ -159,14 +159,17 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q = pf "@[actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \ globals: {@[%a@]}@ q: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp) - (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals pp q] + (List.pp ",@ " Llair.Exp.pp) + (List.rev actuals) + (List.pp ",@ " Llair.Reg.pp) + (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals pp + q] ; let actuals = List.map ~f:Term.of_exp actuals in let areturn = Option.map ~f:Var.of_reg areturn in let formals = List.map ~f:Var.of_reg formals in let freturn_locals = - Var.Set.of_regs (Reg.Set.add_option freturn locals) + Var.Set.of_regs (Llair.Reg.Set.add_option freturn locals) in let modifs = Var.Set.of_option areturn in (* quantify modifs, their current value will be overwritten and so does @@ -200,7 +203,7 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q = (** Leave scope of locals: existentially quantify locals. *) let post locals _ q = [%Trace.call fun {pf} -> - pf "@[locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q] + pf "@[locals: {@[%a@]}@ q: %a@]" Llair.Reg.Set.pp locals Sh.pp q] ; Sh.exists (Var.Set.of_regs locals) q |> simplify |> @@ -212,8 +215,9 @@ let post locals _ q = let retn formals freturn {areturn; subst; frame} q = [%Trace.call fun {pf} -> pf "@[formals: {@[%a@]}%a%a@ subst: %a@ q: %a@ frame: %a@]" - (List.pp ", " Reg.pp) formals - (Option.pp "@ freturn: %a" Reg.pp) + (List.pp ", " Llair.Reg.pp) + formals + (Option.pp "@ freturn: %a" Llair.Reg.pp) freturn (Option.pp "@ areturn: %a" Var.pp) areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] @@ -247,8 +251,8 @@ let retn formals freturn {areturn; subst; frame} q = [%Trace.retn fun {pf} -> pf "%a" pp] let resolve_callee lookup ptr q = - match Reg.of_exp ptr with - | Some callee -> (lookup (Reg.name callee), q) + match Llair.Reg.of_exp ptr with + | Some callee -> (lookup (Llair.Reg.name callee), q) | None -> ([], q) let recursion_beyond_bound = `prune @@ -261,8 +265,8 @@ let pp_summary fs {xs; foot; post} = let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = [%Trace.call fun {pf} -> - pf "formals %a@ entry: %a@ current: %a" Reg.Set.pp formals pp entry pp - post] + pf "formals %a@ entry: %a@ current: %a" Llair.Reg.Set.pp formals pp + entry pp post] ; let locals = Var.Set.of_regs locals in let formals = Var.Set.of_regs formals in diff --git a/sledge/src/domain_sh.mli b/sledge/src/domain_sh.mli index 362d8257e..e832aa8e7 100644 --- a/sledge/src/domain_sh.mli +++ b/sledge/src/domain_sh.mli @@ -12,8 +12,8 @@ include Domain_intf.Dom (* formals should include all the parameters of the summary. That is both formals and globals. *) val create_summary : - locals:Reg.Set.t - -> formals:Reg.Set.t + locals:Llair.Reg.Set.t + -> formals:Llair.Reg.Set.t -> entry:t -> current:t -> summary * t diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml index 236449b92..eb46f7372 100644 --- a/sledge/src/domain_unit.ml +++ b/sledge/src/domain_unit.ml @@ -32,8 +32,8 @@ let retn _ _ _ _ = () let dnf () = [()] let resolve_callee lookup ptr _ = - match Reg.of_exp ptr with - | Some callee -> (lookup (Reg.name callee), ()) + match Llair.Reg.of_exp ptr with + | Some callee -> (lookup (Llair.Reg.name callee), ()) | None -> ([], ()) type summary = unit diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 1f1653f74..b3839e804 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -7,26 +7,28 @@ (** Used-globals abstract domain *) -type t = Reg.Set.t [@@deriving equal, sexp] +type t = Llair.Reg.Set.t [@@deriving equal, sexp] -let pp = Reg.Set.pp +let pp = Llair.Reg.Set.pp let report_fmt_thunk = Fn.flip pp -let empty = Reg.Set.empty +let empty = Llair.Reg.Set.empty let init globals = - [%Trace.info "pgm globals: {%a}" (IArray.pp ", " Global.pp) globals] ; + [%Trace.info "pgm globals: {%a}" (IArray.pp ", " Llair.Global.pp) globals] ; empty -let join l r = Some (Reg.Set.union l r) +let join l r = Some (Llair.Reg.Set.union l r) let recursion_beyond_bound = `skip let is_false _ = false let post _ _ state = state -let retn _ _ from_call post = Reg.Set.union from_call post +let retn _ _ from_call post = Llair.Reg.Set.union from_call post let dnf t = [t] -let add_if_global gs v = if Reg.is_global v then Reg.Set.add gs v else gs + +let add_if_global gs v = + if Llair.Reg.is_global v then Llair.Reg.Set.add gs v else gs let used_globals ?(init = empty) exp = - Exp.fold_regs exp ~init ~f:add_if_global + Llair.Exp.fold_regs exp ~init ~f:add_if_global let exec_assume st exp = Some (used_globals ~init:st exp) let exec_kill st _ = st @@ -46,7 +48,7 @@ let exec_inst st inst = Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)] let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals = - let name = Reg.name intrinsic in + let name = Llair.Reg.name intrinsic in if List.exists [ "malloc" @@ -84,8 +86,8 @@ let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_ let resolve_callee lookup ptr st = let st = used_globals ~init:st ptr in - match Reg.of_exp ptr with - | Some callee -> (lookup (Reg.name callee), st) + match Llair.Reg.of_exp ptr with + | Some callee -> (lookup (Llair.Reg.name callee), st) | None -> ([], st) (* A function summary is the set of global registers accessed by that @@ -94,25 +96,27 @@ type summary = t let pp_summary = pp let create_summary ~locals:_ ~formals:_ state = (state, state) -let apply_summary st summ = Some (Reg.Set.union st summ) +let apply_summary st summ = Some (Llair.Reg.Set.union st summ) (** Query *) -type r = Per_function of Reg.Set.t Reg.Map.t | Declared of Reg.Set.t +type r = + | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t + | Declared of Llair.Reg.Set.t -let by_function : r -> Reg.t -> t = +let by_function : r -> Llair.Reg.t -> t = fun s fn -> - [%Trace.call fun {pf} -> pf "%a" Reg.pp fn] + [%Trace.call fun {pf} -> pf "%a" Llair.Reg.pp fn] ; ( match s with | Declared set -> set | Per_function map -> ( - match Reg.Map.find map fn with + match Llair.Reg.Map.find map fn with | Some gs -> gs | None -> fail "main analysis reached function %a that was not reached by \ used-globals pre-analysis " - Reg.pp fn () ) ) + Llair.Reg.pp fn () ) ) |> - [%Trace.retn fun {pf} r -> pf "%a" Reg.Set.pp r] + [%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r] diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli index 81bdc3b21..e858a03ec 100644 --- a/sledge/src/domain_used_globals.mli +++ b/sledge/src/domain_used_globals.mli @@ -7,11 +7,11 @@ (** Used-globals abstract domain *) -include Domain_intf.Dom with type summary = Reg.Set.t +include Domain_intf.Dom with type summary = Llair.Reg.Set.t type r = - | Per_function of Reg.Set.t Reg.Map.t + | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t (** per-function used-globals map *) - | Declared of Reg.Set.t (** program-wide set *) + | Declared of Llair.Reg.Set.t (** program-wide set *) -val by_function : r -> Reg.t -> summary +val by_function : r -> Llair.Reg.t -> summary diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index a40443b11..77a7f8b73 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -317,7 +317,7 @@ let calloc_spec us reg num len = let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in {xs; foot; sub; ms; post} -let size_of_ptr = Term.integer (Z.of_int (Typ.size_of Typ.ptr)) +let size_of_ptr = Term.integer (Z.of_int Llair.Typ.(size_of ptr)) (* { p-[_;_)->⟨W,_⟩ } * posix_memalign r p s @@ -490,7 +490,7 @@ let nallocx_spec us reg siz = {xs; foot; sub; ms; post} let size_of_int_mul = - Term.mul (Term.integer (Z.of_int (Typ.size_of Typ.siz))) + Term.mul (Term.integer (Z.of_int Llair.Typ.(size_of siz))) (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 } * mallctl r i w n diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index a0435bf1b..31fd3e820 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -9,6 +9,12 @@ [@@@warning "+9"] +module Loc = Loc +module Typ = Typ +module Reg = Reg +module Exp = Exp +module Global = Global + type inst = | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t} | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t} diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 12a180297..6dcf284b7 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -8,6 +8,12 @@ (** LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for static analysis using a low-level model of memory. *) +module Loc = Loc +module Typ = Typ +module Reg = Reg +module Exp = Exp +module Global = Global + (** Instructions for memory manipulation or other non-control effects. *) type inst = private | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t} diff --git a/sledge/src/report.ml b/sledge/src/report.ml index df0ea6a01..2555ca8ce 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -11,14 +11,14 @@ let unknown_call call = [%Trace.kprintf Stop.on_unknown_call "@\n@[%a Unknown function call %a@;<1 2>@[%a@]@]@." - (fun fs call -> Loc.pp fs (Llair.Term.loc call)) + (fun fs call -> Llair.Loc.pp fs (Llair.Term.loc call)) call (fun fs (call : Llair.Term.t) -> match call with | Call {callee} -> ( - match Reg.of_exp callee with - | Some reg -> Reg.pp_demangled fs reg - | None -> Exp.pp fs callee ) + match Llair.Reg.of_exp callee with + | Some reg -> Llair.Reg.pp_demangled fs reg + | None -> Llair.Exp.pp fs callee ) | _ -> () ) call Llair.Term.pp call] @@ -28,7 +28,7 @@ let invalid_access_count () = !count let invalid_access fmt_thunk pp access loc = Int.incr count ; let rep fs = - Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp + Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Llair.Loc.pp (loc access) pp access in Format.printf "@\n@[%t@]@." rep ; diff --git a/sledge/src/term.ml b/sledge/src/term.ml index cd6adce02..c7547f843 100644 --- a/sledge/src/term.ml +++ b/sledge/src/term.ml @@ -12,7 +12,7 @@ type op1 = | Signed of {bits: int} | Unsigned of {bits: int} - | Convert of {src: Typ.t; dst: Typ.t} + | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t} | Splat | Select of int [@@deriving compare, equal, hash, sexp] @@ -155,7 +155,7 @@ let rec ppx strength fs term = | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg | Ap1 (Convert {src; dst}, arg) -> - pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg + pf "((%a)(%a)@ %a)" Llair.Typ.pp dst Llair.Typ.pp src pp arg | Ap2 (Eq, x, y) -> pf "(%a@ = %a)" pp x pp y | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y | Ap2 (Lt, x, y) -> pf "(%a@ < %a)" pp x pp y @@ -310,10 +310,11 @@ let invariant e = | ApN (Record, elts) -> assert (not (IArray.is_empty elts)) | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false | Ap1 (Convert {src; dst}, _) -> - assert (Typ.convertible src dst) ; + assert (Llair.Typ.convertible src dst) ; assert ( - not (Typ.equivalent src dst) (* avoid redundant representations *) - ) + not + (Llair.Typ.equivalent src dst) + (* avoid redundant representations *) ) | Rational {data} -> assert (Q.is_real data) ; assert (not (Z.equal Z.one (Q.den data))) @@ -940,7 +941,8 @@ let signed bits term = norm1 (Signed {bits}) term let unsigned bits term = norm1 (Unsigned {bits}) term let convert src ~to_:dst arg = - if Typ.equivalent src dst then arg else norm1 (Convert {src; dst}) arg + if Llair.Typ.equivalent src dst then arg + else norm1 (Convert {src; dst}) arg let eq = norm2 Eq let dq = norm2 Dq @@ -982,11 +984,11 @@ let eq_concat (siz, arr) ms = let rec binary mk x y = mk (of_exp x) (of_exp y) and ubinary mk typ x y = - let unsigned typ = unsigned (Typ.bit_size_of typ) in + let unsigned typ = unsigned (Llair.Typ.bit_size_of typ) in mk (unsigned typ (of_exp x)) (unsigned typ (of_exp y)) and of_exp e = - match (e : Exp.t) with + match (e : Llair.Exp.t) with | Reg {name; global; typ= _} -> Var {name; id= (if global then -1 else 0)} | Nondet {msg; typ= _} -> nondet msg | Label {parent; name} -> label ~parent ~name @@ -1050,9 +1052,9 @@ module Var = struct | _ -> None let of_reg r = - match of_term (of_exp (r : Reg.t :> Exp.t)) with + match of_term (of_exp (r : Llair.Reg.t :> Llair.Exp.t)) with | Some v -> v - | _ -> violates Reg.invariant r + | _ -> violates Llair.Reg.invariant r let fresh name ~wrt = let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in @@ -1073,7 +1075,8 @@ module Var = struct if not (is_empty xs) then Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs - let of_regs = Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) + let of_regs = + Llair.Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) end (** Variable renaming substitutions *) diff --git a/sledge/src/term.mli b/sledge/src/term.mli index 39fe77097..5e78b963c 100644 --- a/sledge/src/term.mli +++ b/sledge/src/term.mli @@ -19,7 +19,7 @@ type op1 = (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit unsigned integer. That is, it unsigned-binary--decodes the low [n] bits of the infinite two's-complement encoding of [arg]. *) - | Convert of {src: Typ.t; dst: Typ.t} + | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t} (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src] to type [dst], possibly with loss of information. The [src] and [dst] types must be [Typ.convertible] and must not both be @@ -118,7 +118,7 @@ module Var : sig val ppx : strength -> t pp val pp : t pp val pp_xs : t pp - val of_regs : Reg.Set.t -> t + val of_regs : Llair.Reg.Set.t -> t end val pp : t pp @@ -129,7 +129,7 @@ module Var : sig val id : t -> int val of_ : term -> t val of_term : term -> t option - val of_reg : Reg.t -> t + val of_reg : Llair.Reg.t -> t val fresh : string -> wrt:Set.t -> t * Set.t val identified : name:string -> id:int -> t @@ -189,7 +189,7 @@ val float : string -> t (* type conversions *) val signed : int -> t -> t val unsigned : int -> t -> t -val convert : Typ.t -> to_:Typ.t -> t -> t +val convert : Llair.Typ.t -> to_:Llair.Typ.t -> t -> t (* comparisons *) val eq : t -> t -> t @@ -239,7 +239,7 @@ val update : rcd:t -> idx:int -> elt:t -> t val rec_record : int -> t (* convert *) -val of_exp : Exp.t -> t +val of_exp : Llair.Exp.t -> t (** Transform *) diff --git a/sledge/src/term_test.ml b/sledge/src/term_test.ml index 039f29a4b..82d6da460 100644 --- a/sledge/src/term_test.ml +++ b/sledge/src/term_test.ml @@ -41,49 +41,51 @@ let%test_module _ = let%test "unsigned boolean overflow" = is_true (Term.of_exp - (Exp.uge - (Exp.integer Typ.bool Z.minus_one) - (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool))) + Llair.( + Exp.uge + (Exp.integer Typ.bool Z.minus_one) + (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool))) let pp_exp e = - Format.printf "@\nexp= %a; term= %a@." Exp.pp e Term.pp + Format.printf "@\nexp= %a; term= %a@." Llair.Exp.pp e Term.pp (Term.of_exp e) - let ( !! ) i = Exp.integer Typ.siz (Z.of_int i) + let ( !! ) i = Llair.(Exp.integer Typ.siz (Z.of_int i)) let%expect_test _ = - pp_exp (Exp.signed 1 !!1 ~to_:Typ.bool) ; + pp_exp Llair.(Exp.signed 1 !!1 ~to_:Typ.bool) ; [%expect {| exp= ((i1)(s1) 1); term= -1 |}] let%expect_test _ = - pp_exp (Exp.unsigned 1 !!(-1) ~to_:Typ.byt) ; + pp_exp Llair.(Exp.unsigned 1 !!(-1) ~to_:Typ.byt) ; [%expect {| exp= ((i8)(u1) -1); term= 1 |}] let%expect_test _ = - pp_exp (Exp.signed 8 !!(-1) ~to_:Typ.int) ; + pp_exp Llair.(Exp.signed 8 !!(-1) ~to_:Typ.int) ; [%expect {| exp= ((i32)(s8) -1); term= -1 |}] let%expect_test _ = - pp_exp (Exp.unsigned 8 !!(-1) ~to_:Typ.int) ; + pp_exp Llair.(Exp.unsigned 8 !!(-1) ~to_:Typ.int) ; [%expect {| exp= ((i32)(u8) -1); term= 255 |}] let%expect_test _ = - pp_exp (Exp.signed 8 !!255 ~to_:Typ.byt) ; + pp_exp Llair.(Exp.signed 8 !!255 ~to_:Typ.byt) ; [%expect {| exp= ((i8)(s8) 255); term= -1 |}] let%expect_test _ = - pp_exp (Exp.signed 7 !!255 ~to_:Typ.byt) ; + pp_exp Llair.(Exp.signed 7 !!255 ~to_:Typ.byt) ; [%expect {| exp= ((i8)(s7) 255); term= -1 |}] let%expect_test _ = - pp_exp (Exp.unsigned 7 !!255 ~to_:Typ.byt) ; + pp_exp Llair.(Exp.unsigned 7 !!255 ~to_:Typ.byt) ; [%expect {| exp= ((i8)(u7) 255); term= 127 |}] let%expect_test _ = pp_exp - (Exp.uge - (Exp.integer Typ.bool Z.minus_one) - (Exp.signed 1 !!1 ~to_:Typ.bool)) ; + Llair.( + Exp.uge + (Exp.integer Typ.bool Z.minus_one) + (Exp.signed 1 !!1 ~to_:Typ.bool)) ; [%expect {| exp= (-1 u≥ ((i1)(s1) 1)); term= -1 |}] let%expect_test _ =