Revert "[Inferbo] Add relational domain"

Summary: This reverts commit "[Inferbo] Add relational domain" due to linking issues.

Reviewed By: mbouaziz

Differential Revision: D8821355

fbshipit-source-id: b39bfa6

Makefile.autoconf.in

@@ -18,7 +18,6 @@ CFLAGS = @CFLAGS@
 CLANG_INCLUDES = @CLANG_INCLUDES@
 CLANG_PREFIX = @CLANG_PREFIX@
 CMAKE = @CMAKE@
-CPATH = @CPATH@
 CPP = @CPP@
 CXX = @CXX@
 CXXFLAGS = @CXXFLAGS@
@@ -43,7 +42,6 @@ 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@
@@ -81,7 +79,5 @@ 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,8 +192,6 @@ 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@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre
+            (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %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,13 +823,6 @@ 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)]
@@ -2452,8 +2445,6 @@ 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,8 +242,6 @@ 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,8 +42,6 @@ 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
@@ -91,12 +89,3 @@ 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,7 +13,6 @@ open AbsLoc
 open! AbstractDomain.Types
 module BoUtils = BufferOverrunUtils
 module Dom = BufferOverrunDomain
-module Relation = BufferOverrunDomainRelation
 module L = Logging
 module Models = BufferOverrunModels
 module Sem = BufferOverrunSemantics
@@ -48,16 +47,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 loc pname path new_sym_num
+              Dom.Val.make_sym ~unsigned pname path new_sym_num
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
-            mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
+            Dom.Mem.add_heap loc v mem
         | Typ.Tfloat _ ->
             let v =
-              Dom.Val.make_sym loc pname path new_sym_num
+              Dom.Val.make_sym pname path new_sym_num
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
-            mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
+            Dom.Mem.add_heap loc v mem
         | 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
@@ -183,12 +182,6 @@ 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 =
@@ -198,17 +191,12 @@ 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 bound_subst_map, ret_alias, rel_subst_map =
+        let subst_map, ret_alias =
           Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias
         in
-        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
+        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
     | None ->
         caller_mem
 
@@ -236,14 +224,6 @@ 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
@@ -384,9 +364,7 @@ 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
-    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
+    BoUtils.Check.array_access ~arr ~idx ~is_plus pname location cond_set
 
 
   let check_binop
@@ -425,10 +403,7 @@ module Report = struct
     match exp with
     | Exp.Var _ ->
         let arr = Sem.eval exp mem in
-        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
+        BoUtils.Check.array_access ~arr ~idx:Dom.Val.Itv.zero ~is_plus:true pname location cond_set
     | Exp.BinOp (bop, e1, e2) ->
         check_binop pname ~bop ~e1 ~e2 location mem cond_set
     | _ ->
@@ -443,13 +418,11 @@ module Report = struct
     let callee_cond = Dom.Summary.get_cond_set summary in
     match callee_pdesc with
     | Some pdesc ->
-        let bound_subst_map, _, rel_subst_map =
+        let 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
-        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
+        PO.ConditionSet.subst callee_cond subst_map caller_pname pname location
     | _ ->
         callee_cond
 
@@ -585,9 +558,6 @@ 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
@@ -600,34 +570,16 @@ 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 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 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 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,54 +13,31 @@ 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
-    ; sym: Relation.Sym.astate
-    ; powloc: PowLoc.astate
-    ; arrayblk: ArrayBlk.astate
-    ; offset_sym: Relation.Sym.astate
-    ; size_sym: Relation.Sym.astate
-    ; traces: TraceSet.t }
+    {itv: Itv.astate; powloc: PowLoc.astate; arrayblk: ArrayBlk.astate; traces: TraceSet.t}
 
   type t = astate
 
-  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 bot : t = {itv= Itv.bot; powloc= PowLoc.bot; arrayblk= ArrayBlk.bot; traces= TraceSet.empty}
 
   let pp fmt x =
