[Inferbo] Add relational domain

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, so this diff should not make any differences in CI.

Use `--bo-relational-domain {oct, poly}` 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: mbouaziz, jvillard

Differential Revision: D8478542

fbshipit-source-id: 510ff53

Makefile.autoconf.in

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

configure.ac

@@ -192,6 +192,8 @@ AC_ASSERT_OCAML_PKG([oUnit], [], [2.0.0])
 AC_CHECK_TOOL([UTOP], [utop], [no])
 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],
   [Additional directories to search for dynamically-loaded libraries.])
 AC_ARG_VAR([OPAMROOT], [Root of the local opam installation.])

infer/src/absint/AbstractInterpreter.ml

@@ -93,7 +93,7 @@ struct
         in
         if debug then (
           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 Domain.pp astate_post) ;
           NodePrinter.finish_session (Node.underlying_node node) ) ;

infer/src/base/Config.ml

@@ -823,6 +823,13 @@ and blacklist =
     ~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 =
   CLOpt.mk_string_opt ~long:"bootclasspath"
     ~in_help:InferCommand.[(Capture, manual_java)]
@@ -2445,6 +2452,8 @@ and bootclasspath = !bootclasspath
 
 and bo_debug = !bo_debug
 
+and bo_relational_domain = !bo_relational_domain
+
 and buck = !buck
 
 and buck_build_args = !buck_build_args

infer/src/base/Config.mli

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

infer/src/bufferoverrun/absLoc.ml

@@ -42,6 +42,8 @@ module Loc = struct
         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 rec contains_allocsite = function
@@ -89,3 +91,12 @@ module PowLoc = struct
 
   let is_singleton x = Int.equal (cardinal x) 1
 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

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -13,6 +13,7 @@ open AbsLoc
 open! AbstractDomain.Types
 module BoUtils = BufferOverrunUtils
 module Dom = BufferOverrunDomain
+module Relation = BufferOverrunDomainRelation
 module L = Logging
 module Models = BufferOverrunModels
 module Sem = BufferOverrunSemantics
@@ -47,16 +48,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         | Typ.Tint ikind ->
             let unsigned = Typ.ikind_is_unsigned ikind in
             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))
             in
-            Dom.Mem.add_heap loc v mem
+            mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tfloat _ ->
             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))
             in
-            Dom.Mem.add_heap loc v mem
+            mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tptr (typ, _) ->
             BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv
               ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
@@ -182,6 +183,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     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
       : 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 =
@@ -191,12 +198,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in
     match callee_pdesc with
     | 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
         in
-        instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map caller_mem
-          ret_alias location
-        |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location
+        let caller_mem =
+          instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem bound_subst_map
+            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 ->
         caller_mem
 
@@ -224,6 +236,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | Store (exp1, _, exp2, location) ->
           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 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 =
             if PowLoc.is_singleton locs then
@@ -364,7 +384,9 @@ module Report = struct
    fun pname ~is_plus ~e1 ~e2 location mem cond_set ->
     let arr = Sem.eval e1 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
@@ -403,7 +425,10 @@ module Report = struct
     match exp with
     | Exp.Var _ ->
         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) ->
         check_binop pname ~bop ~e1 ~e2 location mem cond_set
     | _ ->
@@ -418,11 +443,13 @@ module Report = struct
     let callee_cond = Dom.Summary.get_cond_set summary in
     match callee_pdesc with
     | 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
         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
 
@@ -558,6 +585,9 @@ module Report = struct
         Reporting.log_error summary ~loc:location ~ltr:trace exn
     in
     PO.ConditionSet.check_all ~report cond_set
+
+
+  let forget_locs = PO.ConditionSet.forget_locs
 end
 
 let extract_pre = Analyzer.extract_pre
@@ -570,16 +600,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
 
 
+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 =
  fun {proc_desc; tenv; summary} ->
   Preanal.do_preanalysis proc_desc tenv ;
   let pdata = ProcData.make_default proc_desc tenv in
   let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata 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 exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map in
+  let locals = get_local_decls cfg 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 =
     Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc
