From 0574372891885ba65462772c9f89d7f5d948c2c1 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Wed, 18 Sep 2019 01:27:24 -0700
Subject: [PATCH] [inferbo] Simplify alias targets

Summary:
This diff simplifies two similar alias targets: AliasTarget.Simple and
AliasTarget.SimplePlusA.  Since the latter is simply extended version
of the former, they are better to have a common constructor.

Reviewed By: jvillard

Differential Revision: D17421416

fbshipit-source-id: e0946a73b
---
 .../src/bufferoverrun/bufferOverrunDomain.ml  | 36 ++++++++-----------
 .../bufferoverrun/bufferOverrunSemantics.ml   | 12 +++----
 2 files changed, 21 insertions(+), 27 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 093b7cd73..8013b845e 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -713,7 +713,7 @@ module AliasTarget = struct
      pruning values of program variables.  For example, a C statement "if(x){...}" is translated to
      "%r=load(x); if(%r){...}" in Sil.  At the load statement, we record the alias between the
      values of %r and x, then we can prune not only the value of %r, but also that of x inside the
-     if branch.
+     if branch.  The i field is to express "%r=load(x)+i".
 
    "Empty relation": For pruning vector.length with vector::empty() results, we adopt a specific
      relation between %r and v->elements, where %r=v.empty().  So, if %r!=0, v's array length
@@ -726,8 +726,7 @@ module AliasTarget = struct
      field is to express "%r=x.size()+i", which is required to follow the semantics of `Array.add`
      inside loops precisely. *)
   type t =
-    | Simple of Loc.t
-    | SimplePlusA of Loc.t * IntLit.t
+    | Simple of {l: Loc.t; i: IntLit.t}
     | Empty of Loc.t
     | Size of {l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | Fgets of Loc.t
@@ -742,10 +741,9 @@ module AliasTarget = struct
       else F.fprintf fmt "+%a" IntLit.pp i
     in
     fun fmt -> function
-      | Simple l ->
-          Loc.pp fmt l
-      | SimplePlusA (l, i) ->
-          Loc.pp fmt l ; intlit_pp fmt i
+      | Simple {l; i} ->
+          Loc.pp fmt l ;
+          if not (IntLit.iszero i) then intlit_pp fmt i
       | Empty l ->
           F.fprintf fmt "empty(%a)" Loc.pp l
       | Size {l; i; java_tmp} ->
@@ -763,7 +761,7 @@ module AliasTarget = struct
   let get_locs = function
     | Size {l; java_tmp= Some tmp} ->
         PowLoc.singleton l |> PowLoc.add tmp
-    | Simple l | SimplePlusA (l, _) | Size {l; java_tmp= None} | Empty l | Fgets l ->
+    | Simple {l} | Size {l; java_tmp= None} | Empty l | Fgets l ->
         PowLoc.singleton l
     | Top ->
         PowLoc.empty
@@ -773,10 +771,8 @@ module AliasTarget = struct
 
   let loc_map x ~f =
     match x with
-    | Simple l ->
-        Option.map (f l) ~f:(fun l -> Simple l)
-    | SimplePlusA (l, i) ->
-        Option.map (f l) ~f:(fun l -> SimplePlusA (l, i))
+    | Simple {l; i} ->
+        Option.map (f l) ~f:(fun l -> Simple {l; i})
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
     | Size {l; i; java_tmp} ->
@@ -863,7 +859,7 @@ module AliasMap = struct
     else
       let tgt =
         match tgt with
-        | AliasTarget.Simple loc when Language.curr_language_is Java ->
+        | AliasTarget.Simple {l= loc; i} when IntLit.iszero i && Language.curr_language_is Java ->
             Option.value (find_loc loc x) ~default:tgt
         | _ ->
             tgt
@@ -951,10 +947,10 @@ module Alias = struct
         else a
     | Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i))
     | Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) ->
