pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] No bottom bound

Browse Source 
Summary:
Bottom bounds do not make sense (what is the meaning of `[_|_; 1]`?), let's get rid of them.
`Bot` was useful for substitution though, with a special meaning, use `bottom_lifted` for that case.

Reviewed By: skcho

Differential Revision: D5941796

fbshipit-source-id: 5778255
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 26f847f381
commit ea4d97ecf8
4 changed files with 127 additions and 141 deletions
Show Stats Download Patch File Download Diff File

5
infer/src/bufferoverrun/arrayBlk.ml
Unescape View File

@ -12,6 +12,7 @@
(* Abstract Array Block *) (* Abstract Array Block *)
open! IStd open! IStd
open AbsLoc open AbsLoc
open! AbstractDomain.Types
module ArrInfo = struct module ArrInfo = struct
type t = {offset: Itv.t; size: Itv.t; stride: Itv.t} [@@deriving compare] type t = {offset: Itv.t; size: Itv.t; stride: Itv.t} [@@deriving compare]
@ -64,7 +65,7 @@ module ArrInfo = struct
let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t = let subst : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t =
fun arr subst_map -> fun arr subst_map ->
{arr with offset= Itv.subst arr.offset subst_map; size= Itv.subst arr.size subst_map} {arr with offset= Itv.subst arr.offset subst_map; size= Itv.subst arr.size subst_map}
@ -138,7 +139,7 @@ let get_pow_loc : astate -> PowLoc.t =
let pow_loc_of_allocsite k _ acc = PowLoc.add (Loc.of_allocsite k) acc in let pow_loc_of_allocsite k _ acc = PowLoc.add (Loc.of_allocsite k) acc in
fold pow_loc_of_allocsite array PowLoc.bot fold pow_loc_of_allocsite array PowLoc.bot
let subst : astate -> Itv.Bound.t Itv.SubstMap.t -> astate = let subst : astate -> Itv.Bound.t bottom_lifted Itv.SubstMap.t -> astate =
fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a
let get_symbols : astate -> Itv.Symbol.t list = let get_symbols : astate -> Itv.Symbol.t list =

