|
9 | 9 |
|
10 | 10 | open! IStd |
11 | 11 | module F = Format |
12 | | -module L = Logging |
13 | | -open AbstractDomain.Types |
14 | | - |
15 | | -module IntCost = struct |
16 | | - type astate = int [@@deriving compare] |
17 | | - |
18 | | - let pp fmt i = F.fprintf fmt "%i" i |
19 | | - |
20 | | - let join = Int.max |
21 | | - |
22 | | - let widen ~prev:_ ~next:_ ~num_iters:_ = assert false |
23 | | - |
24 | | - let ( <= ) ~lhs ~rhs = Int.( <= ) lhs rhs |
25 | | -end |
26 | | - |
27 | | -module Cost = struct |
28 | | - include AbstractDomain.TopLifted (IntCost) |
29 | | - |
30 | | - let widen ~prev ~next ~num_iters:_ = |
31 | | - if phys_equal prev next then prev |
32 | | - else |
33 | | - match (prev, next) with |
34 | | - | NonTop prev, NonTop next when IntCost.( <= ) ~lhs:next ~rhs:prev -> |
35 | | - NonTop prev |
36 | | - | _, _ -> |
37 | | - Top |
38 | | - |
39 | | - |
40 | | - let ( <= ) ~lhs ~rhs = |
41 | | - match (lhs, rhs) with |
42 | | - | Top, Top | NonTop _, Top -> |
43 | | - true |
44 | | - | Top, NonTop _ -> |
45 | | - false |
46 | | - | NonTop c1, NonTop c2 -> |
47 | | - Int.( <= ) c1 c2 |
48 | | - |
49 | | - |
50 | | - let pp_l fmt c = |
51 | | - let c'' = match c with Top -> Top | NonTop c' -> NonTop (-c') in |
52 | | - pp fmt c'' |
53 | | - |
54 | | - |
55 | | - let pp_u = pp |
56 | | -end |
57 | | - |
58 | 12 | (* Map (node,instr) -> basic cost *) |
59 | 13 | module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (Itv.Bound) |
60 | | - |
61 | | -module ItvPureCost = struct |
62 | | - (** (l, u) represents the closed interval [-l; u] (of course infinite bounds are open) *) |
63 | | - type astate = Cost.astate * Cost.astate |
64 | | - |
65 | | - type t = astate |
66 | | - |
67 | | - let ( <= ) : lhs:t -> rhs:t -> bool = |
68 | | - fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Cost.( <= ) ~lhs:l1 ~rhs:l2 && Cost.( <= ) ~lhs:u1 ~rhs:u2 |
69 | | - |
70 | | - |
71 | | - let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Cost.join l1 l2, Cost.join u1 u2) |
72 | | - |
73 | | - let widen : prev:t -> next:t -> num_iters:int -> t = |
74 | | - fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters -> |
75 | | - (Cost.widen ~prev:l1 ~next:l2 ~num_iters, Cost.widen ~prev:u1 ~next:u2 ~num_iters) |
76 | | - |
77 | | - |
78 | | - let pp : F.formatter -> t -> unit = |
79 | | - fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Cost.pp_l l Cost.pp_u u |
80 | | -end |
81 | | - |
82 | | -module EnvDomain = AbstractDomain.Map (Exp) (ItvPureCost) |
83 | 14 | module EnvMap = AbstractDomain.Map (Exp) (Itv) |
84 | 15 | module EnvDomainBO = AbstractDomain.BottomLifted (EnvMap) |
85 | 16 |
|
|
0 commit comments