[Inferbo] Add relational domains

Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.

- Each Mem domain value includes one relational value containing relations among symbols.  The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three symbols, which represent integer value, array offset, and array size of an abstract value.

The relational domain is deactivated by default. Use the `--bo-relational-domain {oct, poly}` option for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.

Reviewed By: jvillard

Differential Revision: D8874102

fbshipit-source-id: 08e5883cb
master
Sungkeun Cho 7 years ago committed by Facebook Github Bot
parent d90a87d743
commit 9eca72d405

@ -24,12 +24,14 @@ is required to compile everything from source.
`xcode-select --install` (only needed for the C/Objective-C analysis) `xcode-select --install` (only needed for the C/Objective-C analysis)
- Xcode >= 6.1 (only needed for the C/Objective-C analysis) - Xcode >= 6.1 (only needed for the C/Objective-C analysis)
- autoconf >= 2.63 and automake >= 1.11.1 (if building from git) - autoconf >= 2.63 and automake >= 1.11.1 (if building from git)
- gmp
- mpfr
You can install some of these dependencies using You can install some of these dependencies using
[Homebrew](http://brew.sh/): [Homebrew](http://brew.sh/):
```sh ```sh
brew install autoconf automake cmake opam pkg-config sqlite brew install autoconf automake cmake opam pkg-config sqlite gmp mpfr
brew cask install java brew cask install java
``` ```

@ -18,6 +18,7 @@ CFLAGS = @CFLAGS@
CLANG_INCLUDES = @CLANG_INCLUDES@ CLANG_INCLUDES = @CLANG_INCLUDES@
CLANG_PREFIX = @CLANG_PREFIX@ CLANG_PREFIX = @CLANG_PREFIX@
CMAKE = @CMAKE@ CMAKE = @CMAKE@
CPATH = @CPATH@
CPP = @CPP@ CPP = @CPP@
CXX = @CXX@ CXX = @CXX@
CXXFLAGS = @CXXFLAGS@ CXXFLAGS = @CXXFLAGS@
@ -42,6 +43,7 @@ LDFLAGS = @LDFLAGS@
libdir = @libdir@ libdir = @libdir@
# override in your `make` command to make the install relocatable # override in your `make` command to make the install relocatable
libdir_relative_to_bindir = $(libdir) libdir_relative_to_bindir = $(libdir)
LIBRARY_PATH = @LIBRARY_PATH@
LIBS = @LIBS@ LIBS = @LIBS@
mandir = @mandir@ mandir = @mandir@
MENHIR = @MENHIR@ MENHIR = @MENHIR@
@ -61,6 +63,7 @@ OCAMLOPT = @OCAMLOPT@
OPAM = @OPAM@ OPAM = @OPAM@
OPAMROOT = @OPAMROOT@ OPAMROOT = @OPAMROOT@
OPAMSWITCH = @OPAMSWITCH@ OPAMSWITCH = @OPAMSWITCH@
PATCHELF = @PATCHELF@
PATH = @PATH@ PATH = @PATH@
prefix = @prefix@ prefix = @prefix@
PYTHON_lxml = @PYTHON_lxml@ PYTHON_lxml = @PYTHON_lxml@
@ -79,5 +82,7 @@ endif
# Export parts of the config relevant to running other programs # Export parts of the config relevant to running other programs
export PATH := $(PATH) export PATH := $(PATH)
export CPATH := $(CPATH)
export LIBRARY_PATH := $(LIBRARY_PATH)
export CAML_LD_LIBRARY_PATH := $(CAML_LD_LIBRARY_PATH) export CAML_LD_LIBRARY_PATH := $(CAML_LD_LIBRARY_PATH)
export OPAMROOT := $(OPAMROOT) export OPAMROOT := $(OPAMROOT)

@ -192,6 +192,8 @@ AC_ASSERT_OCAML_PKG([oUnit], [], [2.0.0])
AC_CHECK_TOOL([UTOP], [utop], [no]) AC_CHECK_TOOL([UTOP], [utop], [no])
AC_ASSERT_OCAML_PKG([yojson]) AC_ASSERT_OCAML_PKG([yojson])
AC_ARG_VAR([CPATH], [Additional directories to search for C headers.])
AC_ARG_VAR([LIBRARY_PATH], [Additional directories to search for C shared objects.])
AC_ARG_VAR([CAML_LD_LIBRARY_PATH], AC_ARG_VAR([CAML_LD_LIBRARY_PATH],
[Additional directories to search for dynamically-loaded libraries.]) [Additional directories to search for dynamically-loaded libraries.])
AC_ARG_VAR([OPAMROOT], [Root of the local opam installation.]) AC_ARG_VAR([OPAMROOT], [Root of the local opam installation.])
@ -324,6 +326,8 @@ AC_SUBST([GNU_SED])
AC_CHECK_TOOL([BREW], [brew], [no]) AC_CHECK_TOOL([BREW], [brew], [no])
AC_CHECK_TOOL([PATCHELF], [patchelf], [no])
# warn about broken pkg-config version for brew users # warn about broken pkg-config version for brew users
if test "$BREW" != "no"; then if test "$BREW" != "no"; then
if "$BREW" info pkg-config > /dev/null && \ if "$BREW" info pkg-config > /dev/null && \

@ -93,7 +93,7 @@ struct
in in
if debug then ( if debug then (
L.d_strln L.d_strln
(Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre (Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre
(Instrs.pp Pp.(html Green)) (Instrs.pp Pp.(html Green))
instrs Domain.pp astate_post) ; instrs Domain.pp astate_post) ;
NodePrinter.finish_session (Node.underlying_node node) ) ; NodePrinter.finish_session (Node.underlying_node node) ) ;

@ -821,6 +821,13 @@ and blacklist =
~meta:"regex" "Skip analysis of files matched by the specified regular expression" ~meta:"regex" "Skip analysis of files matched by the specified regular expression"
and bo_relational_domain =
CLOpt.mk_symbol_opt ~long:"bo-relational-domain"
~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
~symbols:[("oct", `Bo_relational_domain_oct); ("poly", `Bo_relational_domain_poly)]
"Select a relational domain being used in the bufferoverrun checker (experimental)"
and bootclasspath = and bootclasspath =
CLOpt.mk_string_opt ~long:"bootclasspath" CLOpt.mk_string_opt ~long:"bootclasspath"
~in_help:InferCommand.[(Capture, manual_java)] ~in_help:InferCommand.[(Capture, manual_java)]
@ -2443,6 +2450,8 @@ and bootclasspath = !bootclasspath
and bo_debug = !bo_debug and bo_debug = !bo_debug
and bo_relational_domain = !bo_relational_domain
and buck = !buck and buck = !buck
and buck_build_args = !buck_build_args and buck_build_args = !buck_build_args

@ -240,6 +240,8 @@ val bootclasspath : string option
val bo_debug : int val bo_debug : int
val bo_relational_domain : [`Bo_relational_domain_oct | `Bo_relational_domain_poly] option
val buck : bool val buck : bool
val buck_build_args : string list val buck_build_args : string list

@ -42,6 +42,8 @@ module Loc = struct
F.fprintf fmt "%a.%a" pp l Typ.Fieldname.pp f F.fprintf fmt "%a.%a" pp l Typ.Fieldname.pp f
let to_string x = F.asprintf "%a" pp x
let is_var = function Var _ -> true | _ -> false let is_var = function Var _ -> true | _ -> false
let rec contains_allocsite = function let rec contains_allocsite = function
@ -89,3 +91,12 @@ module PowLoc = struct
let is_singleton x = Int.equal (cardinal x) 1 let is_singleton x = Int.equal (cardinal x) 1
end end
(** unsound but ok for bug catching *)
let always_strong_update = true
let can_strong_update : PowLoc.t -> bool =
fun ploc ->
if always_strong_update then true
else if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc)
else false