28
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -150,18 +150,16 @@ module Condition = struct
let description : t -> string = fun c -> Format.asprintf "%a" pp_description c let description : t -> string = fun c -> Format.asprintf "%a" pp_description c
let subst let subst
: t -> Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Typ.Procname.t : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Typ.Procname.t
-> Typ.Procname.t -> Location.t -> t option = -> Typ.Procname.t -> Location.t -> t option =
fun c (bound_map, trace_map) caller_pname callee_pname loc -> fun c (bound_map, trace_map) caller_pname callee_pname loc ->
match ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size with match ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size with
| [] | []
-> Some c -> Some c
| symbols | symbols ->
-> let idx = ItvPure.subst c.idx bound_map in match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with
let size = ItvPure.subst c.size bound_map in | NonBottom idx, NonBottom size
if ItvPure.has_bnd_bot idx || ItvPure.has_bnd_bot size then None -> let traces_caller =
else
let traces_caller =
List.fold symbols ~init:TraceSet.empty ~f:(fun traces symbol -> List.fold symbols ~init:TraceSet.empty ~f:(fun traces symbol ->
match Itv.SubstMap.find symbol trace_map with match Itv.SubstMap.find symbol trace_map with
| symbol_trace | symbol_trace
@ -172,6 +170,8 @@ module Condition = struct
let traces = TraceSet.instantiate ~traces_caller ~traces_callee:c.traces loc in let traces = TraceSet.instantiate ~traces_caller ~traces_callee:c.traces loc in
let cond_trace = Inter (caller_pname, callee_pname, loc) in let cond_trace = Inter (caller_pname, callee_pname, loc) in
Some {c with idx; size; cond_trace; traces} Some {c with idx; size; cond_trace; traces}
| _
-> None
end end
module ConditionSet = struct module ConditionSet = struct
@ -185,7 +185,7 @@ module ConditionSet = struct
add (Condition.make pname loc id ~idx ~size traces) cond add (Condition.make pname loc id ~idx ~size traces) cond
let subst let subst
: t -> Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Typ.Procname.t : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Typ.Procname.t
-> Typ.Procname.t -> Location.t -> t = -> Typ.Procname.t -> Location.t -> t =
fun x subst_map caller_pname callee_pname loc -> fun x subst_map caller_pname callee_pname loc ->
fold fold
@ -203,7 +203,7 @@ module ConditionSet = struct
(fun cond map -> (fun cond map ->
let old_set = let old_set =
try Map.find cond.loc map try Map.find cond.loc map
with _ -> empty with Not_found -> empty
in in
Map.add cond.loc (add cond old_set) map) Map.add cond.loc (add cond old_set) map)
x Map.empty x Map.empty
@ -400,15 +400,17 @@ module Val = struct
let normalize : t -> t = let normalize : t -> t =
fun x -> {x with itv= Itv.normalize x.itv; arrayblk= ArrayBlk.normalize x.arrayblk} fun x -> {x with itv= Itv.normalize x.itv; arrayblk= ArrayBlk.normalize x.arrayblk}
let subst : t -> Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Location.t -> t = let subst
: t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Location.t
-> t =
fun x (bound_map, trace_map) loc -> fun x (bound_map, trace_map) loc ->
let symbols = get_symbols x in let symbols = get_symbols x in
let traces_caller = let traces_caller =
List.fold List.fold symbols
~f:(fun traces symbol -> ~f:(fun traces symbol ->
try TraceSet.join (Itv.SubstMap.find symbol trace_map) traces try TraceSet.join (Itv.SubstMap.find symbol trace_map) traces
with _ -> traces) with Not_found -> traces)
~init:TraceSet.empty symbols ~init:TraceSet.empty
in in
let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces loc in let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces loc in
{x with itv= Itv.subst x.itv bound_map; arrayblk= ArrayBlk.subst x.arrayblk bound_map; traces} {x with itv= Itv.subst x.itv bound_map; arrayblk= ArrayBlk.subst x.arrayblk bound_map; traces}

21
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -12,12 +12,12 @@
open! IStd open! IStd
open AbsLoc open AbsLoc
open! AbstractDomain.Types
module F = Format module F = Format
module L = Logging module L = Logging
module Domain = BufferOverrunDomain
module Trace = BufferOverrunTrace module Trace = BufferOverrunTrace
module TraceSet = Trace.Set module TraceSet = Trace.Set
open Domain open BufferOverrunDomain
module Make (CFG : ProcCfg.S) = struct module Make (CFG : ProcCfg.S) = struct
exception Not_implemented exception Not_implemented
@ -420,7 +420,7 @@ module Make (CFG : ProcCfg.S) = struct
let get_matching_pairs let get_matching_pairs
: Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate
-> callee_ret_alias:Loc.t option -> callee_ret_alias:Loc.t option
-> (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list * Loc.t option = -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * Loc.t option =
fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias ->
let get_itv v = Val.get_itv v in let get_itv v = Val.get_itv v in
let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in
@ -441,10 +441,11 @@ module Make (CFG : ProcCfg.S) = struct
in in
let add_pair_itv itv1 itv2 traces l = let add_pair_itv itv1 itv2 traces l =
let open Itv in let open Itv in
if itv1 <> bot && itv1 <> top && itv2 <> bot then (lb itv1, lb itv2, traces) if itv1 <> bot && itv1 <> top then
:: (ub itv1, ub itv2, traces) :: l if Itv.eq itv2 bot then (lb itv1, Bottom, TraceSet.empty)
else if itv1 <> bot && itv1 <> top && Itv.eq itv2 bot then :: (ub itv1, Bottom, TraceSet.empty) :: l
(lb itv1, Bound.Bot, TraceSet.empty) :: (ub itv1, Bound.Bot, TraceSet.empty) :: l else (lb itv1, NonBottom (lb itv2), traces)
:: (ub itv1, NonBottom (ub itv2), traces) :: l
else l else l
in in
let add_pair_val v1 v2 pairs = let add_pair_val v1 v2 pairs =
@ -480,8 +481,8 @@ module Make (CFG : ProcCfg.S) = struct
(pairs, !ret_alias) (pairs, !ret_alias)
let subst_map_of_pairs let subst_map_of_pairs
: (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
-> Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t = -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t =
fun pairs -> fun pairs ->
let add_pair (bound_map, trace_map) (formal, actual, traces) = let add_pair (bound_map, trace_map) (formal, actual, traces) =
match formal with match formal with
@ -515,7 +516,7 @@ module Make (CFG : ProcCfg.S) = struct
let get_subst_map let get_subst_map
: Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
-> callee_ret_alias:Loc.t option -> Location.t -> callee_ret_alias:Loc.t option -> Location.t
-> (Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) * Loc.t option = -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) * Loc.t option =
fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc -> fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc ->
let add_pair (formal, typ) actual (l, ret_alias) = let add_pair (formal, typ) actual (l, ret_alias) =
let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in

214
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -186,7 +186,6 @@ module Bound = struct
| Linear of int * SymLinear.t | Linear of int * SymLinear.t
| MinMax of int * sign_t * min_max_t * int * Symbol.t | MinMax of int * sign_t * min_max_t * int * Symbol.t
| PInf | PInf
| Bot
[@@deriving compare] [@@deriving compare]
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
@ -204,8 +203,6 @@ module Bound = struct
-> F.fprintf fmt "-oo" -> F.fprintf fmt "-oo"
| PInf | PInf
-> F.fprintf fmt "+oo" -> F.fprintf fmt "+oo"
| Bot
-> F.fprintf fmt "_|_"
| Linear (c, x) | Linear (c, x)
-> if SymLinear.le x SymLinear.empty then F.fprintf fmt "%d" c -> if SymLinear.le x SymLinear.empty then F.fprintf fmt "%d" c
else if Int.equal c 0 then F.fprintf fmt "%a" SymLinear.pp x else if Int.equal c 0 then F.fprintf fmt "%a" SymLinear.pp x
@ -224,7 +221,7 @@ module Bound = struct
let of_sym : SymLinear.t -> t = fun s -> Linear (0, s) let of_sym : SymLinear.t -> t = fun s -> Linear (0, s)
let is_symbolic : t -> bool = function let is_symbolic : t -> bool = function
| MInf | PInf | Bot | MInf | PInf
-> false -> false
| Linear (_, se) | Linear (_, se)
-> not (SymLinear.is_empty se) -> not (SymLinear.is_empty se)
@ -238,13 +235,13 @@ module Bound = struct
let eq_symbol : Symbol.t -> t -> bool = let eq_symbol : Symbol.t -> t -> bool =
fun s -> fun s ->
function function
| Linear (c, se) | Linear (0, se)
-> Int.equal c 0 && opt_lift Symbol.eq (SymLinear.get_one_symbol_opt se) (Some s) -> opt_lift Symbol.eq (SymLinear.get_one_symbol_opt se) (Some s)
| _ | _
-> false -> false
let lift_get_one_symbol : (SymLinear.t -> Symbol.t option) -> t -> Symbol.t option = let lift_get_one_symbol : (SymLinear.t -> Symbol.t option) -> t -> Symbol.t option =
fun f -> function Linear (c, se) when Int.equal c 0 -> f se | _ -> None fun f -> function Linear (0, se) -> f se | _ -> None
let get_one_symbol_opt : t -> Symbol.t option = lift_get_one_symbol SymLinear.get_one_symbol_opt let get_one_symbol_opt : t -> Symbol.t option = lift_get_one_symbol SymLinear.get_one_symbol_opt
@ -264,76 +261,85 @@ module Bound = struct
let use_symbol : Symbol.t -> t -> bool = let use_symbol : Symbol.t -> t -> bool =
fun s -> fun s ->
function function
| PInf | MInf | Bot | PInf | MInf
-> false -> false
| Linear (_, se) | Linear (_, se)
-> SymLinear.find s se <> 0 -> SymLinear.find s se <> 0
| MinMax (_, _, _, _, s') | MinMax (_, _, _, _, s')
-> Symbol.eq s s' -> Symbol.eq s s'
let subst1 : t -> t -> Symbol.t -> t -> t = let subst1 : default:t -> t bottom_lifted -> Symbol.t -> t bottom_lifted -> t bottom_lifted =
fun default x s y -> fun ~default x0 s y0 ->
if not (use_symbol s x) then x match (x0, y0) with
else | Bottom, _
match (x, y) with -> x0
| _, _ when eq_symbol s x | NonBottom x, _ when eq_symbol s x
-> y -> y0
| Linear (c1, se1), Linear (c2, se2) | NonBottom x, _ when not (use_symbol s x)
-> let coeff = SymLinear.find s se1 in -> x0
let c' = c1 + coeff * c2 in | NonBottom _, Bottom
let se1 = SymLinear.add s 0 se1 in -> NonBottom default
let se' = SymLinear.plus se1 (SymLinear.mult_const se2 coeff) in | NonBottom x, NonBottom y
Linear (c', se') -> let res =
| MinMax (_, Plus, Min, _, _), MInf match (x, y) with
-> MInf | Linear (c1, se1), Linear (c2, se2)
| MinMax (_, Minus, Min, _, _), MInf -> let coeff = SymLinear.find s se1 in
-> PInf let c' = c1 + coeff * c2 in
| MinMax (_, Plus, Max, _, _), PInf let se1 = SymLinear.add s 0 se1 in
-> PInf let se' = SymLinear.plus se1 (SymLinear.mult_const se2 coeff) in
| MinMax (_, Minus, Max, _, _), PInf Linear (c', se')
-> MInf | MinMax (_, Plus, Min, _, _), MInf
| MinMax (c, Plus, Min, d, _), PInf -> MInf
-> Linear (c + d, SymLinear.zero) | MinMax (_, Minus, Min, _, _), MInf
| MinMax (c, Minus, Min, d, _), PInf -> PInf
-> Linear (c - d, SymLinear.zero) | MinMax (_, Plus, Max, _, _), PInf
| MinMax (c, Plus, Max, d, _), MInf -> PInf
-> Linear (c + d, SymLinear.zero) | MinMax (_, Minus, Max, _, _), PInf
| MinMax (c, Minus, Max, d, _), MInf -> MInf
-> Linear (c - d, SymLinear.zero) | MinMax (c, Plus, Min, d, _), PInf
| MinMax (c1, Plus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se -> Linear (c + d, SymLinear.zero)
-> Linear (c1 + min d1 c2, SymLinear.zero) | MinMax (c, Minus, Min, d, _), PInf
| MinMax (c1, Minus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se -> Linear (c - d, SymLinear.zero)
-> Linear (c1 - min d1 c2, SymLinear.zero) | MinMax (c, Plus, Max, d, _), MInf
| MinMax (c1, Plus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se -> Linear (c + d, SymLinear.zero)
-> Linear (c1 + max d1 c2, SymLinear.zero) | MinMax (c, Minus, Max, d, _), MInf
| MinMax (c1, Minus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se -> Linear (c - d, SymLinear.zero)
-> Linear (c1 - max d1 c2, SymLinear.zero) | MinMax (c1, Plus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se
| MinMax (c, sign, m, d, _), _ when is_one_symbol y -> Linear (c1 + min d1 c2, SymLinear.zero)
-> MinMax (c, sign, m, d, get_one_symbol y) | MinMax (c1, Minus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se
| MinMax (c, sign, m, d, _), _ when is_mone_symbol y -> Linear (c1 - min d1 c2, SymLinear.zero)
-> MinMax (c, neg_sign sign, neg_min_max m, -d, get_mone_symbol y) | MinMax (c1, Plus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se
| MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') -> Linear (c1 + max d1 c2, SymLinear.zero)
-> MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s') | MinMax (c1, Minus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se
| MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') -> Linear (c1 - max d1 c2, SymLinear.zero)
-> MinMax (c1 + c2, Plus, Max, max (d1 - c2) d2, s') | MinMax (c, sign, m, d, _), _ when is_one_symbol y
| MinMax (c1, Minus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') -> MinMax (c, sign, m, d, get_one_symbol y)
-> MinMax (c1 - c2, Minus, Min, min (d1 - c2) d2, s') | MinMax (c, sign, m, d, _), _ when is_mone_symbol y
| MinMax (c1, Minus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') -> MinMax (c, neg_sign sign, neg_min_max m, -d, get_mone_symbol y)
-> MinMax (c1 - c2, Minus, Max, max (d1 - c2) d2, s') | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s')
| MinMax (c1, Plus, Min, d1, _), MinMax (c2, Minus, Max, d2, s') -> MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s')
-> MinMax (c1 + c2, Minus, Max, max (-d1 + c2) d2, s') | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s')
| MinMax (c1, Plus, Max, d1, _), MinMax (c2, Minus, Min, d2, s') -> MinMax (c1 + c2, Plus, Max, max (d1 - c2) d2, s')
-> MinMax (c1 + c2, Minus, Min, min (-d1 + c2) d2, s') | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Plus, Min, d2, s')
| MinMax (c1, Minus, Min, d1, _), MinMax (c2, Minus, Max, d2, s') -> MinMax (c1 - c2, Minus, Min, min (d1 - c2) d2, s')
-> MinMax (c1 - c2, Minus, Max, max (-d1 + c2) d2, s') | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Plus, Max, d2, s')
| MinMax (c1, Minus, Max, d1, _), MinMax (c2, Minus, Min, d2, s') -> MinMax (c1 - c2, Minus, Max, max (d1 - c2) d2, s')
-> MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s') | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Minus, Max, d2, s')
| _ -> MinMax (c1 + c2, Minus, Max, max (-d1 + c2) d2, s')
-> default | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Minus, Min, d2, s')
-> MinMax (c1 + c2, Minus, Min, min (-d1 + c2) d2, s')
| MinMax (c1, Minus, Min, d1, _), MinMax (c2, Minus, Max, d2, s')
-> MinMax (c1 - c2, Minus, Max, max (-d1 + c2) d2, s')
| MinMax (c1, Minus, Max, d1, _), MinMax (c2, Minus, Min, d2, s')
-> MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s')
| _
-> default
in
NonBottom res
(* substitution symbols in ``x'' with respect to ``map'' *) (* substitution symbols in ``x'' with respect to ``map'' *)
let subst : t -> t -> t SubstMap.t -> t = let subst : default:t -> t -> t bottom_lifted SubstMap.t -> t bottom_lifted =
fun default x map -> SubstMap.fold (fun s y x -> subst1 default x s y) map x fun ~default x map -> SubstMap.fold (fun s y x -> subst1 ~default x s y) map (NonBottom x)
let int_ub_of_minmax = function let int_ub_of_minmax = function
| MinMax (c, Plus, Min, d, _) | MinMax (c, Plus, Min, d, _)
@ -342,7 +348,7 @@ module Bound = struct
-> Some (c - d) -> Some (c - d)
| MinMax _ | MinMax _
-> None -> None
| MInf | PInf | Linear _ | Bot | MInf | PInf | Linear _
-> assert false -> assert false
let int_lb_of_minmax = function let int_lb_of_minmax = function
@ -352,7 +358,7 @@ module Bound = struct
-> Some (c - d) -> Some (c - d)
| MinMax _ | MinMax _
-> None -> None
| MInf | PInf | Linear _ | Bot | MInf | PInf | Linear _
-> assert false -> assert false
let linear_ub_of_minmax = function let linear_ub_of_minmax = function
@ -362,7 +368,7 @@ module Bound = struct
-> Some (Linear (c, SymLinear.singleton x (-1))) -> Some (Linear (c, SymLinear.singleton x (-1)))
| MinMax _ | MinMax _
-> None -> None
| MInf | PInf | Linear _ | Bot | MInf | PInf | Linear _
-> assert false -> assert false
let linear_lb_of_minmax = function let linear_lb_of_minmax = function
@ -372,7 +378,7 @@ module Bound = struct
-> Some (Linear (c, SymLinear.singleton x (-1))) -> Some (Linear (c, SymLinear.singleton x (-1)))
| MinMax _ | MinMax _
-> None -> None
| MInf | PInf | Linear _ | Bot | MInf | PInf | Linear _
-> assert false -> assert false
let le_minmax_by_int x y = let le_minmax_by_int x y =
@ -384,7 +390,6 @@ module Bound = struct
let rec le : t -> t -> bool = let rec le : t -> t -> bool =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
match (x, y) with match (x, y) with
| MInf, _ | _, PInf | MInf, _ | _, PInf
-> true -> true
@ -413,7 +418,6 @@ module Bound = struct
let lt : t -> t -> bool = let lt : t -> t -> bool =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
match (x, y) with match (x, y) with
| MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf
-> true -> true
@ -426,11 +430,7 @@ module Bound = struct
let gt : t -> t -> bool = fun x y -> lt y x let gt : t -> t -> bool = fun x y -> lt y x
let eq : t -> t -> bool = let eq : t -> t -> bool = fun x y -> le x y && le y x
fun x y ->
if equal x Bot && equal y Bot then true
else if equal x Bot || equal y Bot then false
else le x y && le y x
let remove_max_int : t -> t = let remove_max_int : t -> t =
fun x -> fun x ->
@ -444,7 +444,6 @@ module Bound = struct
let rec lb : ?default:t -> t -> t -> t = let rec lb : ?default:t -> t -> t -> t =
fun ?(default= MInf) x y -> fun ?(default= MInf) x y ->
assert (x <> Bot && y <> Bot) ;
if le x y then x if le x y then x
else if le y x then y else if le y x then y
else else
@ -490,7 +489,6 @@ module Bound = struct
let ub : t -> t -> t = let ub : t -> t -> t =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
if le x y then y if le x y then y
else if le y x then x else if le y x then x
else else
@ -508,14 +506,12 @@ module Bound = struct
let widen_l : t -> t -> t = let widen_l : t -> t -> t =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
if equal x PInf || equal y PInf then L.(die InternalError) "Lower bound cannot be +oo." if equal x PInf || equal y PInf then L.(die InternalError) "Lower bound cannot be +oo."
else if le x y then x else if le x y then x
else MInf else MInf
let widen_u : t -> t -> t = let widen_u : t -> t -> t =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
if equal x MInf || equal y MInf then L.(die InternalError) "Upper bound cannot be -oo." if equal x MInf || equal y MInf then L.(die InternalError) "Upper bound cannot be -oo."
else if le y x then x else if le y x then x
else PInf else PInf
@ -529,22 +525,17 @@ module Bound = struct
let mone : t = Linear (-1, SymLinear.zero) let mone : t = Linear (-1, SymLinear.zero)
let is_some_const : int -> t -> bool = let is_some_const : int -> t -> bool =
fun c x -> fun c x -> match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false
assert (x <> Bot) ;
match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false
let is_zero : t -> bool = is_some_const 0 let is_zero : t -> bool = is_some_const 0
let is_one : t -> bool = is_some_const 1 let is_one : t -> bool = is_some_const 1
let is_const : t -> int option = let is_const : t -> int option =
fun x -> fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
assert (x <> Bot) ;
match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
let plus_l : t -> t -> t = let plus_l : t -> t -> t =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
match (x, y) with match (x, y) with
| _, _ when is_zero x | _, _ when is_zero x
-> y -> y
@ -567,7 +558,6 @@ module Bound = struct
let plus_u : t -> t -> t = let plus_u : t -> t -> t =
fun x y -> fun x y ->
assert (x <> Bot && y <> Bot) ;
match (x, y) with match (x, y) with
| _, _ when is_zero x | _, _ when is_zero x
-> y -> y
@ -590,7 +580,6 @@ module Bound = struct
let mult_const : t -> int -> t option = let mult_const : t -> int -> t option =
fun x n -> fun x n ->
assert (x <> Bot) ;
assert (n <> 0) ; assert (n <> 0) ;
match x with match x with
| MInf | MInf
@ -604,7 +593,6 @@ module Bound = struct
let div_const : t -> int -> t option = let div_const : t -> int -> t option =
fun x n -> fun x n ->
assert (x <> Bot) ;
if Int.equal n 0 then Some zero if Int.equal n 0 then Some zero
else else
match x with match x with
@ -628,8 +616,6 @@ module Bound = struct
-> Some (Linear (-c, SymLinear.neg x)) -> Some (Linear (-c, SymLinear.neg x))
| MinMax (c, sign, min_max, d, x) | MinMax (c, sign, min_max, d, x)
-> Some (MinMax (-c, neg_sign sign, min_max, d, x)) -> Some (MinMax (-c, neg_sign sign, min_max, d, x))
| Bot
-> assert false
let get_symbols : t -> Symbol.t list = function let get_symbols : t -> Symbol.t list = function
| MInf | PInf | MInf | PInf
@ -638,8 +624,6 @@ module Bound = struct
-> SymLinear.get_symbols se -> SymLinear.get_symbols se
| MinMax (_, _, _, _, s) | MinMax (_, _, _, _, s)
-> [s] -> [s]
| Bot
-> assert false
let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true
end end
@ -661,8 +645,15 @@ module ItvPure = struct
let make : Bound.t -> Bound.t -> t = fun l u -> (l, u) let make : Bound.t -> Bound.t -> t = fun l u -> (l, u)
let subst : t -> Bound.t SubstMap.t -> t = let subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted =
fun x map -> (Bound.subst Bound.MInf (lb x) map, Bound.subst Bound.PInf (ub x) map) fun x map ->
match
(Bound.subst ~default:Bound.MInf (lb x) map, Bound.subst ~default:Bound.PInf (ub x) map)
with
| NonBottom l, NonBottom u
-> NonBottom (l, u)
| _
-> Bottom
let ( <= ) : lhs:t -> rhs:t -> bool = let ( <= ) : lhs:t -> rhs:t -> bool =
fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2 fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2
@ -739,11 +730,9 @@ module ItvPure = struct
let is_symbolic : t -> bool = fun (lb, ub) -> Bound.is_symbolic lb || Bound.is_symbolic ub let is_symbolic : t -> bool = fun (lb, ub) -> Bound.is_symbolic lb || Bound.is_symbolic ub
let is_ge_zero : t -> bool = let is_ge_zero : t -> bool = fun (lb, _) -> Bound.le Bound.zero lb
fun (lb, _) -> if lb <> Bound.Bot then Bound.le Bound.zero lb else false
let is_le_zero : t -> bool = let is_le_zero : t -> bool = fun (_, ub) -> Bound.le ub Bound.zero
fun (_, ub) -> if ub <> Bound.Bot then Bound.le ub Bound.zero else false
let neg : t -> t = let neg : t -> t =
fun (l, u) -> fun (l, u) ->
@ -865,15 +854,12 @@ module ItvPure = struct
let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2) let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2)
let invalid : t -> bool = let invalid : t -> bool = function Bound.PInf, _ | _, Bound.MInf -> true | l, u -> Bound.lt u l
fun (l, u) ->
Bound.equal l Bound.Bot || Bound.equal u Bound.Bot || Bound.eq l Bound.PInf
|| Bound.eq u Bound.MInf || Bound.lt u l
let prune_le : t -> t -> t = let prune_le : t -> t -> t =
fun x y -> fun x y ->
match (x, y) with match (x, y) with
| (l1, u1), (_, u2) when Bound.equal u1 Bound.PInf | (l1, Bound.PInf), (_, u2)
-> (l1, u2) -> (l1, u2)
| (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when SymLinear.eq s1 s2 | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when SymLinear.eq s1 s2
-> (l1, Bound.Linear (min c1 c2, s1)) -> (l1, Bound.Linear (min c1 c2, s1))
@ -899,7 +885,7 @@ module ItvPure = struct
let prune_ge : t -> t -> t = let prune_ge : t -> t -> t =
fun x y -> fun x y ->
match (x, y) with match (x, y) with
| (l1, u1), (l2, _) when Bound.equal l1 Bound.MInf | (Bound.MInf, u1), (l2, _)
-> (l2, u1) -> (l2, u1)
| (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when SymLinear.eq s1 s2 | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when SymLinear.eq s1 s2
-> (Bound.Linear (max c1 c2, s1), u1) -> (Bound.Linear (max c1 c2, s1), u1)
@ -971,8 +957,6 @@ module ItvPure = struct
fun (l, u as x) -> if Bound.lt l Bound.zero then (Bound.zero, u) else x fun (l, u as x) -> if Bound.lt l Bound.zero then (Bound.zero, u) else x
let normalize : t -> t option = fun (l, u) -> if invalid (l, u) then None else Some (l, u) let normalize : t -> t option = fun (l, u) -> if invalid (l, u) then None else Some (l, u)
let has_bnd_bot : t -> bool = fun (l, u) -> Bound.equal l Bound.Bot || Bound.equal u Bound.Bot
end end
include AbstractDomain.BottomLifted (ItvPure) include AbstractDomain.BottomLifted (ItvPure)
@ -1124,8 +1108,8 @@ let prune_eq : t -> t -> t = lift2_opt ItvPure.prune_eq
let prune_ne : t -> t -> t = lift2_opt ItvPure.prune_ne let prune_ne : t -> t -> t = lift2_opt ItvPure.prune_ne
let subst : t -> Bound.t SubstMap.t -> t = let subst : t -> Bound.t bottom_lifted SubstMap.t -> t =
fun x map -> match x with NonBottom x' -> NonBottom (ItvPure.subst x' map) | _ -> x fun x map -> match x with NonBottom x' -> ItvPure.subst x' map | _ -> x
let get_symbols : t -> Symbol.t list = function let get_symbols : t -> Symbol.t list = function
| Bottom | Bottom
@ -1134,5 +1118,3 @@ let get_symbols : t -> Symbol.t list = function
-> ItvPure.get_symbols x -> ItvPure.get_symbols x
let normalize : t -> t = lift1_opt ItvPure.normalize let normalize : t -> t = lift1_opt ItvPure.normalize
let has_bnd_bot : t -> bool = function Bottom -> false | NonBottom x -> ItvPure.has_bnd_bot x

Write Preview
Loading…
Cancel
Save