-        lift_map (AliasMap.load id (AliasTarget.SimplePlusA (loc, IntLit.neg i))) a
+        lift_map (AliasMap.load id (AliasTarget.Simple {l= loc; i= IntLit.neg i})) a
         |> lift_map (AliasMap.store_n ~prev:prev.map loc id i)
     | Exp.BinOp (Binop.MinusA _, Exp.Var id, Exp.Const (Const.Cint i)) ->
-        lift_map (AliasMap.load id (AliasTarget.SimplePlusA (loc, i))) a
+        lift_map (AliasMap.load id (AliasTarget.Simple {l= loc; i})) a
         |> lift_map (AliasMap.store_n ~prev:prev.map loc id (IntLit.neg i))
     | _ ->
         a
@@ -1479,10 +1475,8 @@ module MemReach = struct
   let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option =
    fun k m ->
     match Alias.find_id k m.alias with
-    | Some (AliasTarget.Simple l) ->
-        Some (l, None)
-    | Some (AliasTarget.SimplePlusA (l, i)) ->
-        Some (l, Some i)
+    | Some (AliasTarget.Simple {l; i}) ->
+        Some (l, if IntLit.iszero i then None else Some i)
     | Some (AliasTarget.Empty _ | AliasTarget.Size _ | AliasTarget.Fgets _ | AliasTarget.Top)
     | None ->
         None
@@ -1646,7 +1640,7 @@ module MemReach = struct
         else {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
     | Lvar return, _, _ when Pvar.is_return return -> (
       match Alias.find_ret m.alias with
-      | Some (Simple (Var (ProgramVar pvar))) ->
+      | Some (Simple {l= Var (ProgramVar pvar); i}) when IntLit.iszero i ->
           {m with latest_prune= LatestPrune.replace ~from:pvar ~to_:return m.latest_prune}
       | _ ->
           m )
@@ -1828,7 +1822,7 @@ module Mem = struct
 
 
   let load_simple_alias : Ident.t -> Loc.t -> t -> t =
-   fun id loc -> load_alias id (AliasTarget.Simple loc)
+   fun id loc -> load_alias id (AliasTarget.Simple {l= loc; i= IntLit.zero})
 
 
   let load_empty_alias : Ident.t -> Loc.t -> t -> t =
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 0712f949b..af256928b 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -307,10 +307,10 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
   match exp with
   | Exp.Var id -> (
     match Mem.find_alias id mem with
-    | Some (AliasTarget.Simple loc) ->
+    | Some (AliasTarget.Simple {l= loc; i}) when IntLit.iszero i ->
         Mem.find loc mem
     | Some
-        ( AliasTarget.SimplePlusA _
+        ( AliasTarget.Simple _
         | AliasTarget.Size _
         | AliasTarget.Empty _
         | AliasTarget.Fgets _
@@ -498,7 +498,7 @@ module Prune = struct
     match e with
     | Exp.Var x -> (
       match Mem.find_alias x mem with
-      | Some (AliasTarget.Simple lv) ->
+      | Some (AliasTarget.Simple {l= lv; i}) when IntLit.iszero i ->
           let v = Mem.find lv mem in
           let v' = Val.prune_ne_zero v in
           update_mem_in_prune lv v' astate
@@ -510,11 +510,11 @@ module Prune = struct
           let strlen_loc = Loc.of_c_strlen lv in
           let v' = Val.prune_ge_one (Mem.find strlen_loc mem) in
           update_mem_in_prune strlen_loc v' astate
-      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | Top) | None ->
+      | Some (AliasTarget.Simple _ | AliasTarget.Size _ | Top) | None ->
           astate )
     | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
       match Mem.find_alias x mem with
-      | Some (AliasTarget.Simple lv) ->
+      | Some (AliasTarget.Simple {l= lv; i}) when IntLit.iszero i ->
           let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
@@ -522,7 +522,7 @@ module Prune = struct
           let v = Mem.find lv mem in
           let v' = Val.prune_length_ge_one v in
           update_mem_in_prune lv v' astate
-      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _ | Top) | None ->
+      | Some (AliasTarget.Simple _ | AliasTarget.Size _ | AliasTarget.Fgets _ | Top) | None ->
           astate )
     | _ ->
         astate