[sledge] Add LLAIR expression form for function names

Summary:
Distinguish expressions that name functions from registers. This leads
to clearer code, and function names are semantically distinct from
general registers. In particular, they are constant, so any machinery
for handling assignment does not need to consider them. Unlike general
globals, they never have initializer expressions, and in particular
not recursive initializers. This diff only adds the distinction to
LLAIR, it is not pushed through to FOL, which will come later.

Reviewed By: jvillard

Differential Revision: D24846672

fbshipit-source-id: 2101f353f
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 60eed3fbad
commit 55dfce6f88

@ -65,7 +65,8 @@ let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function
let rec apron_texpr_of_llair_exp exp q =
match (exp : Llair.Exp.t) with
| Reg {name} -> Some (Texpr1.Var (apron_var_of_name name))
| Reg {name} | Function {name} ->
Some (Texpr1.Var (apron_var_of_name name))
| Integer {data} -> Some (Texpr1.Cst (Coeff.s_of_int (Z.to_int data)))
| Float {data} -> (
match Float.of_string_exn data with
@ -198,7 +199,7 @@ let exec_inst i q =
(** Treat any intrinsic function as havoc on the return register [aret] *)
let exec_intrinsic ~skip_throw:_ aret i _ pre =
let name = Llair.Reg.name i in
let name = Llair.Function.name i in
if
List.exists
[ "malloc"
@ -302,8 +303,8 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
let dnf q = [q]
let resolve_callee lookup ptr q =
match Llair.Reg.of_exp ptr with
| Some callee -> (lookup (Llair.Reg.name callee), q)
match Llair.Function.of_exp ptr with
| Some callee -> (lookup callee, q)
| None -> ([], q)
type summary = t

@ -18,7 +18,7 @@ let pp_llblock fs t =
Format.pp_print_string fs (Llvm.string_of_llvalue (Llvm.value_of_block t))
;;
Reg.demangle :=
Exp.demangle :=
let open Ctypes in
let cxa_demangle =
(* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
@ -452,7 +452,12 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
| Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
|Argument ->
([], Exp.reg (xlate_name x llv))
| Function | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
| Function ->
( []
, Exp.function_
(Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv))
)
| GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
| GlobalAlias -> xlate_value x (Llvm.operand llv 0)
| ConstantInt -> ([], xlate_int x llv)
| ConstantFP -> ([], xlate_float x llv)
@ -916,7 +921,11 @@ let pp_code fs (insts, term, blocks) =
let rec xlate_func_name x llv =
match Llvm.classify_value llv with
| Function | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
| Function ->
( []
, Exp.function_
(Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv)) )
| GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
| ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
| Argument | Instruction _ -> xlate_value x llv
| GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@ -1424,21 +1433,23 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
let report_undefined func name =
if Option.is_some (Llvm.use_begin func) then
[%Trace.info "undefined function: %a" Global.pp name]
[%Trace.info "undefined function: %a" Function.pp name]
let xlate_function : x -> Llvm.llvalue -> Llair.func =
fun x llf ->
[%Trace.call fun {pf} -> pf "%a" pp_llvalue llf]
;
undef_count := 0 ;
let name = xlate_global x llf in
let loc = find_loc llf in
let typ = xlate_type x (Llvm.type_of llf) in
let name = Function.mk typ (find_name llf) in
let formals =
Llvm.fold_left_params
(fun rev_args param -> xlate_name x param :: rev_args)
[] llf
in
let freturn =
match Reg.typ name.reg with
match typ with
| Pointer {elt= Function {return= Some typ; _}} ->
Some (Reg.program typ "freturn")
| _ -> None
@ -1466,10 +1477,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
in
trav_blocks (List.rev entry_blocks) entry_blk
in
Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg
Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc
| At_end _ ->
report_undefined llf name ;
Func.mk_undefined ~name ~formals ~freturn ~fthrow )
Func.mk_undefined ~name ~formals ~freturn ~fthrow ~loc )
|>
[%Trace.retn fun {pf} -> pf "@\n%a" Func.pp]