-    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
+    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 unknown : traces:TraceSet.t -> t =
-   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 }
+   fun ~traces -> {itv= Itv.top; powloc= PowLoc.unknown; arrayblk= ArrayBlk.unknown; traces}
 
 
   let unknown_from : callee_pname:_ -> location:_ -> t =
@@ -74,11 +51,8 @@ module Val = struct
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else
-      Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym
-      && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc
+      Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && 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)
@@ -87,11 +61,8 @@ 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 }
 
 
@@ -100,20 +71,13 @@ 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
@@ -122,10 +86,6 @@ 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}
@@ -136,29 +96,20 @@ module Val = struct
 
   let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x}
 
-  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 of_array_blk : ArrayBlk.astate -> t = fun a -> {bot with arrayblk= a}
 
   let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
 
-  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 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 unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
+  let unknown_bit : t -> t = fun x -> {x with itv= Itv.top}
 
-  let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top}
+  let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv}
 
-  let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool; sym= Relation.Sym.top}
+  let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool}
 
   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}
@@ -344,15 +295,6 @@ 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
 
@@ -454,9 +396,10 @@ 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
@@ -563,7 +506,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
@@ -650,21 +593,11 @@ end
 
 module MemReach = struct
   type astate =
-    { stack: Stack.astate
-    ; heap: Heap.astate
-    ; alias: Alias.astate
-    ; latest_prune: LatestPrune.astate
-    ; relation: Relation.astate }
+    {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate; latest_prune: LatestPrune.astate}
 
   type t = astate
 
-  let init : t =
-    { stack= Stack.bot
-    ; heap= Heap.bot
-    ; alias= Alias.bot
-    ; latest_prune= LatestPrune.top
-    ; relation= Relation.empty }
-
+  let init : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot; latest_prune= LatestPrune.top}
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
@@ -672,7 +605,6 @@ 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 =
@@ -682,7 +614,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 =
@@ -690,15 +622,12 @@ 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
-    ; relation= Relation.join x.relation y.relation }
+    ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune }
 
 
   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 ;
-    if Option.is_some Config.bo_relational_domain then
-      F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
+    F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias
 
 
   let pp_summary : F.formatter -> t -> unit =
@@ -760,6 +689,13 @@ 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
@@ -832,41 +768,6 @@ 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
@@ -993,42 +894,6 @@ 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
@@ -1056,5 +921,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,7 +13,6 @@ module BoUtils = BufferOverrunUtils
 module Dom = BufferOverrunDomain
 module PO = BufferOverrunProofObligations
 module Sem = BufferOverrunSemantics
-module Relation = BufferOverrunDomainRelation
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
@@ -83,17 +82,12 @@ 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 allocsite typ ~stride ~offset ~size |> Dom.Val.set_traces traces
+      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
     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
@@ -184,8 +178,10 @@ 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 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
+        let v =
+          Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length
+            ~inst_num:0 ~dimension:1
+        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,7 +10,6 @@ open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module ItvPure = Itv.ItvPure
-module Relation = BufferOverrunDomainRelation
 module MF = MarkupFormatter
 module ValTraceSet = BufferOverrunTrace.Set
 
@@ -94,13 +93,7 @@ module AllocSizeCondition = struct
 end
 
 module ArrayAccessCondition = struct
-  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]
+  type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare]
 
   let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size
 
@@ -113,10 +106,7 @@ 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 ;
-    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
+    F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size
 
 
   let pp_description : F.formatter -> t -> unit =
@@ -125,12 +115,9 @@ 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 -> 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 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 have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} =
@@ -219,15 +206,8 @@ 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 =
-      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
+    let not_overrun = ItvPure.lt_sem c'.idx c'.size in
+    let not_underrun = 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 *)
@@ -255,22 +235,13 @@ module ArrayAccessCondition = struct
       {report_issue_type; propagate= is_symbolic}
 
 
-  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 ->
+  let subst : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t -> t option =
+   fun bound_map c ->
     match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with
     | NonBottom idx, NonBottom 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}
+        Some {idx; size}
     | _ ->
         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
@@ -287,11 +258,11 @@ module Condition = struct
         ArrayAccessCondition.get_symbols c
 
 