@ -13,6 +13,7 @@ open AbsLoc
open! AbstractDomain.Types open! AbstractDomain.Types
module BoUtils = BufferOverrunUtils module BoUtils = BufferOverrunUtils
module Dom = BufferOverrunDomain module Dom = BufferOverrunDomain
module Relation = BufferOverrunDomainRelation
module L = Logging module L = Logging
module Models = BufferOverrunModels module Models = BufferOverrunModels
module Sem = BufferOverrunSemantics module Sem = BufferOverrunSemantics
@ -47,16 +48,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Typ.Tint ikind -> | Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in let unsigned = Typ.ikind_is_unsigned ikind in
let v = let v =
Dom.Val.make_sym ~unsigned pname path new_sym_num Dom.Val.make_sym ~unsigned loc pname path new_sym_num
|> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
in in
Dom.Mem.add_heap loc v mem mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tfloat _ -> | Typ.Tfloat _ ->
let v = let v =
Dom.Val.make_sym pname path new_sym_num Dom.Val.make_sym loc pname path new_sym_num
|> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
in in
Dom.Mem.add_heap loc v mem mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tptr (typ, _) when Language.curr_language_is Java && not (Typ.is_array typ) -> | Typ.Tptr (typ, _) when Language.curr_language_is Java && not (Typ.is_array typ) ->
BoUtils.Exec.decl_sym_java_ptr BoUtils.Exec.decl_sym_java_ptr
~decl_sym_val:(decl_sym_val ~may_last_field:false) ~decl_sym_val:(decl_sym_val ~may_last_field:false)
@ -186,6 +187,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem
let forget_ret_relation ret callee_pname mem =
let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
let ret_var = Loc.of_var (Var.of_id (fst ret)) in
Dom.Mem.forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem
let instantiate_mem let instantiate_mem
: Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list : Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list
-> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate = -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate =
@ -195,12 +202,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in
match callee_pdesc with match callee_pdesc with
| Some pdesc -> | Some pdesc ->
let subst_map, ret_alias = let bound_subst_map, ret_alias, rel_subst_map =
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias
in in
instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map caller_mem let caller_mem =
ret_alias location instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem bound_subst_map
|> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location caller_mem ret_alias location
|> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem bound_subst_map
location
|> forget_ret_relation ret callee_pname
in
Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
| None -> | None ->
caller_mem caller_mem
@ -228,6 +240,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Store (exp1, _, exp2, location) -> | Store (exp1, _, exp2, location) ->
let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in
let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in
let mem =
let sym_exps =
Dom.Relation.SymExp.of_exps ~get_int_sym_f:(Sem.get_sym_f mem)
~get_offset_sym_f:(Sem.get_offset_sym_f mem)
~get_size_sym_f:(Sem.get_size_sym_f mem) exp2
in
Dom.Mem.store_relation locs sym_exps mem
in
let mem = Dom.Mem.update_mem locs v mem in let mem = Dom.Mem.update_mem locs v mem in
let mem = let mem =
if PowLoc.is_singleton locs then if PowLoc.is_singleton locs then
@ -368,7 +388,9 @@ module Report = struct
fun pname ~is_plus ~e1 ~e2 location mem cond_set -> fun pname ~is_plus ~e1 ~e2 location mem cond_set ->
let arr = Sem.eval e1 mem in let arr = Sem.eval e1 mem in
let idx = Sem.eval e2 mem in let idx = Sem.eval e2 mem in
BoUtils.Check.array_access ~arr ~idx ~is_plus pname location cond_set let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) e2 in
let relation = Dom.Mem.get_relation mem in
BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set
let check_binop let check_binop
@ -407,7 +429,10 @@ module Report = struct
match exp with match exp with
| Exp.Var _ -> | Exp.Var _ ->
let arr = Sem.eval exp mem in let arr = Sem.eval exp mem in
BoUtils.Check.array_access ~arr ~idx:Dom.Val.Itv.zero ~is_plus:true pname location cond_set let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in
let relation = Dom.Mem.get_relation mem in
BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location
cond_set
| Exp.BinOp (bop, e1, e2) -> | Exp.BinOp (bop, e1, e2) ->
check_binop pname ~bop ~e1 ~e2 location mem cond_set check_binop pname ~bop ~e1 ~e2 location mem cond_set
| _ -> | _ ->
@ -422,11 +447,13 @@ module Report = struct
let callee_cond = Dom.Summary.get_cond_set summary in let callee_cond = Dom.Summary.get_cond_set summary in
match callee_pdesc with match callee_pdesc with
| Some pdesc -> | Some pdesc ->
let subst_map, _ = let bound_subst_map, _, rel_subst_map =
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None
in in
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
PO.ConditionSet.subst callee_cond subst_map caller_pname pname location let caller_rel = Dom.Mem.get_relation caller_mem in
PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel caller_pname
pname location
| _ -> | _ ->
callee_cond callee_cond
@ -562,6 +589,9 @@ module Report = struct
Reporting.log_error summary ~loc:location ~ltr:trace exn Reporting.log_error summary ~loc:location ~ltr:trace exn
in in
PO.ConditionSet.check_all ~report cond_set PO.ConditionSet.check_all ~report cond_set
let forget_locs = PO.ConditionSet.forget_locs
end end
let extract_pre = Analyzer.extract_pre let extract_pre = Analyzer.extract_pre
@ -574,16 +604,34 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit =
"@\n@[<v 2>Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s "@\n@[<v 2>Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s
let get_local_decls cfg =
let accum_pvar_list acc pvars =
List.fold pvars ~init:acc ~f:(fun acc (pvar, _) -> PowLoc.add (Loc.of_pvar pvar) acc)
in
let accum_decls_of_instr acc instr =
match instr with Sil.Declare_locals (vars, _) -> accum_pvar_list acc vars | _ -> acc
in
let accum_decls_of_node acc node =
Instrs.fold (CFG.instrs node) ~init:acc ~f:accum_decls_of_instr
in
let decls = CFG.fold_nodes cfg ~init:PowLoc.empty ~f:accum_decls_of_node in
let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name cfg)) in
PowLoc.remove ret_loc decls
let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t = let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
fun {proc_desc; tenv; summary} -> fun {proc_desc; tenv; summary} ->
Preanal.do_preanalysis proc_desc tenv ; Preanal.do_preanalysis proc_desc tenv ;
let pdata = ProcData.make_default proc_desc tenv in let pdata = ProcData.make_default proc_desc tenv in
let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in
let cfg = CFG.from_pdesc proc_desc in let cfg = CFG.from_pdesc proc_desc in
let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map in let locals = get_local_decls cfg in
let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map in let forget_locals mem = Option.map ~f:(Dom.Mem.forget_locs locals) mem in
let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map |> forget_locals in
let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map |> forget_locals in
let cond_set = let cond_set =
Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc
|> Report.forget_locs locals
in in
let summary = let summary =
match (entry_mem, exit_mem) with match (entry_mem, exit_mem) with