@ -75,6 +75,14 @@ let unmarshal file () =
~f:(fun ic -> (Marshal.from_channel ic : Llair.program))
file
let entry_points =
let void_to_void =
Llair.Typ.pointer
~elt:(Llair.Typ.function_ ~args:IArray.empty ~return:None)
in
List.map (Config.find_list "entry-points") ~f:(fun name ->
Llair.Function.mk void_to_void name )
let used_globals pgm preanalyze : Domain_used_globals.r =
if preanalyze then
let summary_table =
@ -82,12 +90,12 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
{ bound= 1
; skip_throw= false
; function_summaries= true
; entry_points= Config.find_list "entry-points"
; entry_points
; globals= Declared Llair.Reg.Set.empty }
pgm
in
Per_function
(Llair.Reg.Map.map summary_table ~f:Llair.Reg.Set.union_list)
(Llair.Function.Map.map summary_table ~f:Llair.Reg.Set.union_list)
else
Declared
(Llair.Reg.Set.of_iter
@ -128,7 +136,6 @@ let analyze =
fun program () ->
let pgm = program () in
let globals = used_globals pgm preanalyze_globals in
let entry_points = Config.find_list "entry-points" in
let skip_throw = not exceptions in
Domain_sh.simplify_states := not no_simplify_states ;
Timer.enabled := stats ;

@ -13,7 +13,7 @@ type exec_opts =
{ bound: int
; skip_throw: bool
; function_summaries: bool
; entry_points: string list
; entry_points: Llair.Function.t list
; globals: Domain_used_globals.r }
module Make (Dom : Domain_intf.Dom) = struct
@ -258,16 +258,14 @@ module Make (Dom : Domain_intf.Dom) = struct
let exec_jump stk state block Llair.{dst; retreating} =
Work.add ~prev:block ~retreating stk state dst
module RegTbl = HashTable.Make (Llair.Reg)
let summary_table = RegTbl.create ()
let summary_table = Llair.Function.Tbl.create ()
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" Llair.Reg.pp name.reg Llair.Reg.pp
return.dst.parent.name.reg Dom.pp state]
pf "%a from %a with state@ %a" Llair.Function.pp name
Llair.Function.pp return.dst.parent.name Dom.pp state]
;
let dnf_states =
if opts.function_summaries then Dom.dnf state else [state]
@ -281,7 +279,7 @@ module Make (Dom : Domain_intf.Dom) = struct
else
let maybe_summary_post =
let state = fst (domain_call ~summaries:false state) in
let* summary = RegTbl.find summary_table name.reg in
let* summary = Llair.Function.Tbl.find summary_table name in
List.find_map ~f:(Dom.apply_summary state) summary
in
[%Trace.info
@ -310,27 +308,26 @@ module Make (Dom : Domain_intf.Dom) = struct
let pp_st () =
[%Trace.printf
"@[<v>%t@]" (fun fs ->
RegTbl.iteri summary_table ~f:(fun ~key ~data ->
Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Reg.pp key
Llair.Function.Tbl.iteri summary_table ~f:(fun ~key ~data ->
Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Function.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" Llair.Reg.pp name.reg]
[%Trace.call fun {pf} -> pf "from: %a" Llair.Function.pp name]
;
let summarize post_state =
if not opts.function_summaries then post_state
else
let globals =
Domain_used_globals.by_function opts.globals name.reg
in
let globals = Domain_used_globals.by_function opts.globals name in
let function_summary, post_state =
Dom.create_summary ~locals post_state
~formals:
(Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals)
in
RegTbl.add_multi ~key:name.reg ~data:function_summary summary_table ;
Llair.Function.Tbl.add_multi ~key:name ~data:function_summary
summary_table ;
pp_st () ;
post_state
in
@ -350,8 +347,7 @@ module Make (Dom : Domain_intf.Dom) = struct
(* Create and store a function summary for main *)
if
opts.function_summaries
&& List.exists opts.entry_points
~f:(String.equal (Llair.Reg.name name.reg))
&& List.exists ~f:(Llair.Function.equal name) opts.entry_points
then summarize exit_state |> (ignore : Dom.t -> unit) ;
Work.skip )
|>
@ -359,7 +355,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" Llair.Reg.pp func.name.reg]
[%Trace.call fun {pf} -> pf "from %a" Llair.Function.pp func.name]
;
let unwind formals scope from_call state =
Dom.retn formals (Some func.fthrow) from_call
@ -424,7 +420,7 @@ module Make (Dom : Domain_intf.Dom) = struct
Dom.exec_assume state
(Llair.Exp.eq ptr
(Llair.Exp.label
~parent:(Llair.Reg.name jump.dst.parent.name.reg)
~parent:(Llair.Function.name jump.dst.parent.name)
~name:jump.dst.lbl))
with
| Some state -> exec_jump stk state block jump |> Work.seq x
@ -440,7 +436,7 @@ module Make (Dom : Domain_intf.Dom) = struct
List.fold callees Work.skip ~f:(fun callee x ->
( match
Dom.exec_intrinsic ~skip_throw:opts.skip_throw areturn
callee.name.reg actuals state
callee.name actuals state
with
| Some None ->
Report.invalid_access_term
@ -454,7 +450,7 @@ module Make (Dom : Domain_intf.Dom) = struct
| None ->
exec_call opts stk state block {call with callee}
(Domain_used_globals.by_function opts.globals
callee.name.reg) )
callee.name) )
|> Work.seq x ) )
| Return {exp} -> exec_return ~opts stk state block exp
| Throw {exc} ->
@ -495,13 +491,13 @@ module Make (Dom : Domain_intf.Dom) = struct
~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions)
opts.entry_points
|> function
| Some {name= {reg}; formals= []; freturn; locals; entry} ->
| Some {name; formals= []; freturn; locals; entry} ->
Some
(Work.init
(fst
(Dom.call ~summaries:opts.function_summaries
~globals:
(Domain_used_globals.by_function opts.globals reg)
(Domain_used_globals.by_function opts.globals name)
~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
(Dom.init pgm.globals)))
entry)
@ -513,9 +509,12 @@ 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 Llair.Reg.Map.t =
let compute_summaries opts pgm : Dom.summary list Llair.Function.Map.t =
assert opts.function_summaries ;
exec_pgm opts pgm ;
RegTbl.fold summary_table Llair.Reg.Map.empty ~f:(fun ~key ~data map ->
match data with [] -> map | _ -> Llair.Reg.Map.add ~key ~data map )
Llair.Function.Tbl.fold summary_table Llair.Function.Map.empty
~f:(fun ~key ~data map ->
match data with
| [] -> map
| _ -> Llair.Function.Map.add ~key ~data map )
end