-  let subst bound_map rel_map caller_relation = function
+  let subst bound_map = function
     | AllocSize c ->
         AllocSizeCondition.subst bound_map c |> make_alloc_size
     | ArrayAccess c ->
-        ArrayAccessCondition.subst bound_map rel_map caller_relation c |> make_array_access
+        ArrayAccessCondition.subst bound_map c |> make_array_access
 
 
   let have_similar_bounds c1 c2 =
@@ -335,14 +306,6 @@ 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
@@ -423,12 +386,12 @@ module ConditionWithTrace = struct
         cmp
 
 
-  let subst (bound_map, trace_map) rel_map caller_relation caller_pname callee_pname location cwt =
+  let subst (bound_map, trace_map) caller_pname callee_pname location cwt =
     match Condition.get_symbols cwt.cond with
     | [] ->
         Some cwt
     | symbols ->
-      match Condition.subst bound_map rel_map caller_relation cwt.cond with
+      match Condition.subst bound_map cwt.cond with
       | None ->
           None
       | Some cond ->
@@ -462,9 +425,6 @@ 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
@@ -526,10 +486,9 @@ module ConditionSet = struct
         join [cwt] 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_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_alloc_size pname location ~length val_traces condset =
@@ -537,12 +496,10 @@ module ConditionSet = struct
     |> add_opt pname location val_traces condset
 
 
-  let subst condset bound_map_trace_map rel_subst_map caller_relation caller_pname callee_pname
-      location =
+  let subst condset bound_map_trace_map caller_pname callee_pname location =
     let subst_add_cwt condset cwt =
       match
-        ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation caller_pname
-          callee_pname location cwt
+        ConditionWithTrace.subst bound_map_trace_map caller_pname callee_pname location cwt
       with
       | None ->
           condset
@@ -567,13 +524,11 @@ module ConditionSet = struct
   let pp : Format.formatter -> t -> unit =
    fun fmt condset ->
     let pp_sep fmt () = F.fprintf fmt ", @," in
-    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)
+    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 "@]"
 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 -> Allocsite.t =
+let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string =
  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,19 +324,15 @@ let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension
 
 
 let eval_array_alloc
-    : Allocsite.t -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t =
- fun allocsite typ ~stride ~offset ~size ->
+    : 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
   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 ~allocsite
+  ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk
 
 
-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}
 
@@ -427,16 +423,12 @@ module Prune = struct
 
 
   let is_unreachable_constant : Exp.t -> Mem.astate -> bool =
-   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)
+   fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0)
 
 
   let prune_unreachable : Exp.t -> astate -> astate =
    fun e ({mem} as astate) ->
-    if is_unreachable_constant e mem || Mem.is_relation_unsat mem then {astate with mem= Mem.bot}
-    else astate
+    if is_unreachable_constant e mem then {astate with mem= Mem.bot} else astate
 
 
   let rec prune_helper e astate =
@@ -469,10 +461,6 @@ 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
@@ -484,17 +472,13 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
 
 
 let get_matching_pairs
-    : Tenv.t -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate -> Mem.astate
+    : Tenv.t -> Val.t -> Val.t -> 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
-         * (Relation.Var.t * Relation.SymExp.t option) list =
- fun tenv formal actual actual_exp_opt typ caller_mem callee_mem ~callee_ret_alias ->
+      -> (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 ->
   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
@@ -522,38 +506,17 @@ let get_matching_pairs
       else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l
     else l
   in
-  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) =
+  let add_pair_val v1 v2 pairs =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
-    let bound_pairs =
-      bound_pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2)
+    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' ~e2_opt:None pairs
+    add_pair_val v1' v2' pairs
   in
   let add_pair_ptr typ v1 v2 pairs =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
@@ -568,17 +531,15 @@ 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' ~e2_opt:None pairs
+        add_pair_val v1' v2' pairs
     | _ ->
         pairs
   in