@ -13,31 +13,54 @@ open AbsLoc
open! AbstractDomain.Types open! AbstractDomain.Types
module F = Format module F = Format
module L = Logging module L = Logging
module Relation = BufferOverrunDomainRelation
module PO = BufferOverrunProofObligations module PO = BufferOverrunProofObligations
module Trace = BufferOverrunTrace module Trace = BufferOverrunTrace
module TraceSet = Trace.Set module TraceSet = Trace.Set
(** unsound but ok for bug catching *)
let always_strong_update = true
module Val = struct module Val = struct
type astate = type astate =
{itv: Itv.astate; powloc: PowLoc.astate; arrayblk: ArrayBlk.astate; traces: TraceSet.t} { itv: Itv.astate
; sym: Relation.Sym.astate
; powloc: PowLoc.astate
; arrayblk: ArrayBlk.astate
; offset_sym: Relation.Sym.astate
; size_sym: Relation.Sym.astate
; traces: TraceSet.t }
type t = astate type t = astate
let bot : t = {itv= Itv.bot; powloc= PowLoc.bot; arrayblk= ArrayBlk.bot; traces= TraceSet.empty} let bot : t =
{ itv= Itv.bot
; sym= Relation.Sym.bot
; powloc= PowLoc.bot
; arrayblk= ArrayBlk.bot
; offset_sym= Relation.Sym.bot
; size_sym= Relation.Sym.bot
; traces= TraceSet.empty }
let pp fmt x = let pp fmt x =
if Config.bo_debug <= 1 then let relation_sym_pp fmt sym =
F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym
else in
F.fprintf fmt "(%a, %a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk let trace_pp fmt traces =
TraceSet.pp x.traces if Config.bo_debug <= 1 then F.fprintf fmt ", %a" TraceSet.pp traces
in
F.fprintf fmt "(%a%a, %a, %a%a%a%a)" Itv.pp x.itv relation_sym_pp x.sym PowLoc.pp x.powloc
ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp
x.traces
let unknown : traces:TraceSet.t -> t = let unknown : traces:TraceSet.t -> t =
fun ~traces -> {itv= Itv.top; powloc= PowLoc.unknown; arrayblk= ArrayBlk.unknown; traces} fun ~traces ->
{ itv= Itv.top
; sym= Relation.Sym.top
; powloc= PowLoc.unknown
; arrayblk= ArrayBlk.unknown
; offset_sym= Relation.Sym.top
; size_sym= Relation.Sym.top
; traces }
let unknown_from : callee_pname:_ -> location:_ -> t = let unknown_from : callee_pname:_ -> location:_ -> t =
@ -51,8 +74,11 @@ module Val = struct
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true
else else
Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym
&& PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc
&& ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk
&& Relation.Sym.( <= ) ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym
&& Relation.Sym.( <= ) ~lhs:lhs.size_sym ~rhs:rhs.size_sym
let equal x y = phys_equal x y || (( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x) let equal x y = phys_equal x y || (( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x)
@ -61,8 +87,11 @@ module Val = struct
if phys_equal prev next then prev if phys_equal prev next then prev
else else
{ itv= Itv.widen ~prev:prev.itv ~next:next.itv ~num_iters { itv= Itv.widen ~prev:prev.itv ~next:next.itv ~num_iters
; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters
; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters
; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters
; offset_sym= Relation.Sym.widen ~prev:prev.offset_sym ~next:next.offset_sym ~num_iters
; size_sym= Relation.Sym.widen ~prev:prev.size_sym ~next:next.size_sym ~num_iters
; traces= TraceSet.join prev.traces next.traces } ; traces= TraceSet.join prev.traces next.traces }
@ -71,13 +100,20 @@ module Val = struct
if phys_equal x y then x if phys_equal x y then x
else else
{ itv= Itv.join x.itv y.itv { itv= Itv.join x.itv y.itv
; sym= Relation.Sym.join x.sym y.sym
; powloc= PowLoc.join x.powloc y.powloc ; powloc= PowLoc.join x.powloc y.powloc
; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk
; offset_sym= Relation.Sym.join x.offset_sym y.offset_sym
; size_sym= Relation.Sym.join x.size_sym y.size_sym
; traces= TraceSet.join x.traces y.traces } ; traces= TraceSet.join x.traces y.traces }
let get_itv : t -> Itv.t = fun x -> x.itv let get_itv : t -> Itv.t = fun x -> x.itv
let get_sym : t -> Relation.Sym.astate = fun x -> x.sym
let get_sym_var : t -> Relation.Var.t option = fun x -> Relation.Sym.get_var x.sym
let get_pow_loc : t -> PowLoc.t = fun x -> x.powloc let get_pow_loc : t -> PowLoc.t = fun x -> x.powloc
let get_array_blk : t -> ArrayBlk.astate = fun x -> x.arrayblk let get_array_blk : t -> ArrayBlk.astate = fun x -> x.arrayblk
@ -86,6 +122,10 @@ module Val = struct
let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x) let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x)
let get_offset_sym : t -> Relation.Sym.astate = fun x -> x.offset_sym
let get_size_sym : t -> Relation.Sym.astate = fun x -> x.size_sym
let get_traces : t -> TraceSet.t = fun x -> x.traces let get_traces : t -> TraceSet.t = fun x -> x.traces
let set_traces : TraceSet.t -> t -> t = fun traces x -> {x with traces} let set_traces : TraceSet.t -> t -> t = fun traces x -> {x with traces}
@ -96,20 +136,29 @@ module Val = struct
let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x}
let of_array_blk : ArrayBlk.astate -> t = fun a -> {bot with arrayblk= a} let of_array_blk : allocsite:Allocsite.t -> ArrayBlk.astate -> t =
fun ~allocsite a ->
{ bot with
arrayblk= a
; offset_sym= Relation.Sym.of_allocsite_offset allocsite
; size_sym= Relation.Sym.of_allocsite_size allocsite }
let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
let make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t = let make_sym
fun ?(unsigned= false) pname path new_sym_num -> : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t =
{bot with itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num} fun ?(unsigned= false) loc pname path new_sym_num ->
{ bot with
itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num
; sym= Relation.Sym.of_loc loc }
let unknown_bit : t -> t = fun x -> {x with itv= Itv.top} let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv} let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top}
let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool} let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool; sym= Relation.Sym.top}
let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces} fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces}
@ -297,6 +346,15 @@ module Heap = struct
fun ~f locs mem -> PowLoc.fold (fun loc -> find loc mem |> f |> add loc) locs mem fun ~f locs mem -> PowLoc.fold (fun loc -> find loc mem |> f |> add loc) locs mem
let add x v =
let sym = if Itv.is_empty (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x in
let offset_sym, size_sym =
if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot)
else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x)
in
add x {v with Val.sym; Val.offset_sym; Val.size_sym}
let strong_update : PowLoc.t -> Val.t -> astate -> astate = let strong_update : PowLoc.t -> Val.t -> astate -> astate =
fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem
@ -398,10 +456,9 @@ module AliasMap = struct
let pp_sep fmt () = F.fprintf fmt ", @," in let pp_sep fmt () = F.fprintf fmt ", @," in
let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in
(* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *) (* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *)
F.fprintf fmt "@[<hov 2>{ @," ; F.fprintf fmt "@[<hov 2>{ " ;
F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ;
F.fprintf fmt " }@]" ; F.fprintf fmt " }@]"
F.fprintf fmt "@]"
let load : Ident.t -> AliasTarget.t -> t -> t = fun id loc m -> M.add id loc m let load : Ident.t -> AliasTarget.t -> t -> t = fun id loc m -> M.add id loc m
@ -508,7 +565,7 @@ module Alias = struct
let pp : F.formatter -> astate -> unit = let pp : F.formatter -> astate -> unit =
fun fmt (aliasmap, aliasret) -> fun fmt (aliasmap, aliasret) ->
F.fprintf fmt "AliasMap:@;%a@;AliasRet:@;%a@;" AliasMap.pp aliasmap AliasRet.pp aliasret F.fprintf fmt "AliasMap:@;%a@;AliasRet:@;%a" AliasMap.pp aliasmap AliasRet.pp aliasret
end end
module PrunePairs = struct module PrunePairs = struct
@ -595,11 +652,21 @@ end
module MemReach = struct module MemReach = struct
type astate = type astate =
{stack: Stack.astate; heap: Heap.astate; alias: Alias.astate; latest_prune: LatestPrune.astate} { stack: Stack.astate
; heap: Heap.astate
; alias: Alias.astate
; latest_prune: LatestPrune.astate
; relation: Relation.astate }
type t = astate type t = astate
let init : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot; latest_prune= LatestPrune.top} let init : t =
{ stack= Stack.bot
; heap= Heap.bot
; alias= Alias.bot
; latest_prune= LatestPrune.top
; relation= Relation.empty }
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true
@ -607,6 +674,7 @@ module MemReach = struct
Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap
&& Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias
&& LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune
&& Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation
let widen ~prev ~next ~num_iters = let widen ~prev ~next ~num_iters =
@ -616,7 +684,7 @@ module MemReach = struct
; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters
; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters
; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters
} ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters }
let join : t -> t -> t = let join : t -> t -> t =
@ -624,12 +692,15 @@ module MemReach = struct
{ stack= Stack.join x.stack y.stack { stack= Stack.join x.stack y.stack
; heap= Heap.join x.heap y.heap ; heap= Heap.join x.heap y.heap
; alias= Alias.join x.alias y.alias ; alias= Alias.join x.alias y.alias
; latest_prune= LatestPrune.join x.latest_prune y.latest_prune } ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune
; relation= Relation.join x.relation y.relation }
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt x -> fun fmt x ->
F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias ;
if Option.is_some Config.bo_relational_domain then
F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
let pp_summary : F.formatter -> t -> unit = let pp_summary : F.formatter -> t -> unit =
@ -691,13 +762,6 @@ module MemReach = struct
let get_return : t -> Val.t = fun m -> Heap.get_return m.heap let get_return : t -> Val.t = fun m -> Heap.get_return m.heap
let can_strong_update : PowLoc.t -> bool =
fun ploc ->
if always_strong_update then true
else if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc)
else false
let update_mem : PowLoc.t -> Val.t -> t -> t = let update_mem : PowLoc.t -> Val.t -> t -> t =
fun ploc v s -> fun ploc v s ->
if can_strong_update ploc then strong_update_heap ploc v s if can_strong_update ploc then strong_update_heap ploc v s
@ -770,6 +834,41 @@ module MemReach = struct
let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate = let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate =
fun ~filter_loc {heap} -> Heap.range ~filter_loc heap fun ~filter_loc {heap} -> Heap.range ~filter_loc heap
let get_relation : t -> Relation.astate = fun m -> m.relation
let is_relation_unsat : t -> bool = fun m -> Relation.is_unsat m.relation
let lift_relation : (Relation.astate -> Relation.astate) -> t -> t =
fun f m -> {m with relation= f m.relation}
let meet_constraints : Relation.Constraints.t -> t -> t =
fun constrs -> lift_relation (Relation.meet_constraints constrs)
let store_relation
: PowLoc.t -> Relation.SymExp.t option * Relation.SymExp.t option * Relation.SymExp.t option
-> t -> t =
fun locs symexp_opts -> lift_relation (Relation.store_relation locs symexp_opts)
let forget_locs : PowLoc.t -> t -> t = fun locs -> lift_relation (Relation.forget_locs locs)
let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc)
let init_array_relation
: Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t
-> t =
fun allocsite ~offset ~size ~size_exp_opt ->
lift_relation (Relation.init_array allocsite ~offset ~size ~size_exp_opt)
let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t =
fun subst_map ~caller ~callee ->
{ caller with
relation= Relation.instantiate subst_map ~caller:caller.relation ~callee:callee.relation }
end end
module Mem = struct module Mem = struct
@ -896,6 +995,42 @@ module Mem = struct
let update_latest_prune : Exp.t -> Exp.t -> t -> t = let update_latest_prune : Exp.t -> Exp.t -> t -> t =
fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2) fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2)
let get_relation : t -> Relation.astate =
fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m
let meet_constraints : Relation.Constraints.t -> t -> t =
fun constrs -> f_lift (MemReach.meet_constraints constrs)
let is_relation_unsat m = f_lift_default ~default:true MemReach.is_relation_unsat m
let store_relation
: PowLoc.t -> Relation.SymExp.t option * Relation.SymExp.t option * Relation.SymExp.t option
-> t -> t =
fun locs symexp_opts -> f_lift (MemReach.store_relation locs symexp_opts)
let forget_locs : PowLoc.t -> t -> t = fun locs -> f_lift (MemReach.forget_locs locs)
let init_param_relation : Loc.t -> t -> t = fun loc -> f_lift (MemReach.init_param_relation loc)
let init_array_relation
: Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t
-> t =
fun allocsite ~offset ~size ~size_exp_opt ->
f_lift (MemReach.init_array_relation allocsite ~offset ~size ~size_exp_opt)
let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t =
fun subst_map ~caller ~callee ->
match callee with
| Bottom ->
caller
| NonBottom callee ->
f_lift (fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller
end end
module Summary = struct module Summary = struct
@ -923,5 +1058,5 @@ module Summary = struct
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt (entry_mem, exit_mem, condition_set) -> fun fmt (entry_mem, exit_mem, condition_set) ->
F.fprintf fmt "%a@,%a@,%a@," Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set F.fprintf fmt "%a@;%a@;%a" Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set
end end

File diff suppressed because it is too large Load Diff

@ -13,6 +13,7 @@ module BoUtils = BufferOverrunUtils
module Dom = BufferOverrunDomain module Dom = BufferOverrunDomain
module PO = BufferOverrunProofObligations module PO = BufferOverrunProofObligations
module Sem = BufferOverrunSemantics module Sem = BufferOverrunSemantics
module Relation = BufferOverrunDomainRelation
module Trace = BufferOverrunTrace module Trace = BufferOverrunTrace
module TraceSet = Trace.Set module TraceSet = Trace.Set
@ -86,12 +87,17 @@ let malloc size_exp =
let typ, stride, length0, dyn_length = get_malloc_info size_exp in let typ, stride, length0, dyn_length = get_malloc_info size_exp in
let length = Sem.eval length0 mem in let length = Sem.eval length0 mem in
let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in
let offset, size = (Itv.zero, Dom.Val.get_itv length) in
let size_exp_opt =
let size_exp = Option.value dyn_length ~default:length0 in
Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) size_exp
in
let v = let v =
Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero Sem.eval_array_alloc allocsite typ ~stride ~offset ~size |> Dom.Val.set_traces traces
~size:(Dom.Val.get_itv length) ~inst_num:0 ~dimension:1
|> Dom.Val.set_traces traces
in in
mem |> Dom.Mem.add_stack (Loc.of_id id) v mem |> Dom.Mem.add_stack (Loc.of_id id) v
|> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt
|> set_uninitialized location typ (Dom.Val.get_array_locs v) |> set_uninitialized location typ (Dom.Val.get_array_locs v)
|> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v) |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v)
?dyn_length ?dyn_length
@ -182,10 +188,8 @@ let set_array_length array length_exp =
| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
let stride = Option.map ~f:IntLit.to_int_exn stride in let stride = Option.map ~f:IntLit.to_int_exn stride in
let v = let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in
Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length let v = Sem.eval_array_alloc allocsite elt ~stride ~offset:Itv.zero ~size:length in
~inst_num:0 ~dimension:1
in
mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
|> set_uninitialized location elt (Dom.Val.get_array_locs v) |> set_uninitialized location elt (Dom.Val.get_array_locs v)
| _ -> | _ ->