+    |> Report.forget_locs locals
   in
   let summary =
     match (entry_mem, exit_mem) with

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -13,31 +13,54 @@ open AbsLoc
 open! AbstractDomain.Types
 module F = Format
 module L = Logging
+module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
-(** unsound but ok for bug catching *)
-let always_strong_update = true
-
 module Val = struct
   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
 
-  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 =
-    if Config.bo_debug <= 1 then
-      F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk
-    else
-      F.fprintf fmt "(%a, %a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk
-        TraceSet.pp x.traces
+    let relation_sym_pp fmt sym =
+      if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym
+    in
+    let trace_pp fmt 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 =
-   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 =
@@ -51,8 +74,11 @@ module Val = struct
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     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
+      && 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)
@@ -61,8 +87,11 @@ module Val = struct
     if phys_equal prev next then prev
     else
       { 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
       ; 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 }
 
 
@@ -71,13 +100,20 @@ module Val = struct
     if phys_equal x y then x
     else
       { itv= Itv.join x.itv y.itv
+      ; sym= Relation.Sym.join x.sym y.sym
       ; powloc= PowLoc.join x.powloc y.powloc
       ; 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 }
 
 
   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_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_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 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_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 make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t =
-   fun ?(unsigned= false) pname path new_sym_num ->
-    {bot with itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num}
+  let make_sym
+      : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t =
+   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 =
    fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces}
@@ -295,6 +344,15 @@ module Heap = struct
    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 =
    fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem
 
@@ -396,10 +454,9 @@ module AliasMap = struct
     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
     (* 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.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
@@ -506,7 +563,7 @@ module Alias = struct
 
   let pp : F.formatter -> astate -> unit =
    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
 
 module PrunePairs = struct
@@ -593,11 +650,21 @@ end
 
 module MemReach = struct
   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
 
-  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 =
     if phys_equal lhs rhs then true
@@ -605,6 +672,7 @@ module MemReach = struct
       Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap
       && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias
       && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune
+      && Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation
 
 
   let widen ~prev ~next ~num_iters =
@@ -614,7 +682,7 @@ module MemReach = struct
       ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~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
-      }
+      ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters }
 
 
   let join : t -> t -> t =
@@ -622,12 +690,15 @@ module MemReach = struct
     { stack= Stack.join x.stack y.stack
     ; heap= Heap.join x.heap y.heap
     ; 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 =
    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 =
@@ -689,13 +760,6 @@ module MemReach = struct
 
   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 =
    fun ploc v s ->
     if can_strong_update ploc then strong_update_heap ploc v s
@@ -768,6 +832,41 @@ module MemReach = struct
 
   let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate =
    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
 
 module Mem = struct
@@ -894,6 +993,42 @@ module Mem = struct
 
   let update_latest_prune : Exp.t -> Exp.t -> t -> t =
    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
 
 module Summary = struct
@@ -921,5 +1056,5 @@ module Summary = struct
 
   let pp : F.formatter -> t -> unit =
    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

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -13,6 +13,7 @@ module BoUtils = BufferOverrunUtils
 module Dom = BufferOverrunDomain
 module PO = BufferOverrunProofObligations
 module Sem = BufferOverrunSemantics
+module Relation = BufferOverrunDomainRelation
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
@@ -82,12 +83,17 @@ let malloc size_exp =
     let typ, stride, length0, dyn_length = get_malloc_info size_exp in
     let length = Sem.eval length0 mem 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 =
-      Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero
-        ~size:(Dom.Val.get_itv length) ~inst_num:0 ~dimension:1
-      |> Dom.Val.set_traces traces
+      Sem.eval_array_alloc allocsite typ ~stride ~offset ~size |> Dom.Val.set_traces traces
     in
     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)
     |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v)
          ?dyn_length
@@ -178,10 +184,8 @@ let set_array_length array length_exp =
     | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
         let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
         let stride = Option.map ~f:IntLit.to_int stride in
