|
|
@ -29,30 +29,30 @@ struct
|
|
|
|
trace : trace;
|
|
|
|
trace : trace;
|
|
|
|
id : string }
|
|
|
|
id : string }
|
|
|
|
[@@deriving compare]
|
|
|
|
[@@deriving compare]
|
|
|
|
and trace = Intra of Typ.Procname.t
|
|
|
|
and trace = Intra of Typ.Procname.t
|
|
|
|
| Inter of Typ.Procname.t * Typ.Procname.t * Location.t
|
|
|
|
| Inter of Typ.Procname.t * Typ.Procname.t * Location.t
|
|
|
|
[@@deriving compare]
|
|
|
|
[@@deriving compare]
|
|
|
|
|
|
|
|
|
|
|
|
and astate = t
|
|
|
|
and astate = t
|
|
|
|
|
|
|
|
|
|
|
|
let set_size_pos : t -> t
|
|
|
|
let set_size_pos : t -> t
|
|
|
|
= fun c ->
|
|
|
|
= fun c ->
|
|
|
|
if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
|
|
|
|
if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
|
|
|
|
then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
|
|
|
|
then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
|
|
|
|
else c
|
|
|
|
else c
|
|
|
|
|
|
|
|
|
|
|
|
let string_of_location : Location.t -> string
|
|
|
|
let string_of_location : Location.t -> string
|
|
|
|
= fun loc ->
|
|
|
|
= fun loc ->
|
|
|
|
let fname = SourceFile.to_string loc.Location.file in
|
|
|
|
let fname = SourceFile.to_string loc.Location.file in
|
|
|
|
let pos = Location.to_string loc in
|
|
|
|
let pos = Location.to_string loc in
|
|
|
|
F.fprintf F.str_formatter "%s:%s" fname pos;
|
|
|
|
F.fprintf F.str_formatter "%s:%s" fname pos;
|
|
|
|
F.flush_str_formatter ()
|
|
|
|
F.flush_str_formatter ()
|
|
|
|
|
|
|
|
|
|
|
|
let pp_location : F.formatter -> t -> unit
|
|
|
|
let pp_location : F.formatter -> t -> unit
|
|
|
|
= fun fmt c ->
|
|
|
|
= fun fmt c ->
|
|
|
|
F.fprintf fmt "%s" (string_of_location c.loc)
|
|
|
|
F.fprintf fmt "%s" (string_of_location c.loc)
|
|
|
|
|
|
|
|
|
|
|
|
let pp : F.formatter -> t -> unit
|
|
|
|
let pp : F.formatter -> t -> unit
|
|
|
|
= fun fmt c ->
|
|
|
|
= fun fmt c ->
|
|
|
|
let c = set_size_pos c in
|
|
|
|
let c = set_size_pos c in
|
|
|
|
if Config.bo_debug <= 1 then
|
|
|
|
if Config.bo_debug <= 1 then
|
|
|
@ -65,27 +65,27 @@ struct
|
|
|
|
Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
|
|
|
|
Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
|
|
|
|
| Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
|
|
|
|
| Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
|
|
|
|
|
|
|
|
|
|
|
|
let get_location : t -> Location.t
|
|
|
|
let get_location : t -> Location.t
|
|
|
|
= fun c -> c.loc
|
|
|
|
= fun c -> c.loc
|
|
|
|
|
|
|
|
|
|
|
|
let get_trace : t -> trace
|
|
|
|
let get_trace : t -> trace
|
|
|
|
= fun c -> c.trace
|
|
|
|
= fun c -> c.trace
|
|
|
|
|
|
|
|
|
|
|
|
let get_proc_name : t -> Typ.Procname.t
|
|
|
|
let get_proc_name : t -> Typ.Procname.t
|
|
|
|
= fun c -> c.proc_name
|
|
|
|
= fun c -> c.proc_name
|
|
|
|
|
|
|
|
|
|
|
|
let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
|
|
|
|
let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
|
|
|
|
= fun proc_name loc id ~idx ~size ->
|
|
|
|
= fun proc_name loc id ~idx ~size ->
|
|
|
|
{ proc_name; idx; size; loc; id ; trace = Intra proc_name }
|
|
|
|
{ proc_name; idx; size; loc; id ; trace = Intra proc_name }
|
|
|
|
|
|
|
|
|
|
|
|
let filter1 : t -> bool
|
|
|
|
let filter1 : t -> bool
|
|
|
|
= fun c ->
|
|
|
|
= fun c ->
|
|
|
|
Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
|
|
|
|
Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
|
|
|
|
|| Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
|
|
|
|
|| Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
|
|
|
|
|| Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
|
|
|
|
|| Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
|
|
|
|
|| (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
|
|
|
|
|| (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
|
|
|
|
|
|
|
|
|
|
|
|
let filter2 : t -> bool
|
|
|
|
let filter2 : t -> bool
|
|
|
|
= fun c ->
|
|
|
|
= fun c ->
|
|
|
|
(* basically, alarms involving infinity are filtered *)
|
|
|
|
(* basically, alarms involving infinity are filtered *)
|
|
|
|
(not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
|
|
|
|
(not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
|
|
|
@ -105,8 +105,8 @@ struct
|
|
|
|
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *)
|
|
|
|
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *)
|
|
|
|
(Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
|
|
|
|
(Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
|
|
|
|
|
|
|
|
|
|
|
|
(* check buffer overrun and return its confidence *)
|
|
|
|
(* check buffer overrun and return its confidence *)
|
|
|
|
let check : t -> string option
|
|
|
|
let check : t -> string option
|
|
|
|
= fun c ->
|
|
|
|
= fun c ->
|
|
|
|
(* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
|
|
|
|
(* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
|
|
|
|
let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
|
|
|
|
let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
|
|
|
@ -136,10 +136,10 @@ struct
|
|
|
|
else
|
|
|
|
else
|
|
|
|
Some Localise.BucketLevel.b2
|
|
|
|
Some Localise.BucketLevel.b2
|
|
|
|
|
|
|
|
|
|
|
|
let invalid : t -> bool
|
|
|
|
let invalid : t -> bool
|
|
|
|
= fun x -> Itv.invalid x.idx || Itv.invalid x.size
|
|
|
|
= fun x -> Itv.invalid x.idx || Itv.invalid x.size
|
|
|
|
|
|
|
|
|
|
|
|
let to_string : t -> string
|
|
|
|
let to_string : t -> string
|
|
|
|
= fun c ->
|
|
|
|
= fun c ->
|
|
|
|
let c = set_size_pos c in
|
|
|
|
let c = set_size_pos c in
|
|
|
|
"Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
|
|
|
|
"Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
|
|
|
@ -150,7 +150,7 @@ struct
|
|
|
|
^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
|
|
|
|
^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
|
|
|
|
| Intra _ -> "")
|
|
|
|
| Intra _ -> "")
|
|
|
|
|
|
|
|
|
|
|
|
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
|
|
|
|
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
|
|
|
|
= fun c subst_map caller_pname callee_pname loc ->
|
|
|
|
= fun c subst_map caller_pname callee_pname loc ->
|
|
|
|
if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
|
|
|
|
if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
|
|
|
|
{ c with idx = Itv.subst c.idx subst_map;
|
|
|
|
{ c with idx = Itv.subst c.idx subst_map;
|
|
|
@ -161,8 +161,7 @@ end
|
|
|
|
|
|
|
|
|
|
|
|
module ConditionSet =
|
|
|
|
module ConditionSet =
|
|
|
|
struct
|
|
|
|
struct
|
|
|
|
module PPSet = PrettyPrintable.MakePPSet (Condition)
|
|
|
|
include AbstractDomain.FiniteSet (Condition)
|
|
|
|
include AbstractDomain.FiniteSet (PPSet)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module Map = Caml.Map.Make (struct
|
|
|
|
module Map = Caml.Map.Make (struct
|
|
|
|
type t = Location.t [@@deriving compare]
|
|
|
|
type t = Location.t [@@deriving compare]
|
|
|
@ -419,28 +418,7 @@ end
|
|
|
|
|
|
|
|
|
|
|
|
module Stack =
|
|
|
|
module Stack =
|
|
|
|
struct
|
|
|
|
struct
|
|
|
|
module PPMap =
|
|
|
|
include AbstractDomain.Map (Loc) (Val)
|
|
|
|
struct
|
|
|
|
|
|
|
|
include PrettyPrintable.MakePPMap (Loc)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp_collection
|
|
|
|
|
|
|
|
: pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
|
|
|
|
|
|
|
|
= fun ~pp_item fmt c ->
|
|
|
|
|
|
|
|
let pp_sep fmt () = F.fprintf fmt ",@," in
|
|
|
|
|
|
|
|
F.pp_print_list ~pp_sep pp_item fmt c
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp
|
|
|
|
|
|
|
|
: pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
|
|
|
|
|
|
|
|
= fun ~pp_value fmt m ->
|
|
|
|
|
|
|
|
let pp_item fmt (k, v) =
|
|
|
|
|
|
|
|
F.fprintf fmt "%a -> %a" Loc.pp k pp_value v
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
F.fprintf fmt "@[<v 2>{ ";
|
|
|
|
|
|
|
|
pp_collection ~pp_item fmt (bindings m);
|
|
|
|
|
|
|
|
F.fprintf fmt " }@]"
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
include AbstractDomain.Map (PPMap) (Val)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let bot = empty
|
|
|
|
let bot = empty
|
|
|
|
|
|
|
|
|
|
|
@ -493,7 +471,7 @@ struct
|
|
|
|
F.fprintf fmt " }@]"
|
|
|
|
F.fprintf fmt " }@]"
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
include AbstractDomain.Map (PPMap) (Val)
|
|
|
|
include AbstractDomain.Map (Loc) (Val)
|
|
|
|
|
|
|
|
|
|
|
|
let bot = empty
|
|
|
|
let bot = empty
|
|
|
|
|
|
|
|
|
|
|
@ -549,10 +527,10 @@ struct
|
|
|
|
match M.find k rhs with
|
|
|
|
match M.find k rhs with
|
|
|
|
| v' -> Pvar.equal v v'
|
|
|
|
| v' -> Pvar.equal v v'
|
|
|
|
| exception Not_found -> false
|
|
|
|
| exception Not_found -> false
|
|
|
|
in
|
|
|
|
in
|
|
|
|
M.for_all is_in_rhs lhs
|
|
|
|
M.for_all is_in_rhs lhs
|
|
|
|
|
|
|
|
|
|
|
|
let join : t -> t -> t
|
|
|
|
let join : t -> t -> t
|
|
|
|
= fun x y ->
|
|
|
|
= fun x y ->
|
|
|
|
let join_v _ v1_opt v2_opt =
|
|
|
|
let join_v _ v1_opt v2_opt =
|
|
|
|
match v1_opt, v2_opt with
|
|
|
|
match v1_opt, v2_opt with
|
|
|
@ -563,10 +541,10 @@ let join : t -> t -> t
|
|
|
|
in
|
|
|
|
in
|
|
|
|
M.merge join_v x y
|
|
|
|
M.merge join_v x y
|
|
|
|
|
|
|
|
|
|
|
|
let widen : prev:t -> next:t -> num_iters:int -> t
|
|
|
|
let widen : prev:t -> next:t -> num_iters:int -> t
|
|
|
|
= fun ~prev ~next ~num_iters:_ -> join prev next
|
|
|
|
= fun ~prev ~next ~num_iters:_ -> join prev next
|
|
|
|
|
|
|
|
|
|
|
|
let pp : F.formatter -> t -> unit
|
|
|
|
let pp : F.formatter -> t -> unit
|
|
|
|
= fun fmt x ->
|
|
|
|
= fun fmt x ->
|
|
|
|
let pp_sep fmt () = F.fprintf fmt ", @," in
|
|
|
|
let pp_sep fmt () = F.fprintf fmt ", @," in
|
|
|
|
let pp1 fmt (k, v) =
|
|
|
|
let pp1 fmt (k, v) =
|
|
|
@ -578,19 +556,19 @@ let pp : F.formatter -> t -> unit
|
|
|
|
F.fprintf fmt " }@]";
|
|
|
|
F.fprintf fmt " }@]";
|
|
|
|
F.fprintf fmt "@]"
|
|
|
|
F.fprintf fmt "@]"
|
|
|
|
|
|
|
|
|
|
|
|
let load : Ident.t -> Exp.t -> t -> t
|
|
|
|
let load : Ident.t -> Exp.t -> t -> t
|
|
|
|
= fun id exp m ->
|
|
|
|
= fun id exp m ->
|
|
|
|
match exp with
|
|
|
|
match exp with
|
|
|
|
| Exp.Lvar x -> M.add id x m
|
|
|
|
| Exp.Lvar x -> M.add id x m
|
|
|
|
| _ -> m
|
|
|
|
| _ -> m
|
|
|
|
|
|
|
|
|
|
|
|
let store : Exp.t -> Exp.t -> t -> t
|
|
|
|
let store : Exp.t -> Exp.t -> t -> t
|
|
|
|
= fun e _ m ->
|
|
|
|
= fun e _ m ->
|
|
|
|
match e with
|
|
|
|
match e with
|
|
|
|
| Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m
|
|
|
|
| Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m
|
|
|
|
| _ -> m
|
|
|
|
| _ -> m
|
|
|
|
|
|
|
|
|
|
|
|
let find : Ident.t -> t -> Pvar.t option
|
|
|
|
let find : Ident.t -> t -> Pvar.t option
|
|
|
|
= fun k m -> try Some (M.find k m) with Not_found -> None
|
|
|
|
= fun k m -> try Some (M.find k m) with Not_found -> None
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|