@ -10,6 +10,7 @@ open! AbstractDomain.Types
module F = Format module F = Format
module L = Logging module L = Logging
module ItvPure = Itv.ItvPure module ItvPure = Itv.ItvPure
module Relation = BufferOverrunDomainRelation
module MF = MarkupFormatter module MF = MarkupFormatter
module ValTraceSet = BufferOverrunTrace.Set module ValTraceSet = BufferOverrunTrace.Set
@ -93,7 +94,13 @@ module AllocSizeCondition = struct
end end
module ArrayAccessCondition = struct module ArrayAccessCondition = struct
type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare] type t =
{ idx: ItvPure.astate
; size: ItvPure.astate
; idx_sym_exp: Relation.SymExp.t option
; size_sym_exp: Relation.SymExp.t option
; relation: Relation.astate }
[@@deriving compare]
let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size
@ -106,7 +113,10 @@ module ArrayAccessCondition = struct
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
F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size ;
if Option.is_some Config.bo_relational_domain then
F.fprintf fmt "@,%a < %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp Relation.SymExp.pp_opt
c.size_sym_exp Relation.pp c.relation
let pp_description : F.formatter -> t -> unit = let pp_description : F.formatter -> t -> unit =
@ -115,9 +125,12 @@ module ArrayAccessCondition = struct
F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size
let make : idx:ItvPure.t -> size:ItvPure.t -> t option = let make
fun ~idx ~size -> : idx:ItvPure.t -> size:ItvPure.t -> idx_sym_exp:Relation.SymExp.t option
if ItvPure.is_invalid idx || ItvPure.is_invalid size then None else Some {idx; size} -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.astate -> t option =
fun ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation ->
if ItvPure.is_invalid idx || ItvPure.is_invalid size then None
else Some {idx; size; idx_sym_exp; size_sym_exp; relation}
let have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} = let have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} =
@ -209,9 +222,15 @@ module ArrayAccessCondition = struct
let c' = set_size_pos c in let c' = set_size_pos c in
(* if sl < 0, use sl' = 0 *) (* if sl < 0, use sl' = 0 *)
let not_overrun = let not_overrun =
if is_arraylist_add then ItvPure.le_sem c'.idx c'.size else ItvPure.lt_sem c'.idx c'.size if is_arraylist_add then ItvPure.le_sem c'.idx c'.size
else if Relation.lt_sat_opt c'.idx_sym_exp c'.size_sym_exp c'.relation then Itv.Boolean.true_
else ItvPure.lt_sem c'.idx c'.size
in
let not_underrun =
if Relation.le_sat_opt (Some Relation.SymExp.zero) c'.idx_sym_exp c'.relation then
Itv.Boolean.true_
else ItvPure.le_sem ItvPure.zero c'.idx
in in
let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in
(* il >= 0 and iu < sl, definitely not an error *) (* il >= 0 and iu < sl, definitely not an error *)
if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then
{report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *) {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *)
@ -239,13 +258,22 @@ module ArrayAccessCondition = struct
{report_issue_type; propagate= is_symbolic} {report_issue_type; propagate= is_symbolic}
let subst : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t -> t option = let subst
fun bound_map c -> : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> Relation.SubstMap.t -> Relation.astate -> t
-> t option =
fun bound_map rel_map caller_relation c ->
match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with
| NonBottom idx, NonBottom size -> | NonBottom idx, NonBottom size ->
Some {idx; size} let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in
let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in
let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in
Some {idx; size; idx_sym_exp; size_sym_exp; relation}
| _ -> | _ ->
None None
let forget_locs : AbsLoc.PowLoc.t -> t -> t =
fun locs c -> {c with relation= Relation.forget_locs locs c.relation}
end end
module Condition = struct module Condition = struct
@ -266,11 +294,12 @@ module Condition = struct
ArrayAccessCondition.get_symbols c ArrayAccessCondition.get_symbols c
let subst bound_map = function let subst bound_map rel_map caller_relation = function
| AllocSize c -> | AllocSize c ->
AllocSizeCondition.subst bound_map c |> make_alloc_size AllocSizeCondition.subst bound_map c |> make_alloc_size
| ArrayAccess {is_arraylist_add; c} -> | ArrayAccess {is_arraylist_add; c} ->
ArrayAccessCondition.subst bound_map c |> make_array_access ~is_arraylist_add ArrayAccessCondition.subst bound_map rel_map caller_relation c
|> make_array_access ~is_arraylist_add
let have_similar_bounds c1 c2 = let have_similar_bounds c1 c2 =
@ -315,6 +344,14 @@ module Condition = struct
AllocSizeCondition.check c AllocSizeCondition.check c
| ArrayAccess {is_arraylist_add; c} -> | ArrayAccess {is_arraylist_add; c} ->
ArrayAccessCondition.check ~is_arraylist_add c ArrayAccessCondition.check ~is_arraylist_add c
let forget_locs locs x =
match x with
| ArrayAccess {is_arraylist_add; c} ->
ArrayAccess {is_arraylist_add; c= ArrayAccessCondition.forget_locs locs c}
| AllocSize _ ->
x
end end
module ConditionTrace = struct module ConditionTrace = struct
@ -395,12 +432,12 @@ module ConditionWithTrace = struct
cmp cmp
let subst (bound_map, trace_map) caller_pname callee_pname location cwt = let subst (bound_map, trace_map) rel_map caller_relation caller_pname callee_pname location cwt =
match Condition.get_symbols cwt.cond with match Condition.get_symbols cwt.cond with
| [] -> | [] ->
Some cwt Some cwt
| symbols -> | symbols ->
match Condition.subst bound_map cwt.cond with match Condition.subst bound_map rel_map caller_relation cwt.cond with
| None -> | None ->
None None
| Some cond -> | Some cond ->
@ -434,6 +471,9 @@ module ConditionWithTrace = struct
report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt) report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt)
|> Option.iter ~f:(report cwt.cond cwt.trace) ; |> Option.iter ~f:(report cwt.cond cwt.trace) ;
propagate propagate
let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
end end
module ConditionSet = struct module ConditionSet = struct
@ -495,9 +535,10 @@ module ConditionSet = struct
join [cwt] condset join [cwt] condset
let add_array_access pname location ~idx ~size ~is_arraylist_add val_traces condset = let add_array_access pname location ~idx ~size ~is_arraylist_add ~idx_sym_exp ~size_sym_exp
ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access ~is_arraylist_add ~relation val_traces condset =
|> add_opt pname location val_traces condset ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation
|> Condition.make_array_access ~is_arraylist_add |> add_opt pname location val_traces condset
let add_alloc_size pname location ~length val_traces condset = let add_alloc_size pname location ~length val_traces condset =
@ -505,10 +546,12 @@ module ConditionSet = struct
|> add_opt pname location val_traces condset |> add_opt pname location val_traces condset
let subst condset bound_map_trace_map caller_pname callee_pname location = let subst condset bound_map_trace_map rel_subst_map caller_relation caller_pname callee_pname
location =
let subst_add_cwt condset cwt = let subst_add_cwt condset cwt =
match match
ConditionWithTrace.subst bound_map_trace_map caller_pname callee_pname location cwt ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation caller_pname
callee_pname location cwt
with with
| None -> | None ->
condset condset
@ -532,12 +575,14 @@ module ConditionSet = struct
let pp : Format.formatter -> t -> unit = let pp : Format.formatter -> t -> unit =
fun fmt condset -> fun fmt condset ->
let pp_sep fmt () = F.fprintf fmt ", @," in let pp_sep fmt () = F.fprintf fmt ",@," in
F.fprintf fmt "@[<v 2>Safety conditions :@," ; F.fprintf fmt "Safety conditions:@;@[<hov 2>{ %a }@]"
F.fprintf fmt "@[<hov 1>{" ; (F.pp_print_list ~pp_sep ConditionWithTrace.pp)
F.pp_print_list ~pp_sep ConditionWithTrace.pp fmt condset ; condset
F.fprintf fmt " }@]" ;
F.fprintf fmt "@]"
let forget_locs : AbsLoc.PowLoc.t -> t -> t =
fun locs x -> List.map x ~f:(ConditionWithTrace.forget_locs locs)
end end
let description cond trace = let description cond trace =