-        let v =
-          Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length
-            ~inst_num:0 ~dimension:1
-        in
+        let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in
+        let v = Sem.eval_array_alloc allocsite elt ~stride ~offset:Itv.zero ~size:length in
         mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
         |> set_uninitialized location elt (Dom.Val.get_array_locs v)
     | _ ->

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -10,6 +10,7 @@ open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module ItvPure = Itv.ItvPure
+module Relation = BufferOverrunDomainRelation
 module MF = MarkupFormatter
 module ValTraceSet = BufferOverrunTrace.Set
 
@@ -93,7 +94,13 @@ module AllocSizeCondition = struct
 end
 
 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
 
@@ -106,7 +113,10 @@ module ArrayAccessCondition = struct
   let pp : F.formatter -> t -> unit =
    fun fmt c ->
     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 =
@@ -115,9 +125,12 @@ module ArrayAccessCondition = struct
     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 =
-   fun ~idx ~size ->
-    if ItvPure.is_invalid idx || ItvPure.is_invalid size then None else Some {idx; size}
+  let make
+      : idx:ItvPure.t -> size:ItvPure.t -> idx_sym_exp:Relation.SymExp.t option
+        -> 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} =
@@ -206,8 +219,15 @@ module ArrayAccessCondition = struct
     (* 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 not_overrun = ItvPure.lt_sem c'.idx c'.size in
-    let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in
+    let not_overrun =
+      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
     (* il >= 0 and iu < sl, definitely not an error *)
     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 *)
@@ -235,13 +255,22 @@ module ArrayAccessCondition = struct
       {report_issue_type; propagate= is_symbolic}
 
 
-  let subst : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t -> t option =
-   fun bound_map c ->
+  let subst
+      : 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
     | 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
+
+
+  let forget_locs : AbsLoc.PowLoc.t -> t -> t =
+   fun locs c -> {c with relation= Relation.forget_locs locs c.relation}
 end
 
 module Condition = struct
@@ -258,11 +287,11 @@ module Condition = struct
         ArrayAccessCondition.get_symbols c
 
 
-  let subst bound_map = function
+  let subst bound_map rel_map caller_relation = function
     | AllocSize c ->
         AllocSizeCondition.subst bound_map c |> make_alloc_size
     | ArrayAccess c ->
-        ArrayAccessCondition.subst bound_map c |> make_array_access
+        ArrayAccessCondition.subst bound_map rel_map caller_relation c |> make_array_access
 
 
   let have_similar_bounds c1 c2 =
@@ -306,6 +335,14 @@ module Condition = struct
         AllocSizeCondition.check c
     | ArrayAccess c ->
         ArrayAccessCondition.check c
+
+
+  let forget_locs locs x =
+    match x with
+    | ArrayAccess c ->
+        ArrayAccess (ArrayAccessCondition.forget_locs locs c)
+    | AllocSize _ ->
+        x
 end
 
 module ConditionTrace = struct
@@ -386,12 +423,12 @@ module ConditionWithTrace = struct
         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
     | [] ->
         Some cwt
     | symbols ->
-      match Condition.subst bound_map cwt.cond with
+      match Condition.subst bound_map rel_map caller_relation cwt.cond with
       | None ->
           None
       | Some cond ->
@@ -425,6 +462,9 @@ module ConditionWithTrace = struct
     report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt)
     |> Option.iter ~f:(report cwt.cond cwt.trace) ;
     propagate
+
+
+  let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
 end
 
 module ConditionSet = struct
@@ -486,9 +526,10 @@ module ConditionSet = struct
         join [cwt] condset
 
 
-  let add_array_access pname location ~idx ~size val_traces condset =
-    ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access
-    |> add_opt pname location val_traces condset
+  let add_array_access pname location ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation val_traces
+      condset =
+    ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation
+    |> Condition.make_array_access |> add_opt pname location val_traces condset
 
 
   let add_alloc_size pname location ~length val_traces condset =
@@ -496,10 +537,12 @@ module ConditionSet = struct
     |> 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 =
       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
       | None ->
           condset
@@ -524,11 +567,13 @@ module ConditionSet = struct
   let pp : Format.formatter -> t -> unit =
    fun fmt condset ->
     let pp_sep fmt () = F.fprintf fmt ",@," in
