diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index e2d513999..53960d34d 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -28,61 +28,6 @@ let expensive_threshold = Itv.Bound.of_int 200 (* CFG module used in several other modules *) module CFG = ProcCfg.Normal -(* Transfer function computing the semantics of the program. - Here semantics means: for each node a pair (env, alias) where - 1. env is an 'environment', i.e. a map from variables to values - 2 alias is an alias map. -*) -module TransferFunctionsSemantics (CFG : ProcCfg.S) = struct - module CFG = CFG - module Domain = CostDomain.SemanticDomain - - let _exec_instr ((env, alias) as astate: Domain.astate) {ProcData.tenv} _ instr = - let astate' = - match instr with - | Sil.Store (lhs, {Typ.desc= Tint _}, rhs, _) -> - let env' = CostDomain.SemanticDomain.update_env env lhs rhs in - let alias' = CostDomain.SemanticDomain.update_alias tenv alias lhs rhs in - (env', alias') - | Sil.Load (id, rhs, {Typ.desc= Tint _}, _) -> - let env' = CostDomain.SemanticDomain.update_env env (Exp.Var id) rhs in - let alias' = CostDomain.SemanticDomain.update_alias tenv alias (Exp.Var id) rhs in - (env', alias') - | Sil.Prune (e, _, _, _) -> ( - match CostDomain.SemanticDomain.sem env e with - | Some e', Some v -> - L.(debug Analysis Medium) "@\n e'= %a, v=%a @\n" Exp.pp e' CostDomain.ItvPureCost.pp v ; - let v' = - match CostDomain.EnvDomain.find_opt e' env with - | Some v_pre -> - L.(debug Analysis Medium) "@\n>>>Starting meet 2 \n" ; - let meet = CostDomain.ItvPureCost.meet v_pre v in - L.(debug Analysis Medium) - "@\n>>> Result Meet v_pre= %a e_val= %a --> %a\n" CostDomain.ItvPureCost.pp - v_pre CostDomain.ItvPureCost.pp v CostDomain.ItvPureCost.pp meet ; - if CostDomain.ItvPureCost.is_empty meet then v else meet - | None -> - v - in - let env' = CostDomain.EnvDomain.add e' v' env in - L.(debug Analysis Medium) - "@\n e'= %a, v'=%a @\n" Exp.pp e' CostDomain.ItvPureCost.pp v' ; - let env'' = CostDomain.SemanticDomain.update_alias_env env' alias e' in - (env'', alias) - | _ -> - (env, alias) ) - | Sil.Load _ - | Sil.Store _ - | Sil.Call _ - | Sil.Declare_locals _ - | Remove_temps _ - | Abstract _ - | Nullify _ -> - astate - in - astate' -end - (* Map associating to each node a bound on the number of times it can be executed. This bound is computed using environments (map: val -> values), using the following observation: the number of environments associated with a program point is an upperbound diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 5cc36810e..f74e7079f 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -12,22 +12,6 @@ module F = Format module L = Logging open AbstractDomain.Types -module Alias = struct - type astate = Prop.pi - - let pp = Prop.pp_pi Pp.text - - let join pi1 pi2 = pi1 @ pi2 - - let widen ~prev ~next:_ ~num_iters:_ = prev - - (* DINO: ??? what should be this one?*) - - let ( <= ) ~lhs:_ ~rhs:_ = true - - (*DINO: ???? what should be this one?*) -end - module IntCost = struct type astate = int [@@deriving compare] @@ -63,58 +47,6 @@ module Cost = struct Int.( <= ) c1 c2 - let plus c1 c2 = - match (c1, c2) with - | Top, _ -> - Top - | _, Top -> - Top - | NonTop c1', NonTop c2' -> - NonTop (c1' + c2') - - - let _minus c1 c2 = - match (c1, c2) with - | Top, _ -> - Top - | _, Top -> - assert false (* ????? *) - | NonTop c1', NonTop c2' -> - NonTop (c1' - c2') - - - let _mult c1 c2 = - match (c1, c2) with Top, _ | _, Top -> Top | NonTop c1', NonTop c2' -> NonTop (c1' * c2') - - - let min c1 c2 = - match (c1, c2) with - | Top, _ -> - c2 - | _, Top -> - c1 - | NonTop c1', NonTop c2' -> - NonTop (Int.min c1' c2') - - - let max c1 c2 = - match (c1, c2) with - | Top, _ | _, Top -> - Top - | NonTop c1', NonTop c2' -> - NonTop (Int.max c1' c2') - - - let _one = NonTop 1 - - let zero = NonTop 0 - - let nth n = NonTop n - - let dec n = match n with NonTop n' -> NonTop (n' - 1) | _ -> n - - let inc n = match n with NonTop n' -> NonTop (n' + 1) | _ -> n - let pp_l fmt c = let c'' = match c with Top -> Top | NonTop c' -> NonTop (-c') in pp fmt c'' @@ -123,8 +55,6 @@ module Cost = struct let pp_u = pp end -module CostSingleIteration = Cost - module IntPair = struct (* Represents node id,instr index within node *) include AbstractDomain.Pair (IntCost) (IntCost) @@ -147,17 +77,6 @@ module ItvPureCost = struct let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Cost.join l1 l2, Cost.join u1 u2) - let meet (l1, u1) (l2, u2) = - let l = match (l1, l2) with Top, _ -> l2 | _, Top -> l1 | _, _ -> Cost.max l1 l2 in - L.(debug Analysis Medium) - "@\n l1= %a, l2=%a l/max=%a @\n" Cost.pp_l l1 Cost.pp_l l2 Cost.pp_l l ; - (* l1 l2 are negative so we use min instead of max *) - let u = Cost.min u1 u2 in - L.(debug Analysis Medium) - "@\n u1= %a, u2=%a u/min=%a @\n" Cost.pp_u u1 Cost.pp_u u2 Cost.pp_u u ; - (l, u) - - let widen : prev:t -> next:t -> num_iters:int -> t = fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters -> (Cost.widen ~prev:l1 ~next:l2 ~num_iters, Cost.widen ~prev:u1 ~next:u2 ~num_iters) @@ -165,189 +84,11 @@ module ItvPureCost = struct let pp : F.formatter -> t -> unit = fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Cost.pp_l l Cost.pp_u u - - - let of_int n = (Cost.nth (-n), Cost.nth n) - - let of_int_lit i = of_int (IntLit.to_int i) - - (* range [-a,b] = (b+a+1) *) - let range (l, u) = Cost.inc (Cost.plus u l) - - let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Cost.plus l1 l2, Cost.plus u1 u2) - - (* a const interval is of type [-n,n] *) - let is_const (l, u) = - match (l, u) with NonTop l', NonTop u' -> Int.equal (-l') u' | _, _ -> false - - - let is_empty itv = Cost.( <= ) ~lhs:(range itv) ~rhs:Cost.zero - - let negation (u, l) = (l, u) end module EnvDomain = AbstractDomain.Map (Exp) (ItvPureCost) module EnvDomainBO = AbstractDomain.Map (Exp) (Itv) -module SemanticDomain = struct - include AbstractDomain.Pair (EnvDomain) (Alias) - - let get_val env e = - match e with - | Exp.Var _ | Exp.Lvar _ -> ( - match EnvDomain.find_opt e env with - | Some c -> - c - | None -> - L.(debug Analysis Medium) - " @\n[WARNING:] Expression %a not found on env. Returning zero@\n" Exp.pp e ; - ItvPureCost.of_int 0 ) - | Exp.Const Cint i -> - ItvPureCost.of_int (IntLit.to_int i) - | _ -> - L.(debug Analysis Medium) " @\n[WARNING:] Returning value zero for %a @\n" Exp.pp e ; - ItvPureCost.of_int 0 - - - let eval_bin_op op val1 val2 = - match op with Binop.PlusA -> ItvPureCost.plus val1 val2 | _ -> assert false - - - let update_env env lhs rhs = - let open Exp in - match rhs with - | Var _ | UnOp _ -> - env - | BinOp (op, e1, e2) -> - let val1 = get_val env e1 in - let val2 = get_val env e2 in - let res = eval_bin_op op val1 val2 in - L.(debug Analysis Medium) - " @\n #### Operation: %a val1= %a val2=%a res = %a@\n" Exp.pp rhs ItvPureCost.pp - val1 ItvPureCost.pp val2 ItvPureCost.pp res ; - L.(debug Analysis Medium) - " @\nAdding binding %a --> %a to env o@\n" Exp.pp lhs ItvPureCost.pp res ; - EnvDomain.add lhs res env - | Const Cint i -> - (*let lhs_var = Var.of_pvar lhs in*) - let itv = ItvPureCost.of_int_lit i in - EnvDomain.add lhs itv env - | Lvar _ -> - let val_rhs = get_val env rhs in - L.(debug Analysis Medium) - " @\nAdding binding %a --> %a to env o@\n" Exp.pp lhs ItvPureCost.pp val_rhs ; - EnvDomain.add lhs val_rhs env - | Exn _ | Closure _ | Const _ | Cast _ | Lfield _ | Lindex _ | Sizeof _ -> - env - - - let remove_from_alias_list alias e = - let remove_exp a = - match a with Sil.Aeq (e1, e2) when Exp.equal e1 e || Exp.equal e e2 -> false | _ -> true - in - List.filter ~f:remove_exp alias - - - let update_alias tenv alias e1 e2 = - match (e1, e2) with - | Exp.Var _, Exp.Var _ | Exp.Var _, Exp.Lvar _ | Exp.Lvar _, Exp.Var _ | Exp.Lvar _, Exp.Lvar _ -> - (*Sil.Aeq (e1,e2) :: alias*) - let alias' = remove_from_alias_list alias e1 in - let prop = Prop.normalize tenv (Prop.from_pi alias') in - let prop' = Prop.conjoin_eq tenv e1 e2 prop in - Prop.get_pure prop' - | Exp.Lvar _, _ -> - remove_from_alias_list alias e1 - | _ -> - alias - - - (* Try to improve value for e using alias variables to get the tightest interval *) - let update_alias_env env alias e = - let try_restrict_itv env_acc e' e_val = - let v' = - match EnvDomain.find_opt e' env_acc with - | Some v_pre -> - L.(debug Analysis Medium) "@\n>>>Starting meet \n" ; - let meet = ItvPureCost.meet v_pre e_val in - L.(debug Analysis Medium) - "@\n>>>Result Meet v_pre= %a e_val= %a --> %a\n" ItvPureCost.pp v_pre - ItvPureCost.pp e_val ItvPureCost.pp meet ; - if ItvPureCost.is_empty meet then e_val else meet - | None -> - e_val - in - EnvDomain.add e' v' env_acc - in - let do_atom env_acc e_val a = - match a with - | Sil.Aeq (e1, e2) -> - if Exp.equal e1 e then try_restrict_itv env_acc e2 e_val - else if Exp.equal e2 e then try_restrict_itv env_acc e1 e_val - else env_acc - | _ -> - env - in - match EnvDomain.find_opt e env with - | Some e_val -> - List.fold ~f:(fun acc a -> do_atom acc e_val a) ~init:env alias - | _ -> - env - - - let sem_binop op (e1_opt, v1_opt) (e2_opt, v2_opt) = - let open Binop in - match op with - | Lt -> ( - match ((e1_opt, v1_opt), (e2_opt, v2_opt)) with - | (Some e, _), (_, Some (v1, v2)) when ItvPureCost.is_const (v1, v2) -> - let ub = Cost.dec v2 in - (Some e, Some (Top, ub)) - | (Some e1, Some v1), (Some e2, Some v2) -> - L.die InternalError - " @\n Incomplete Lt binon. Dies with (e1,v1)= (%a,%a) (e2,v2)=(%a, %a) @\n" Exp.pp e1 - ItvPureCost.pp v1 Exp.pp e2 ItvPureCost.pp v2 - | (Some e1, None), (Some e2, None) -> - L.die InternalError - " @\n Incomplete Lt binon. Dies with (e1,v1)= (%a,None) (e2,v2)=(%a,None) @\n" Exp.pp - e1 Exp.pp e2 - | _ -> - assert false ) - | Gt | Le | Ge | Eq | _ -> - L.die InternalError " @\n Incomplete Sem_binop function. Dies with op= %s @\n" - (Binop.str Pp.text op) - - - let sem_unop op (e1_opt, v1_opt) = - match op with - | Unop.LNot -> ( - match (e1_opt, v1_opt) with - | Some e, Some v -> - (Some e, Some (ItvPureCost.negation v)) - | _ -> - assert false ) - | _ -> - L.die InternalError " @\n Incomplete Sem_unop function. Dies with op= %s @\n" (Unop.str op) - - - (* semantics of expression e according to environment env *) - let rec sem env e : Exp.t option * ItvPureCost.t option = - match e with - | Exp.BinOp (op, e1, e2) -> - let res1 = sem env e1 in - let res2 = sem env e2 in - sem_binop op res1 res2 - | Exp.Const Cint i -> - (None, Some (ItvPureCost.of_int_lit i)) - | Exp.Lvar _ | Exp.Var _ -> - (Some e, None) - | Exp.UnOp (op, e1, _) -> - let res1 = sem env e1 in - sem_unop op res1 - | _ -> - L.die InternalError " @\n Incomplete Sem function. Dies with e= %a @\n" Exp.pp e -end - type summary = {post: Itv.Bound.t} let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" Itv.Bound.pp post