@ -314,7 +314,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
Val.bot Val.bot
let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string = let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> Allocsite.t =
fun proc_name ~node_hash ~inst_num ~dimension -> fun proc_name ~node_hash ~inst_num ~dimension ->
let proc_name = Typ.Procname.to_string proc_name in let proc_name = Typ.Procname.to_string proc_name in
let node_num = string_of_int node_hash in let node_num = string_of_int node_hash in
@ -324,15 +324,19 @@ let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension
let eval_array_alloc let eval_array_alloc
: Typ.Procname.t -> node_hash:int -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t : Allocsite.t -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t =
-> inst_num:int -> dimension:int -> Val.t = fun allocsite typ ~stride ~offset ~size ->
fun pdesc ~node_hash typ ~stride ~offset ~size ~inst_num ~dimension ->
let allocsite = get_allocsite pdesc ~node_hash ~inst_num ~dimension in
let int_stride = match stride with None -> sizeof typ | Some stride -> stride in let int_stride = match stride with None -> sizeof typ | Some stride -> stride in
let stride = Itv.of_int int_stride in let stride = Itv.of_int int_stride in
ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk ~allocsite
let get_sym_f mem e = Val.get_sym (eval e mem)
let get_offset_sym_f mem e = Val.get_offset_sym (eval e mem)
let get_size_sym_f mem e = Val.get_size_sym (eval e mem)
module Prune = struct module Prune = struct
type astate = {prune_pairs: PrunePairs.t; mem: Mem.astate} type astate = {prune_pairs: PrunePairs.t; mem: Mem.astate}
@ -423,12 +427,16 @@ module Prune = struct
let is_unreachable_constant : Exp.t -> Mem.astate -> bool = let is_unreachable_constant : Exp.t -> Mem.astate -> bool =
fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0) fun e m ->
let v = eval e m in
Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) && PowLoc.is_bot (Val.get_pow_loc v)
&& ArrayBlk.is_bot (Val.get_array_blk v)
let prune_unreachable : Exp.t -> astate -> astate = let prune_unreachable : Exp.t -> astate -> astate =
fun e ({mem} as astate) -> fun e ({mem} as astate) ->
if is_unreachable_constant e mem then {astate with mem= Mem.bot} else astate if is_unreachable_constant e mem || Mem.is_relation_unsat mem then {astate with mem= Mem.bot}
else astate
let rec prune_helper e astate = let rec prune_helper e astate =
@ -461,6 +469,10 @@ module Prune = struct
let prune : Exp.t -> Mem.astate -> Mem.astate = let prune : Exp.t -> Mem.astate -> Mem.astate =
fun e mem -> fun e mem ->
let mem = Mem.apply_latest_prune e mem in let mem = Mem.apply_latest_prune e mem in
let mem =
let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f mem) in
Mem.meet_constraints constrs mem
in
let {mem; prune_pairs} = prune_helper e {mem; prune_pairs= PrunePairs.empty} in let {mem; prune_pairs} = prune_helper e {mem; prune_pairs= PrunePairs.empty} in
Mem.set_prune_pairs prune_pairs mem Mem.set_prune_pairs prune_pairs mem
end end
@ -472,13 +484,17 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
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 -> Exp.t option -> Typ.t -> Mem.astate -> Mem.astate
-> callee_ret_alias:AliasTarget.t option -> callee_ret_alias:AliasTarget.t option
-> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option = -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> * AliasTarget.t option
* (Relation.Var.t * Relation.SymExp.t option) list =
fun tenv formal actual actual_exp_opt 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
let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
let get_offset_sym v = Val.get_offset_sym v in
let get_size_sym v = Val.get_size_sym v in
let get_field_name (fn, _, _) = fn in let get_field_name (fn, _, _) = fn in
let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in
let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in
@ -506,17 +522,38 @@ let get_matching_pairs
else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: 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_sym_main_value v1 v2 ~e2_opt l =
Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var ->
let sym_exp_opt =
Option.first_some
(Relation.SymExp.of_exp_opt ~get_sym_f:(get_sym_f caller_mem) e2_opt)
(Relation.SymExp.of_sym (Val.get_sym v2))
in
(var, sym_exp_opt) :: l )
in
let add_pair_sym s1 s2 l =
Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var ->
(var, Relation.SymExp.of_sym s2) :: l )
in
let add_pair_val v1 v2 ~e2_opt (bound_pairs, rel_pairs) =
add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) let bound_pairs =
|> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) bound_pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2)
|> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2)
|> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2)
in
let rel_pairs =
rel_pairs |> add_pair_sym_main_value v1 v2 ~e2_opt
|> add_pair_sym (get_offset_sym v1) (get_offset_sym v2)
|> add_pair_sym (get_size_sym v1) (get_size_sym v2)
in
(bound_pairs, rel_pairs)
in in
let add_pair_field v1 v2 pairs fn = let add_pair_field v1 v2 pairs fn =
add_ret_alias (append_field v1 fn) (append_field v2 fn) ; add_ret_alias (append_field v1 fn) (append_field v2 fn) ;
let v1' = deref_field v1 fn callee_mem in let v1' = deref_field v1 fn callee_mem in
let v2' = deref_field v2 fn caller_mem in let v2' = deref_field v2 fn caller_mem in
add_pair_val v1' v2' pairs add_pair_val v1' v2' ~e2_opt:None pairs
in in
let add_pair_ptr typ v1 v2 pairs = let add_pair_ptr typ v1 v2 pairs =
add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
@ -531,15 +568,17 @@ let get_matching_pairs
| Typ.Tptr (_, _) -> | Typ.Tptr (_, _) ->
let v1' = deref_ptr v1 callee_mem in let v1' = deref_ptr v1 callee_mem in
let v2' = deref_ptr v2 caller_mem in let v2' = deref_ptr v2 caller_mem in
add_pair_val v1' v2' pairs add_pair_val v1' v2' ~e2_opt:None pairs
| _ -> | _ ->
pairs pairs
in in
let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in let bound_pairs, rel_pairs =
(pairs, !ret_alias) ([], []) |> add_pair_val formal actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ formal actual
in
(bound_pairs, !ret_alias, rel_pairs)
let subst_map_of_pairs let subst_map_of_bound_pairs
: (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
-> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t = -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t =
fun pairs -> fun pairs ->
@ -552,8 +591,16 @@ let subst_map_of_pairs
List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs
let subst_map_of_rel_pairs
: (Relation.Var.t * Relation.SymExp.t option) list -> Relation.SubstMap.t =
fun pairs ->
let add_pair rel_map (x, e) = Relation.SubstMap.add x e rel_map in
List.fold pairs ~init:Relation.SubstMap.empty ~f:add_pair
let rec list_fold2_def let rec list_fold2_def
: default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b = : default:Val.t * Exp.t option -> f:('a -> Val.t * Exp.t option -> 'b -> 'b) -> 'a list
-> (Val.t * Exp.t option) list -> init:'b -> 'b =
fun ~default ~f xs ys ~init:acc -> fun ~default ~f xs ys ~init:acc ->
match (xs, ys) with match (xs, ys) with
| [], _ -> | [], _ ->
@ -561,7 +608,9 @@ let rec list_fold2_def
| x :: xs', [] -> | x :: xs', [] ->
list_fold2_def ~default ~f xs' ys ~init:(f x default acc) list_fold2_def ~default ~f xs' ys ~init:(f x default acc)
| [x], _ :: _ -> | [x], _ :: _ ->
f x (List.fold ~f:Val.join ~init:Val.bot ys) acc let v = List.fold ys ~init:Val.bot ~f:(fun acc (y, _) -> Val.join y acc) in
let exp_opt = match ys with [(_, exp_opt)] -> exp_opt | _ -> None in
f x (v, exp_opt) acc
| x :: xs', y :: ys' -> | x :: xs', y :: ys' ->
list_fold2_def ~default ~f xs' ys' ~init:(f x y acc) list_fold2_def ~default ~f xs' ys' ~init:(f x y acc)
@ -570,18 +619,22 @@ 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:AliasTarget.t option -> callee_ret_alias:AliasTarget.t option
-> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t) -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t)
* AliasTarget.t option = * AliasTarget.t option
* Relation.SubstMap.t =
fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias ->
let add_pair (formal, typ) actual (l, ret_alias) = let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) =
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
let new_matching, ret_alias' = let new_bound_matching, ret_alias', new_rel_matching =
get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias get_matching_pairs tenv formal actual actual_exp typ caller_mem callee_entry_mem
~callee_ret_alias
in in
(List.rev_append new_matching l, Option.first_some ret_alias ret_alias') ( List.rev_append new_bound_matching bound_l
, Option.first_some ret_alias ret_alias'
, List.rev_append new_rel_matching rel_l )
in in
let formals = get_formals callee_pdesc in let formals = get_formals callee_pdesc in
let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in
let pairs, ret_alias = let bound_pairs, ret_alias, rel_pairs =
list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None) list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:([], None, [])
in in
(subst_map_of_pairs pairs, ret_alias) (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs)