-    F.fprintf fmt "@[<v 2>Safety conditions :@," ;
-    F.fprintf fmt "@[<hov 1>{" ;
-    F.pp_print_list ~pp_sep ConditionWithTrace.pp fmt condset ;
-    F.fprintf fmt " }@]" ;
-    F.fprintf fmt "@]"
+    F.fprintf fmt "Safety conditions:@;@[<hov 2>{ %a }@]"
+      (F.pp_print_list ~pp_sep ConditionWithTrace.pp)
+      condset
+
+
+  let forget_locs : AbsLoc.PowLoc.t -> t -> t =
+   fun locs x -> List.map x ~f:(ConditionWithTrace.forget_locs locs)
 end
 
 let description cond trace =

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -314,7 +314,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
       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 ->
   let proc_name = Typ.Procname.to_string proc_name 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
-    : Typ.Procname.t -> node_hash:int -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t
-      -> inst_num:int -> dimension:int -> Val.t =
- fun pdesc ~node_hash typ ~stride ~offset ~size ~inst_num ~dimension ->
-  let allocsite = get_allocsite pdesc ~node_hash ~inst_num ~dimension in
+    : Allocsite.t -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t =
+ fun allocsite typ ~stride ~offset ~size ->
   let int_stride = match stride with None -> sizeof typ | Some stride -> 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
   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 =
-   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 =
    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 =
@@ -461,6 +469,10 @@ module Prune = struct
   let prune : Exp.t -> Mem.astate -> Mem.astate =
    fun e mem ->
     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
     Mem.set_prune_pairs prune_pairs mem
 end
@@ -472,13 +484,17 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
 
 
 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
-      -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option =
- fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias ->
+      -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
+         * 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_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof 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 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
@@ -506,17 +522,38 @@ let get_matching_pairs
       else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l
     else l
   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) ;
-    pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2)
+    let bound_pairs =
+      bound_pairs |> add_pair_itv (get_itv v1) (get_itv 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
   let add_pair_field v1 v2 pairs fn =
     add_ret_alias (append_field v1 fn) (append_field v2 fn) ;
     let v1' = deref_field v1 fn callee_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
   let add_pair_ptr typ v1 v2 pairs =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
@@ -531,15 +568,17 @@ let get_matching_pairs
     | Typ.Tptr (_, _) ->
         let v1' = deref_ptr v1 callee_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
   in
-  let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in
-  (pairs, !ret_alias)
+  let bound_pairs, rel_pairs =
+    ([], []) |> 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 bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t =
  fun pairs ->
@@ -552,8 +591,16 @@ let subst_map_of_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
-    : 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 ->
   match (xs, ys) with
   | [], _ ->
@@ -561,7 +608,9 @@ let rec list_fold2_def
   | x :: xs', [] ->
       list_fold2_def ~default ~f xs' ys ~init:(f x default acc)
   | [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' ->
       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
       -> callee_ret_alias:AliasTarget.t option
       -> (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 ->
-  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 new_matching, ret_alias' =
-      get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias
+    let new_bound_matching, ret_alias', new_rel_matching =
+      get_matching_pairs tenv formal actual actual_exp typ caller_mem callee_entry_mem
+        ~callee_ret_alias
     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
   let formals = get_formals callee_pdesc in
-  let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in
-  let pairs, ret_alias =
-    list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None)
+  let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in
+  let bound_pairs, ret_alias, rel_pairs =
+    list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:([], None, [])
   in
-  (subst_map_of_pairs pairs, ret_alias)
+  (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs)

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -10,6 +10,7 @@ open AbsLoc
 open! AbstractDomain.Types
 module L = Logging
 module Dom = BufferOverrunDomain
+module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
@@ -33,15 +34,18 @@ module Exec = struct
         -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate
         -> Dom.Mem.astate * int =
    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 allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
     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)
     in
     let mem =
       if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem
     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, _ =
       decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem
     in
@@ -69,12 +73,14 @@ module Exec = struct
     in
     let alloc_num = Itv.Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
+    let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in
     let arr =
-      Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num
-        ~dimension:alloc_num
-      |> Dom.Val.add_trace_elem elem
+      Sem.eval_array_alloc allocsite typ ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem
+    in
+    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
-    let mem = Dom.Mem.add_heap loc arr mem in
     let deref_loc =
       Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num)
     in