-  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 pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in
+  (pairs, !ret_alias)
 
 
-let subst_map_of_bound_pairs
+let subst_map_of_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 ->
@@ -591,16 +552,8 @@ let subst_map_of_bound_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 * Exp.t option -> f:('a -> Val.t * Exp.t option -> 'b -> 'b) -> 'a list
-      -> (Val.t * Exp.t option) list -> init:'b -> 'b =
+    : default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b =
  fun ~default ~f xs ys ~init:acc ->
   match (xs, ys) with
   | [], _ ->
@@ -608,9 +561,7 @@ let rec list_fold2_def
   | x :: xs', [] ->
       list_fold2_def ~default ~f xs' ys ~init:(f x default acc)
   | [x], _ :: _ ->
-      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
+      f x (List.fold ~f:Val.join ~init:Val.bot ys) acc
   | x :: xs', y :: ys' ->
       list_fold2_def ~default ~f xs' ys' ~init:(f x y acc)
 
@@ -619,22 +570,18 @@ 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
-         * Relation.SubstMap.t =
+         * AliasTarget.t option =
  fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias ->
-  let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) =
+  let add_pair (formal, typ) actual (l, ret_alias) =
     let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in
-    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
+    let new_matching, ret_alias' =
+      get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias
     in
-    ( List.rev_append new_bound_matching bound_l
-    , Option.first_some ret_alias ret_alias'
-    , List.rev_append new_rel_matching rel_l )
+    (List.rev_append new_matching l, Option.first_some ret_alias ret_alias')
   in
   let formals = get_formals callee_pdesc in
-  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, [])
+  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)
   in
-  (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs)
+  (subst_map_of_pairs pairs, ret_alias)

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -10,7 +10,6 @@ open AbsLoc
 open! AbstractDomain.Types
 module L = Logging
 module Dom = BufferOverrunDomain
-module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
@@ -34,18 +33,15 @@ 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 allocsite typ ~stride ~offset ~size
+      Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num ~dimension
       |> 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 mem = Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None mem in
-    let loc = Loc.of_allocsite allocsite in
+    let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in
     let mem, _ =
       decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem
     in
@@ -73,14 +69,12 @@ 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 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
+      Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num
+        ~dimension:alloc_num
+      |> Dom.Val.add_trace_elem elem
     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
@@ -101,11 +95,11 @@ module Exec = struct
                   Itv.plus i length )
             in
             let stride = Option.map stride ~f:IntLit.to_int in
-            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
+            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
         | _ ->
             init_fields field_typ field_loc dimension ?dyn_length mem
       in
@@ -147,21 +141,14 @@ module Exec = struct
 end
 
 module Check = struct
-  let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set =
+  let array_access ~arr ~idx ~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 ;
@@ -169,8 +156,7 @@ 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 ~size_sym_exp ~idx_sym_exp
-          ~relation traces cond_set
+        PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set
     | _ ->
         cond_set
 
@@ -178,7 +164,5 @@ 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
-    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
+    array_access ~arr ~idx ~is_plus:true pname location cond_set
 end

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -8,7 +8,6 @@
 open! IStd
 open AbsLoc
 module Dom = BufferOverrunDomain
-module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 
 module Exec : sig
@@ -42,8 +41,7 @@ end
 
 module Check : sig
   val array_access :
-    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
+    arr:Dom.Val.t -> idx:Dom.Val.t -> is_plus:bool -> Typ.Procname.t -> Location.t
     -> PO.ConditionSet.t -> PO.ConditionSet.t
 
   val lindex :

infer/src/bufferoverrun/itv.ml

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

infer/src/jbuild.common.in

@@ -55,9 +55,6 @@ 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,8 +38,7 @@ let infer_cflags =
     ; "-open"
     ; "InferIR"
     ; "-open"
-    ; "InferBase"
-    ; "-cclib -lparmap_stubs" ]
+    ; "InferBase" ]
 
 
 (** The build stanzas to be passed to jbuilder *)

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

@@ -86,10 +86,6 @@ 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

@@ -1,43 +0,0 @@
-/*
- * 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,18 +27,14 @@ 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,21 +1,16 @@
 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
@@ -27,7 +22,6 @@ 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
@@ -35,7 +29,6 @@ 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