From f5c6a5a79decf2dbb797dfc7c86030548c005f24 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 1 Jul 2021 17:35:17 -0700 Subject: [PATCH] [sledge] Add type for instruction pointers and use in Control Summary: In the sequential analysis there is no control-flow within a basic block. This changes in the concurrent analyis as context switches can occur within basic blocks. To support this, this diff adds a notion of "instruction pointer" to Llair and adjusts Control to use it to iterate blocks. Differential Revision: D29441164 fbshipit-source-id: b9c977545 --- sledge/src/control.ml | 38 +++++++++++++++++--------------------- sledge/src/llair/llair.ml | 24 ++++++++++++++++++++---- sledge/src/llair/llair.mli | 14 ++++++++++++-- sledge/src/report.ml | 8 ++++---- sledge/src/report.mli | 2 +- 5 files changed, 54 insertions(+), 32 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 9a10d6857..25705918d 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -650,32 +650,28 @@ module Make (Config : Config) (D : Domain) (Queue : Queue) = struct | Throw {exc} -> exec_throw stk state block exc | Unreachable -> Work.skip - let exec_inst : Llair.block -> Llair.inst -> D.t -> D.t Or_alarm.t = - fun block inst state -> - [%Trace.info "@\n@[%a@]@\n%a" D.pp state Llair.Inst.pp inst] ; - Report.step_inst block inst ; - D.exec_inst inst state + let rec exec_ip : Llair.program -> Stack.t -> D.t -> Llair.ip -> Work.x = + fun pgm stk state ip -> + match Llair.IP.inst ip with + | Some inst -> ( + [%Trace.info "@\n@[%a@]@\n%a" D.pp state Llair.Inst.pp inst] ; + Report.step_inst ip ; + match D.exec_inst inst state with + | Ok state -> + let ip = Llair.IP.succ ip in + exec_ip pgm stk state ip + | Error alarm -> + Report.alarm alarm ; + Work.skip ) + | None -> exec_term pgm stk state (Llair.IP.block ip) let exec_block : Llair.program -> Stack.t -> D.t -> Llair.block -> Work.x = fun pgm stk state block -> [%trace] - ~call:(fun {pf} -> - pf "@ #%i %%%s in %a" block.sort_index block.lbl Llair.Function.pp - block.parent.name ) - ~retn:(fun {pf} _ -> - pf "#%i %%%s in %a" block.sort_index block.lbl Llair.Function.pp - block.parent.name ) - @@ fun () -> - match - Iter.fold_result ~f:(exec_inst block) - (IArray.to_iter block.cmnd) - state - with - | Ok state -> exec_term pgm stk state block - | Error alarm -> - Report.alarm alarm ; - Work.skip + ~call:(fun {pf} -> pf "@ %a" Llair.Block.pp block) + ~retn:(fun {pf} _ -> pf "%a" Llair.Block.pp block) + @@ fun () -> exec_ip pgm stk state (Llair.IP.mk block) let call_entry_point : Llair.program -> Work.t option = fun pgm -> diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index b36a5c926..8c0395932 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -370,10 +370,6 @@ and dummy_func = module Inst = struct type t = inst [@@deriving compare, equal, hash, sexp] - module Tbl = HashTable.Make (struct - type t = block * inst [@@deriving equal, hash] - end) - let pp = pp_inst let move ~reg_exps ~loc = Move {reg_exps; loc} let load ~reg ~ptr ~len ~loc = Load {reg; ptr; len; loc} @@ -538,6 +534,26 @@ module Block = struct ; sort_index= dummy_block.sort_index } end +type ip = {block: block; index: int} [@@deriving equal, hash] + +module IP = struct + type t = ip + + let mk block = {block; index= 0} + let succ {block; index} = {block; index= index + 1} + + let inst {block; index} = + if index < IArray.length block.cmnd then + Some (IArray.get block.cmnd index) + else None + + let block ip = ip.block + + module Tbl = HashTable.Make (struct + type t = ip [@@deriving equal, hash] + end) +end + (* Blocks compared by label, which are unique within a function, used to compute unique sort_index ids *) module Block_label = struct diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index de61bdaf4..1954bd5cf 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -106,6 +106,7 @@ and func = private ; entry: block ; loc: Loc.t } +type ip type functions = func Function.Map.t type program = private @@ -134,8 +135,6 @@ module Inst : sig val loc : inst -> Loc.t val locals : inst -> Reg.Set.t val fold_exps : inst -> 's -> f:(Exp.t -> 's -> 's) -> 's - - module Tbl : HashTable.S with type key := block * t end module Jump : sig @@ -197,6 +196,17 @@ module Block : sig module Tbl : HashTable.S with type key := t end +module IP : sig + type t = ip + + val mk : block -> t + val block : t -> block + val inst : t -> inst option + val succ : t -> t + + module Tbl : HashTable.S with type key := t +end + module Func : sig type t = func [@@deriving compare, equal, hash] diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 00e231928..5d6e179c8 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -33,11 +33,11 @@ let unknown_call call = let solver_steps = ref 0 let step_solver () = Int.incr solver_steps let steps = ref 0 -let hit_insts = Llair.Inst.Tbl.create () +let hit_insts = Llair.IP.Tbl.create () let hit_terms = Llair.Block.Tbl.create () -let step_inst b i = - Llair.Inst.Tbl.incr hit_insts (b, i) ; +let step_inst ip = + Llair.IP.Tbl.incr hit_insts ip ; Int.incr steps let step_term b = @@ -162,7 +162,7 @@ let coverage (pgm : Llair.program) = n + IArray.length blk.cmnd + 1 ) ) in let hit = - Llair.Inst.Tbl.length hit_insts + Llair.Block.Tbl.length hit_terms + Llair.IP.Tbl.length hit_insts + Llair.Block.Tbl.length hit_terms in let fraction = Float.(of_int hit /. of_int size) in output diff --git a/sledge/src/report.mli b/sledge/src/report.mli index 3a3bb4f12..45b6bea41 100644 --- a/sledge/src/report.mli +++ b/sledge/src/report.mli @@ -9,7 +9,7 @@ val init : ?append:bool -> string -> unit val step_solver : unit -> unit -val step_inst : Llair.block -> Llair.inst -> unit +val step_inst : Llair.ip -> unit val step_term : Llair.block -> unit val hit_bound : int -> unit val unknown_call : Llair.term -> unit