@ -10,6 +10,7 @@ open AbsLoc
open! AbstractDomain.Types open! AbstractDomain.Types
module L = Logging module L = Logging
module Dom = BufferOverrunDomain module Dom = BufferOverrunDomain
module Relation = BufferOverrunDomainRelation
module PO = BufferOverrunProofObligations module PO = BufferOverrunProofObligations
module Sem = BufferOverrunSemantics module Sem = BufferOverrunSemantics
module Trace = BufferOverrunTrace module Trace = BufferOverrunTrace
@ -38,15 +39,18 @@ module Exec = struct
-> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate
-> Dom.Mem.astate * int = -> Dom.Mem.astate * int =
fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem -> fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem ->
let offset = Itv.zero in
let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
let arr = let arr =
Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num ~dimension Sem.eval_array_alloc allocsite typ ~stride ~offset ~size
|> Dom.Val.add_trace_elem (Trace.ArrDecl location) |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
in in
let mem = let mem =
if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem
in in
let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in let mem = Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None mem in
let loc = Loc.of_allocsite allocsite in
let mem, _ = let mem, _ =
decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem
in in
@ -92,12 +96,14 @@ module Exec = struct
in in
let alloc_num = Itv.Counter.next new_alloc_num in let alloc_num = Itv.Counter.next new_alloc_num in
let elem = Trace.SymAssign (loc, location) in let elem = Trace.SymAssign (loc, location) in
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in
let arr = let arr =
Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num Sem.eval_array_alloc allocsite typ ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem
~dimension:alloc_num in
|> Dom.Val.add_trace_elem elem let mem =
mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc
|> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
in in
let mem = Dom.Mem.add_heap loc arr mem in
let deref_loc = let deref_loc =
Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num) Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num)
in in
@ -145,11 +151,11 @@ module Exec = struct
Itv.plus i length ) Itv.plus i length )
in in
let stride = Option.map stride ~f:IntLit.to_int_exn in let stride = Option.map stride ~f:IntLit.to_int_exn in
let v = let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size:length let offset, size = (Itv.zero, length) in
~inst_num ~dimension let v = Sem.eval_array_alloc allocsite typ ~stride ~offset ~size in
in mem |> Dom.Mem.strong_update_heap field_loc v
Dom.Mem.strong_update_heap field_loc v mem |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
| _ -> | _ ->
init_fields field_typ field_loc dimension ?dyn_length mem init_fields field_typ field_loc dimension ?dyn_length mem
in in
@ -191,27 +197,36 @@ module Exec = struct
end end
module Check = struct module Check = struct
let check_access ~size ~idx ~arr ~idx_traces ?(is_arraylist_add= false) pname location cond_set = let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces
?(is_arraylist_add= false) pname location cond_set =
let arr_traces = Dom.Val.get_traces arr in let arr_traces = Dom.Val.get_traces arr in
match (size, idx) with match (size, idx) with
| NonBottom length, NonBottom idx -> | NonBottom length, NonBottom idx ->
let traces = TraceSet.merge ~arr_traces ~idx_traces location in let traces = TraceSet.merge ~arr_traces ~idx_traces location in
PO.ConditionSet.add_array_access pname location ~size:length ~idx ~is_arraylist_add traces PO.ConditionSet.add_array_access pname location ~size:length ~idx ~size_sym_exp
cond_set ~idx_sym_exp ~relation ~is_arraylist_add traces cond_set
| _ -> | _ ->
cond_set cond_set
let array_access ~arr ~idx ~is_plus pname location cond_set = let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set =
let arr_blk = Dom.Val.get_array_blk arr in let arr_blk = Dom.Val.get_array_blk arr in
let size = ArrayBlk.sizeof arr_blk in let size = ArrayBlk.sizeof arr_blk in
let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
let offset = ArrayBlk.offsetof arr_blk in let offset = ArrayBlk.offsetof arr_blk in
let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in
let idx_itv = Dom.Val.get_itv idx in let idx_itv = Dom.Val.get_itv idx in
let idx_traces = Dom.Val.get_traces idx in let idx_traces = Dom.Val.get_traces idx in
let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in
let idx_sym_exp =
Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp ->
let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in
op idx_sym_exp offset_sym_exp )
in
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
"@[<v 2>Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; "@[<v 2>Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ;
check_access ~size ~idx:idx_in_blk ~arr ~idx_traces pname location cond_set check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces pname
location cond_set
let arraylist_access ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set = let arraylist_access ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set =
@ -220,11 +235,15 @@ module Check = struct
let idx_traces = Dom.Val.get_traces idx in let idx_traces = Dom.Val.get_traces idx in
let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in
let idx = Dom.Val.get_itv idx in let idx = Dom.Val.get_itv idx in
check_access ~size ~idx ~arr ~idx_traces ~is_arraylist_add pname location cond_set let relation = Dom.Mem.get_relation mem in
check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
~is_arraylist_add pname location cond_set
let lindex ~array_exp ~index_exp mem pname location cond_set = let lindex ~array_exp ~index_exp mem pname location cond_set =
let idx = Sem.eval index_exp mem in let idx = Sem.eval index_exp mem in
let arr = Sem.eval_arr array_exp mem in let arr = Sem.eval_arr array_exp mem in
array_access ~arr ~idx ~is_plus:true pname location cond_set let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in
let relation = Dom.Mem.get_relation mem in
array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location cond_set
end end

@ -8,6 +8,7 @@
open! IStd open! IStd
open AbsLoc open AbsLoc
module Dom = BufferOverrunDomain module Dom = BufferOverrunDomain
module Relation = BufferOverrunDomainRelation
module PO = BufferOverrunProofObligations module PO = BufferOverrunProofObligations
module Exec : sig module Exec : sig
@ -56,7 +57,8 @@ end
module Check : sig module Check : sig
val array_access : val array_access :
arr:Dom.Val.t -> idx:Dom.Val.t -> is_plus:bool -> Typ.Procname.t -> Location.t arr:Dom.Val.t -> idx:Dom.Val.t -> idx_sym_exp:Relation.SymExp.t option
-> relation:Relation.astate -> is_plus:bool -> Typ.Procname.t -> Location.t
-> PO.ConditionSet.t -> PO.ConditionSet.t -> PO.ConditionSet.t -> PO.ConditionSet.t
val lindex : val lindex :

@ -35,6 +35,8 @@ module Boolean = struct
let top = Top let top = Top
let true_ = True
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
let is_false = function False -> true | _ -> false let is_false = function False -> true | _ -> false

@ -22,6 +22,8 @@ module Boolean : sig
val top : t val top : t
val true_ : t
val equal : t -> t -> bool val equal : t -> t -> bool
val is_false : t -> bool val is_false : t -> bool

@ -61,7 +61,7 @@ module TransferFunctionsNodesBasicCost = struct
let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in
let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in
let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in
let (subst_map, _), _ = let (subst_map, _), _, _ =
BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem
callee_entry_mem ~callee_ret_alias callee_entry_mem ~callee_ret_alias
in in

@ -55,11 +55,14 @@ let common_optflags = match build_mode with Opt -> ["-O3"] | Default | Test -> [
let common_libraries = let common_libraries =
(if java then ["javalib"; "ptrees"; "sawja"] else []) (if java then ["javalib"; "ptrees"; "sawja"] else [])
@ [ "ANSITerminal" @ [ "ANSITerminal"
; "apron"
; "apron.octMPQ"
; "atdgen" ; "atdgen"
; "base" ; "base"
; "base64" ; "base64"
; "cmdliner" ; "cmdliner"
; "core" ; "core"
; "elina"
; "extlib" ; "extlib"
; "mtime.clock.os" ; "mtime.clock.os"
; "oUnit" ; "oUnit"

@ -86,6 +86,10 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDI
codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]]
codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]]
codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]]
codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [-1, -1] Size: [1, 1] by call to `array_access_Ok()` ]
codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]