@@ -95,11 +101,11 @@ module Exec = struct
                   Itv.plus i length )
             in
             let stride = Option.map stride ~f:IntLit.to_int in
-            let v =
-              Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size:length
-                ~inst_num ~dimension
-            in
-            Dom.Mem.strong_update_heap field_loc v mem
+            let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
+            let offset, size = (Itv.zero, length) in
+            let v = Sem.eval_array_alloc allocsite typ ~stride ~offset ~size in
+            mem |> Dom.Mem.strong_update_heap field_loc v
+            |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
         | _ ->
             init_fields field_typ field_loc dimension ?dyn_length mem
       in
@@ -141,14 +147,21 @@ module Exec = struct
 end
 
 module Check = struct
-  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_traces = Dom.Val.get_traces arr 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_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in
     let idx_itv = Dom.Val.get_itv 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_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) "@[<v 2>Add condition :@," ;
     L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr_blk ;
     L.(debug BufferOverrun Verbose) "  idx: %a@," Itv.pp idx_in_blk ;
@@ -156,7 +169,8 @@ module Check = struct
     match (size, idx_in_blk) with
     | NonBottom size, NonBottom idx ->
         let traces = TraceSet.merge ~arr_traces ~idx_traces location in
-        PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set
+        PO.ConditionSet.add_array_access pname location ~size ~idx ~size_sym_exp ~idx_sym_exp
+          ~relation traces cond_set
     | _ ->
         cond_set
 
@@ -164,5 +178,7 @@ module Check = struct
   let lindex ~array_exp ~index_exp mem pname location cond_set =
     let arr = Sem.eval_arr array_exp mem in
     let idx = Sem.eval index_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

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -8,6 +8,7 @@
 open! IStd
 open AbsLoc
 module Dom = BufferOverrunDomain
+module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 
 module Exec : sig
@@ -41,7 +42,8 @@ end
 
 module Check : sig
   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
 
   val lindex :

infer/src/bufferoverrun/itv.ml

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

infer/src/bufferoverrun/itv.mli

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

infer/src/checkers/cost.ml

@@ -61,7 +61,7 @@ module TransferFunctionsNodesBasicCost = struct
           let callee_entry_mem = BufferOverrunDomain.Summary.get_input 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 (subst_map, _), _ =
+          let (subst_map, _), _, _ =
             BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem
               callee_entry_mem ~callee_ret_alias
           in

infer/src/deadcode/jbuild.in

@@ -1,6 +1,8 @@
 (* -*- tuareg -*- *)
 (* NOTE: prepend jbuild.common to this file! *)
 
+let deadcode_cflags = common_cflags @ ["-cclib -lparmap_stubs"]
+
 ;; Format.sprintf
      {|
 (executable
@@ -12,7 +14,7 @@
   (preprocess (pps (ppx_compare ppx_sexp_conv -no-check)))
  ))
 |}
-     (String.concat " " common_cflags)
+     (String.concat " " deadcode_cflags)
      (String.concat " " common_optflags)
      (String.concat " " common_libraries)
    |> Jbuild_plugin.V1.send

infer/src/jbuild.common.in

@@ -55,6 +55,9 @@ let common_optflags = match build_mode with Opt -> ["-O3"] | Default | Test -> [
 let common_libraries =
   (if java then ["javalib"; "ptrees"; "sawja"] else [])
   @ [ "ANSITerminal"
+    ; "apron"
+    ; "apron.octMPQ"
+    ; "elina"
     ; "atdgen"
     ; "base"
     ; "base64"

infer/src/jbuild.in

@@ -38,7 +38,8 @@ let infer_cflags =
     ; "-open"
     ; "InferIR"
     ; "-open"
-    ; "InferBase" ]
+    ; "InferBase"
+    ; "-cclib -lparmap_stubs" ]
 
 
 (** The build stanzas to be passed to jbuilder *)

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -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_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/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, 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]]

infer/tests/codetoanalyze/c/bufferoverrun/relation.c

@@ -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;
+    }
+  }
+}

opam

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

opam.lock

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