@ -11,12 +11,12 @@ type exec_opts =
{ bound: int (** Loop/recursion unrolling bound *)
; skip_throw: bool (** Treat throw as unreachable *)
; function_summaries: bool (** Use function summarisation *)
; entry_points: string list
; entry_points: Llair.Function.t list
; globals: Domain_used_globals.r }
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 Llair.Reg.Map.t
exec_opts -> Llair.program -> Dom.summary list Llair.Function.Map.t
end

@ -23,7 +23,7 @@ module type Dom = sig
val exec_intrinsic :
skip_throw:bool
-> Llair.Reg.t option
-> Llair.Reg.t
-> Llair.Function.t
-> Llair.Exp.t list
-> t
-> t option option
@ -45,7 +45,10 @@ module type Dom = sig
val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t
val resolve_callee :
(string -> Llair.func list) -> Llair.Exp.t -> t -> Llair.func list * t
(Llair.Function.t -> Llair.func list)
-> Llair.Exp.t
-> t
-> Llair.func list * t
val recursion_beyond_bound : [`skip | `prune]

@ -69,7 +69,7 @@ let exec_inst inst pre =
|> Option.map ~f:simplify
let exec_intrinsic ~skip_throw r i es q =
Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.reg i)
Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.func i)
(List.map ~f:X.term es)
|> Option.map ~f:(Option.map ~f:simplify)
@ -236,8 +236,8 @@ let retn formals freturn {areturn; unshadow; frame} q =
[%Trace.retn fun {pf} -> pf "%a" pp]
let resolve_callee lookup ptr q =
match Llair.Reg.of_exp ptr with
| Some callee -> (lookup (Llair.Reg.name callee), q)
match Llair.Function.of_exp ptr with
| Some callee -> (lookup callee, q)
| None -> ([], q)
let recursion_beyond_bound = `prune

@ -32,8 +32,8 @@ let retn _ _ _ _ = ()
let dnf () = [()]
let resolve_callee lookup ptr _ =
match Llair.Reg.of_exp ptr with
| Some callee -> (lookup (Llair.Reg.name callee), ())
match Llair.Function.of_exp ptr with
| Some callee -> (lookup callee, ())
| None -> ([], ())
type summary = unit

@ -43,7 +43,7 @@ let exec_inst inst st =
Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
let exec_intrinsic ~skip_throw:_ _ intrinsic actuals st =
let name = Llair.Reg.name intrinsic in
let name = Llair.Function.name intrinsic in
if
List.exists
[ "malloc"
@ -79,8 +79,8 @@ let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
let resolve_callee lookup ptr st =
let st = used_globals ptr st in
match Llair.Reg.of_exp ptr with
| Some callee -> (lookup (Llair.Reg.name callee), st)
match Llair.Function.of_exp ptr with
| Some callee -> (lookup callee, st)
| None -> ([], st)
(* A function summary is the set of global registers accessed by that
@ -94,22 +94,22 @@ let apply_summary st summ = Some (Llair.Reg.Set.union st summ)
(** Query *)
type r =
| Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
| Per_function of Llair.Reg.Set.t Llair.Function.Map.t
| Declared of Llair.Reg.Set.t
let by_function : r -> Llair.Reg.t -> t =
let by_function : r -> Llair.Function.t -> t =
fun s fn ->
[%Trace.call fun {pf} -> pf "%a" Llair.Reg.pp fn]
[%Trace.call fun {pf} -> pf "%a" Llair.Function.pp fn]
;
( match s with
| Declared set -> set
| Per_function map -> (
match Llair.Reg.Map.find fn map with
match Llair.Function.Map.find fn map with
| Some gs -> gs
| None ->
fail
"main analysis reached function %a that was not reached by \
used-globals pre-analysis "
Llair.Reg.pp fn () ) )
Llair.Function.pp fn () ) )
|>
[%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r]

@ -10,8 +10,8 @@
include Domain_intf.Dom with type summary = Llair.Reg.Set.t
type r =
| Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
| Per_function of Llair.Reg.Set.t Llair.Function.Map.t
(** per-function used-globals map *)
| Declared of Llair.Reg.Set.t (** program-wide set *)
val by_function : r -> Llair.Reg.t -> summary
val by_function : r -> Llair.Function.t -> summary

@ -63,6 +63,7 @@ module T = struct
type t =
| Reg of {name: string; global: bool; typ: Typ.t}
| Function of {name: string; typ: Typ.t [@ignore]}
| Label of {parent: string; name: string}
| Integer of {data: Z.t; typ: Typ.t}
| Float of {data: string; typ: Typ.t}
@ -81,6 +82,15 @@ module Set = struct
end
module Map = Map.Make (T)
module Tbl = HashTable.Make (T)
let demangle = ref (fun _ -> None)
let pp_demangled ppf name =
match !demangle name with
| Some demangled when not (String.equal name demangled) ->
Format.fprintf ppf "“%s”" demangled
| _ -> ()
let pp_op2 fs op =
let pf fmt = Format.fprintf fs fmt in
@ -120,6 +130,7 @@ let rec pp fs exp =
match exp with
| Reg {name; global= true} -> pf "%@%s" name
| Reg {name; global= false} -> pf "%%%s" name
| Function {name} -> pf "&%s%a" name pp_demangled name
| Label {name} -> pf "%s" name
| Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
| Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
@ -162,6 +173,8 @@ let rec invariant exp =
let@ () = Invariant.invariant [%here] exp [%sexp_of: t] in
match exp with
| Reg {typ} -> assert (Typ.is_sized typ)
| Function {typ= Pointer {elt= Function _}} -> ()
| Function _ -> assert false
| Integer {data; typ} -> (
match typ with
| Integer {bits} ->
@ -238,7 +251,7 @@ let rec invariant exp =
and typ_of exp =
match exp with
| Reg {typ} | Integer {typ} | Float {typ} -> typ
| Reg {typ} | Function {typ} | Integer {typ} | Float {typ} -> typ
| Label _ -> Typ.ptr
| Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst
| Ap1 (Select idx, typ, _) -> (
@ -277,19 +290,6 @@ module Reg = struct
let pp = Set.pp pp_exp
end
module Map = Map
let demangle = ref (fun _ -> None)
let pp_demangled fs = function
| Reg {name} -> (
match !demangle name with
| Some demangled when not (String.equal name demangled) ->
Format.fprintf fs "“%s”" demangled
| _ -> () )
| _ -> ()
[@@warning "-9"]
let invariant x =
let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
match x with Reg _ -> invariant x | _ -> assert false
@ -297,7 +297,7 @@ module Reg = struct
let name = function Reg x -> x.name | r -> violates invariant r
let typ = function Reg x -> x.typ | r -> violates invariant r
let is_global = function Reg x -> x.global | r -> violates invariant r
let of_ = function Reg _ as r -> r | _ -> invalid_arg "Reg.of_"
let pp_demangled ppf r = pp_demangled ppf (name r)
let of_exp = function
| Reg _ as e -> Some (e |> check invariant)
@ -307,6 +307,28 @@ module Reg = struct
Reg {name; global= Option.is_some global; typ} |> check invariant
end
(** Function names are the expressions constructed by [Function] *)
module Function = struct
include T
let pp = pp
let name = function Function x -> x.name | r -> violates invariant r
let typ = function Function x -> x.typ | r -> violates invariant r
let invariant x =
let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
match x with Function _ -> invariant x | _ -> assert false
let of_exp = function
| Function _ as e -> Some (e |> check invariant)
| _ -> None
let mk typ name = Function {name; typ} |> check invariant
module Map = Map
module Tbl = Tbl
end
(** Construct *)
(* registers *)
@ -315,6 +337,7 @@ let reg x = x
(* constants *)
let function_ f = f
let label ~parent ~name = Label {parent; name} |> check invariant
let integer typ data = Integer {data; typ} |> check invariant
let null = integer Typ.ptr Z.zero

@ -73,6 +73,7 @@ type opN = Record (** Record (array / struct) constant *)
type t = private
| Reg of {name: string; global: bool; typ: Typ.t} (** Virtual register *)
| Function of {name: string; typ: Typ.t [@ignore]} (** Function name *)
| Label of {parent: string; name: string}
(** Address of named code block within parent function *)
| Integer of {data: Z.t; typ: Typ.t} (** Integer constant *)
@ -87,6 +88,8 @@ val pp : t pp
include Invariant.S with type t := t
val demangle : (string -> string option) ref
(** Exp.Reg is re-exported as Reg *)
module Reg : sig
type exp := t
@ -100,15 +103,11 @@ module Reg : sig
val pp : t pp
end
module Map : Map.S with type key := t
val demangle : (string -> string option) ref
val pp : t pp
val pp_demangled : t pp
include Invariant.S with type t := t
val of_ : exp -> t
val of_exp : exp -> t option
val program : ?global:unit -> Typ.t -> string -> t
val name : t -> string
@ -116,12 +115,31 @@ module Reg : sig
val is_global : t -> bool
end
(** Exp.Function is re-exported as Function *)
module Function : sig
type exp := t
type t = private exp [@@deriving compare, equal, hash, sexp]
module Map : Map.S with type key := t
module Tbl : HashTable.S with type key := t
val pp : t pp
include Invariant.S with type t := t
val of_exp : exp -> t option
val mk : Typ.t -> string -> t
val name : t -> string
val typ : t -> Typ.t
end
(** Construct *)
(* registers *)
val reg : Reg.t -> t
(* constants *)
val function_ : Function.t -> t
val label : parent:string -> name:string -> t
val null : t
val bool : bool -> t

@ -0,0 +1,10 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
(** Function names *)
include Exp.Function

@ -0,0 +1,12 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
(** Function names *)
include module type of struct
include Exp.Function
end

@ -13,6 +13,7 @@ module Loc = Loc
module Typ = Typ
module Reg = Reg
module Exp = Exp
module Function = Function
module Global = Global
type inst =
@ -59,12 +60,13 @@ and block =
; mutable sort_index: int }
and func =
{ name: Global.t
{ name: Function.t
; formals: Reg.t list
; freturn: Reg.t option
; fthrow: Reg.t
; locals: Reg.Set.t
; entry: block }
; entry: block
; loc: Loc.t }
let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
match tl with
@ -104,23 +106,24 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
{ lbl: label
; cmnd: cmnd
; term: term
; parent: Reg.t = parent.name.reg
; parent: Function.t = parent.name
; sort_index: int }]
let sexp_of_func {name; formals; freturn; fthrow; locals; entry} =
let sexp_of_func {name; formals; freturn; fthrow; locals; entry; loc} =
[%sexp
{ name: Global.t
{ name: Function.t
; formals: Reg.t list
; freturn: Reg.t option
; fthrow: Reg.t
; locals: Reg.Set.t
; entry: block }]
; entry: block
; loc: Loc.t }]
(* blocks in a [t] are uniquely identified by [sort_index] *)
let compare_block x y = Int.compare x.sort_index y.sort_index
let equal_block x y = Int.equal x.sort_index y.sort_index
type functions = func String.Map.t [@@deriving sexp_of]
type functions = func Function.Map.t [@@deriving sexp_of]
type program = {globals: Global.t iarray; functions: functions}
[@@deriving sexp_of]
@ -219,13 +222,16 @@ let rec dummy_block =
; sort_index= 0 }
and dummy_func =
let dummy_reg = Reg.program ~global:() Typ.ptr "dummy" in
{ name= Global.mk dummy_reg Loc.none
{ name=
Function.mk
(Typ.pointer ~elt:(Typ.function_ ~args:IArray.empty ~return:None))
"dummy"
; formals= []
; freturn= None
; fthrow= dummy_reg
; fthrow= Reg.program Typ.ptr "dummy"
; locals= Reg.Set.empty
; entry= dummy_block }
; entry= dummy_block
; loc= Loc.none }
(** Instructions *)
@ -387,14 +393,14 @@ module Block_label = struct
type t = block [@@deriving sexp_of]
let compare x y =
[%compare: string * Global.t] (x.lbl, x.parent.name)
[%compare: string * Function.t] (x.lbl, x.parent.name)
(y.lbl, y.parent.name)
let equal x y =
[%equal: string * Global.t] (x.lbl, x.parent.name)
[%equal: string * Function.t] (x.lbl, x.parent.name)
(y.lbl, y.parent.name)
let hash b = [%hash: string * Global.t] (b.lbl, b.parent.name)
let hash b = [%hash: string * Function.t] (b.lbl, b.parent.name)
end
include T
@ -403,7 +409,7 @@ end
module BlockS = HashSet.Make (Block_label)
module BlockQ = HashQueue.Make (Block_label)
module FuncQ = HashQueue.Make (Reg)
module FuncQ = HashQueue.Make (Function)
(** Functions *)
@ -437,16 +443,16 @@ module Func = struct
let entry_cfg func = fold_cfg ~f:(fun blk cfg -> blk :: cfg) func []
let pp fs func =
let {name; formals; freturn; entry; _} = func in
let {name; formals; freturn; entry; loc; _} = func in
let {cmnd; term; sort_index; _} = entry in
let pp_if cnd str fs = if cnd then Format.fprintf fs str in
Format.fprintf fs "@[<v>@[<v>%a%a@[<2>%a%a@]%t@]"
(Option.pp "%a " Typ.pp)
( match Reg.typ name.reg with
( match Function.typ name with
| Pointer {elt= Function {return; _}} -> return
| _ -> None )
(Option.pp " %a := " Reg.pp)
freturn Global.pp name (pp_actuals pp_formal) formals
freturn Function.pp name (pp_actuals pp_formal) formals
(fun fs ->
if is_undefined func then Format.fprintf fs " #%i@]" sort_index
else
@ -454,7 +460,7 @@ module Func = struct
List.sort ~cmp:Block.compare (List.tl_exn (entry_cfg func))
in
Format.fprintf fs " { #%i %a@;<1 4>@[<v>%a@ %a@]%t%a@]@ }"
sort_index Loc.pp name.loc pp_cmnd cmnd Term.pp term
sort_index Loc.pp loc pp_cmnd cmnd Term.pp term
(pp_if (not (List.is_empty cfg)) "@ @ ")
(List.pp "@\n@\n " Block.pp)
cfg )
@ -462,7 +468,7 @@ module Func = struct
let invariant func =
assert (func == func.entry.parent) ;
let@ () = Invariant.invariant [%here] func [%sexp_of: t] in
match Reg.typ func.name.reg with
match Function.typ func.name with
| Pointer {elt= Function {return; _}; _} ->
assert (
not
@ -475,9 +481,9 @@ module Func = struct
iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
| _ -> assert false
let find functions name = String.Map.find functions name
let find functions name = Function.Map.find functions name
let mk ~(name : Global.t) ~formals ~freturn ~fthrow ~entry ~cfg =
let mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc =
let locals =
let locals_cmnd locals cmnd =
IArray.fold_right ~f:Inst.union_locals cmnd locals
@ -487,7 +493,7 @@ module Func = struct
in
IArray.fold ~f:locals_block cfg (locals_block entry Reg.Set.empty)
in
let func = {name; formals; freturn; fthrow; locals; entry} in
let func = {name; formals; freturn; fthrow; locals; entry; loc} in
let resolve_parent_and_jumps block =
block.parent <- func ;
let lookup cfg lbl : block =
@ -522,13 +528,13 @@ end
let set_derived_metadata functions =
let compute_roots functions =
let roots = FuncQ.create () in
String.Map.iter functions ~f:(fun func ->
FuncQ.enqueue_back_exn roots func.name.reg func ) ;
String.Map.iter functions ~f:(fun func ->
Function.Map.iter functions ~f:(fun func ->
FuncQ.enqueue_back_exn roots func.name func ) ;
Function.Map.iter functions ~f:(fun func ->
Func.iter_term func ~f:(fun term ->
match term with
| Call {callee; _} -> (
match Reg.of_exp callee with
match Function.of_exp callee with
| Some callee ->
FuncQ.remove roots callee |> (ignore : [> ] -> unit)
| None -> () )
@ -553,8 +559,8 @@ let set_derived_metadata functions =
| Iswitch {tbl; _} -> IArray.iter tbl ~f:jump
| Call ({callee; return; throw; _} as call) ->
( match
let* reg = Reg.of_exp callee in
Func.find (Reg.name reg) functions
let* name = Function.of_exp callee in
Func.find name functions
with
| Some func ->
if Block_label.Set.mem func.entry ancestors then
@ -579,8 +585,8 @@ let set_derived_metadata functions =
index := !index - 1 )
in
let functions =
List.fold functions String.Map.empty ~f:(fun func m ->
String.Map.add_exn ~key:(Reg.name func.name.reg) ~data:func m )
List.fold functions Function.Map.empty ~f:(fun func m ->
Function.Map.add_exn ~key:func.name ~data:func m )
in
let roots = compute_roots functions in
let tips_to_roots = topsort functions roots in
@ -607,7 +613,7 @@ module Program = struct
(IArray.pp "@\n@\n" Global.pp_defn)
globals
(List.pp "@\n@\n" Func.pp)
( String.Map.values functions
( Function.Map.values functions
|> Iter.to_list
|> List.sort ~cmp:(fun x y -> compare_block x.entry y.entry) )
end

@ -12,6 +12,7 @@ module Loc = Loc
module Typ = Typ
module Reg = Reg
module Exp = Exp
module Function = Function
module Global = Global
(** Instructions for memory manipulation or other non-control effects. *)
@ -92,12 +93,13 @@ and block = private
(** A function is a control-flow graph with distinguished entry block, whose
parameters are the function parameters. *)
and func = private
{ name: Global.t
{ name: Function.t
; formals: Reg.t list (** Formal parameters, first-param-last stack *)
; freturn: Reg.t option
; fthrow: Reg.t
; locals: Reg.Set.t (** Local registers *)
; entry: block }
; entry: block
; loc: Loc.t }
type functions
@ -180,25 +182,27 @@ module Func : sig
include Invariant.S with type t := t
val mk :
name:Global.t
name:Function.t
-> formals:Reg.t list
-> freturn:Reg.t option
-> fthrow:Reg.t
-> entry:block
-> cfg:block iarray
-> func
-> loc:Loc.t
-> t
val mk_undefined :
name:Global.t
name:Function.t
-> formals:Reg.t list
-> freturn:Reg.t option
-> fthrow:Reg.t
-> loc:Loc.t
-> t
val find : string -> functions -> func option
val find : Function.t -> functions -> t option
(** Look up a function of the given name in the given functions. *)
val is_undefined : func -> bool
val is_undefined : t -> bool
(** Holds of functions that are declared but not defined. *)
end

@ -9,6 +9,10 @@ open Fol
module T = Term
module F = Formula
let func f =
let name = Llair.Function.name f in
Var.program ~name ~global:true
let reg r =
let name = Llair.Reg.name r in
let global = Llair.Reg.is_global r in
@ -64,6 +68,7 @@ and term : Llair.Exp.t -> T.t =
(F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
(* terms *)
| Reg {name; global; typ= _} -> T.var (Var.program ~name ~global)
| Function {name; typ= _} -> T.var (Var.program ~name ~global:true)
| Label {parent; name} ->
uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
| Integer {typ= _; data} -> T.integer data

@ -7,6 +7,7 @@
open Fol
val func : Llair.Function.t -> Var.t
val reg : Llair.Reg.t -> Var.t
val regs : Llair.Reg.Set.t -> Var.Set.t
val term : Llair.Exp.t -> Term.t

@ -14,12 +14,7 @@ let unknown_call 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 Llair.Reg.of_exp callee with
| Some reg -> Llair.Reg.pp_demangled fs reg
| None -> Llair.Exp.pp fs callee )
| _ -> () )
match call with Call {callee} -> Llair.Exp.pp fs callee | _ -> () )
call Llair.Term.pp call]
let invalid_access_count = ref 0

Loading…
Cancel
Save