@ -0,0 +1,43 @@
/*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
void array_access_Ok(int x, int y) {
int a[1];
if (x + y == 1) {
a[x + y - 1] = 0;
}
}
void FP_call_array_access_Ok() { array_access_Ok(0, 0); }
void FP_array_access2_Ok(int x, int y) {
int a[1];
if (x + y == 1) {
if (x + y != 1) {
a[3] = 0;
}
}
}
void FP_array_access3_Ok(int x, int* y) {
int a[1];
*y = x + 1;
if (x + 1 == 1) {
if (*y != 1) {
a[3] = 0;
}
}
}
void FP_array_access4_Ok(int x, int* y) {
int a[1];
*y = x * 3 + 1;
if (x * 3 + 1 == 1) {
if (*y != 1) {
a[3] = 0;
}
}
}

@ -27,15 +27,19 @@ remove: [
ocaml-version: [ >= "4.04.2" ] ocaml-version: [ >= "4.04.2" ]
depends: [ depends: [
"ANSITerminal" {>="0.7"} "ANSITerminal" {>="0.7"}
"apron"
"atdgen" {>="1.6.0"} "atdgen" {>="1.6.0"}
"base64" "base64"
"cmdliner" {>="1.0.0"} "cmdliner" {>="1.0.0"}
"core" "core"
"conf-autoconf" {build} "conf-autoconf" {build}
"conf-gmp" {build}
"conf-mpfr" {build}
"conf-sqlite3" {build} "conf-sqlite3" {build}
"conf-zlib" {build} "conf-zlib" {build}
"ctypes" {>="0.9.2"} "ctypes" {>="0.9.2"}
"dune" {build & >="1.0"} "dune" {build & >="1.0"}
"elina" {>="1.1"}
"extlib-compat" "extlib-compat"
"javalib" {>="2.3.4"} "javalib" {>="2.3.4"}
"mtime" "mtime"

@ -1,16 +1,21 @@
ANSITerminal = 0.8 ANSITerminal = 0.8
apron = 20160125
atd = 1.12.0 atd = 1.12.0
atdgen = 1.12.0 atdgen = 1.12.0
base = v0.11.0 base = v0.11.0
base64 = 2.2.0 base64 = 2.2.0
bin_prot = v0.11.0 bin_prot = v0.11.0
biniou = 1.2.0 biniou = 1.2.0
camlidl = 1.05
camlp4 = 4.06+1 camlp4 = 4.06+1
camlzip = 1.07 camlzip = 1.07
cmdliner = 1.0.2 cmdliner = 1.0.2
conf-aclocal = 1.0.0 conf-aclocal = 1.0.0
conf-autoconf = 0.1 conf-autoconf = 0.1
conf-gmp = 1
conf-m4 = 1 conf-m4 = 1
conf-mpfr = 1
conf-perl = 1
conf-pkg-config = 1.0 conf-pkg-config = 1.0
conf-sqlite3 = 1 conf-sqlite3 = 1
conf-which = 1 conf-which = 1
@ -23,6 +28,7 @@ cppo_ocamlbuild = 1.6.0
ctypes = 0.14.0 ctypes = 0.14.0
dune = 1.0.0 dune = 1.0.0
easy-format = 1.3.1 easy-format = 1.3.1
elina = 1.1
extlib-compat = 1.7.2 extlib-compat = 1.7.2
fieldslib = v0.11.0 fieldslib = v0.11.0
integers = 0.2.2 integers = 0.2.2
@ -30,6 +36,7 @@ jane-street-headers = v0.11.0
javalib = 2.3.4 javalib = 2.3.4
jbuilder = transition jbuilder = transition
menhir = 20171222 menhir = 20171222
mlgmpidl = 1.2.6-1
mtime = 1.1.0 mtime = 1.1.0
num = 1.1 num = 1.1
ocaml-compiler-libs = v0.11.0 ocaml-compiler-libs = v0.11.0

Loading…
Cancel
Save