|
|
|
@ -9,77 +9,8 @@
|
|
|
|
|
|
|
|
|
|
open! IStd
|
|
|
|
|
module F = Format
|
|
|
|
|
module L = Logging
|
|
|
|
|
open AbstractDomain.Types
|
|
|
|
|
|
|
|
|
|
module IntCost = struct
|
|
|
|
|
type astate = int [@@deriving compare]
|
|
|
|
|
|
|
|
|
|
let pp fmt i = F.fprintf fmt "%i" i
|
|
|
|
|
|
|
|
|
|
let join = Int.max
|
|
|
|
|
|
|
|
|
|
let widen ~prev:_ ~next:_ ~num_iters:_ = assert false
|
|
|
|
|
|
|
|
|
|
let ( <= ) ~lhs ~rhs = Int.( <= ) lhs rhs
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
module Cost = struct
|
|
|
|
|
include AbstractDomain.TopLifted (IntCost)
|
|
|
|
|
|
|
|
|
|
let widen ~prev ~next ~num_iters:_ =
|
|
|
|
|
if phys_equal prev next then prev
|
|
|
|
|
else
|
|
|
|
|
match (prev, next) with
|
|
|
|
|
| NonTop prev, NonTop next when IntCost.( <= ) ~lhs:next ~rhs:prev ->
|
|
|
|
|
NonTop prev
|
|
|
|
|
| _, _ ->
|
|
|
|
|
Top
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let ( <= ) ~lhs ~rhs =
|
|
|
|
|
match (lhs, rhs) with
|
|
|
|
|
| Top, Top | NonTop _, Top ->
|
|
|
|
|
true
|
|
|
|
|
| Top, NonTop _ ->
|
|
|
|
|
false
|
|
|
|
|
| NonTop c1, NonTop c2 ->
|
|
|
|
|
Int.( <= ) c1 c2
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp_l fmt c =
|
|
|
|
|
let c'' = match c with Top -> Top | NonTop c' -> NonTop (-c') in
|
|
|
|
|
pp fmt c''
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp_u = pp
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
(* Map (node,instr) -> basic cost *)
|
|
|
|
|
module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (Itv.Bound)
|
|
|
|
|
|
|
|
|
|
module ItvPureCost = struct
|
|
|
|
|
(** (l, u) represents the closed interval [-l; u] (of course infinite bounds are open) *)
|
|
|
|
|
type astate = Cost.astate * Cost.astate
|
|
|
|
|
|
|
|
|
|
type t = astate
|
|
|
|
|
|
|
|
|
|
let ( <= ) : lhs:t -> rhs:t -> bool =
|
|
|
|
|
fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Cost.( <= ) ~lhs:l1 ~rhs:l2 && Cost.( <= ) ~lhs:u1 ~rhs:u2
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Cost.join l1 l2, Cost.join u1 u2)
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp : F.formatter -> t -> unit =
|
|
|
|
|
fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Cost.pp_l l Cost.pp_u u
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
module EnvDomain = AbstractDomain.Map (Exp) (ItvPureCost)
|
|
|
|
|
module EnvMap = AbstractDomain.Map (Exp) (Itv)
|
|
|
|
|
module EnvDomainBO = AbstractDomain.BottomLifted (EnvMap)
|
|
|
|
|
|
|
|
|
|