From f43901bc69b5e6d0baae165bd098fc708678b815 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 19 Jun 2020 08:49:03 -0700
Subject: [PATCH] [CCBM] Revise assignment semantics

Summary:
This diff revises assignment semantics, so it can store/load from the
heap location.

Reviewed By: ezgicicek

Differential Revision: D22042823

fbshipit-source-id: 20d91bfc5
---
 .../checkers/ConfigChecksBetweenMarkers.ml    | 48 +++++++++++++------
 infer/src/opensource/FbGKInteraction.ml       | 14 +++++-
 infer/src/opensource/FbGKInteraction.mli      | 12 ++++-
 3 files changed, 58 insertions(+), 16 deletions(-)

diff --git a/infer/src/checkers/ConfigChecksBetweenMarkers.ml b/infer/src/checkers/ConfigChecksBetweenMarkers.ml
index 296071c49..c3114d7c0 100644
--- a/infer/src/checkers/ConfigChecksBetweenMarkers.ml
+++ b/infer/src/checkers/ConfigChecksBetweenMarkers.ml
@@ -8,13 +8,7 @@
 open! IStd
 open AbstractDomain.Types
 module F = Format
-
-module ConfigName = struct
-  type t = {config_class: Pvar.t; config_name: Fieldname.t} [@@deriving compare, equal]
-
-  (** For readability, this prints short name of config. *)
-  let pp f {config_name} = F.fprintf f "%a" Fieldname.pp config_name
-end
+module ConfigName = FbGKInteraction.ConfigName
 
 module ConfigTopLifted = struct
   type t = ConfigName.t top_lifted
@@ -40,7 +34,22 @@ module ConfigWithLocation = struct
   let pp f (config, location) = F.fprintf f "%a at %a" ConfigName.pp config Location.pp location
 end
 
-module Mem = AbstractDomain.Map (Ident) (ConfigTopLifted)
+module Loc = struct
+  type t = Id of Ident.t | Pvar of Pvar.t [@@deriving compare]
+
+  let pp f = function Id id -> Ident.pp f id | Pvar pvar -> Pvar.pp Pp.text f pvar
+
+  let of_id id = Id id
+
+  let of_pvar pvar = Pvar pvar
+end
+
+module Mem = struct
+  include AbstractDomain.Map (Loc) (ConfigTopLifted)
+
+  let copy ~to_ ~from mem =
+    Option.value_map (find_opt from mem) ~default:mem ~f:(fun config -> add to_ config mem)
+end
 
 module Trace = struct
   type elem = MarkerStart of IntLit.t | ConfigCheck of ConfigName.t
@@ -306,9 +315,15 @@ module Dom = struct
     && ConfigChecks.leq ~lhs:lhs.config_checks ~rhs:rhs.config_checks
 
 
-  let load_config id ~config_class ~config_name ({mem} as astate) =
-    {astate with mem= Mem.add id (NonTop {ConfigName.config_class; config_name}) mem}
+  let load_constant_config id config ({mem} as astate) =
+    {astate with mem= Mem.add id (NonTop config) mem}
+
+
+  let mem_copy ~to_ ~from ({mem} as astate) = {astate with mem= Mem.copy ~to_ ~from mem}
+
+  let load_config id pvar astate = mem_copy ~to_:(Loc.of_id id) ~from:(Loc.of_pvar pvar) astate
 
+  let store_config pvar id astate = mem_copy ~to_:(Loc.of_pvar pvar) ~from:(Loc.of_id id) astate
 
   let call_marker_start marker location ({context} as astate) =
     {astate with context= Context.call_marker_start marker location context}
@@ -319,7 +334,7 @@ module Dom = struct
 
 
   let call_config_check analysis_data id location ({mem; context; config_checks} as astate) =
-    match Mem.find_opt id mem with
+    match Mem.find_opt (Loc.of_id id) mem with
     | Some (NonTop config) ->
         let trace_elem = Trace.config_check config in
         let context = Context.call_config_check trace_elem location context in
@@ -376,9 +391,14 @@ module TransferFunctions = struct
   let exec_instr astate ({InterproceduralAnalysis.tenv; analyze_dependency} as analysis_data) _node
       instr =
     match (instr : Sil.instr) with
-    | Load {id; e= Lfield (Lvar config_class, config_name, _)}
-      when FbGKInteraction.is_config_class config_class ->
-        Dom.load_config id ~config_class ~config_name astate
+    | Load {id; e} -> (
+      match FbGKInteraction.get_config e with
+      | Some config ->
+          Dom.load_constant_config (Loc.of_id id) config astate
+      | None -> (
+        match e with Lvar pvar -> Dom.load_config id pvar astate | _ -> astate ) )
+    | Store {e1= Lvar pvar; e2= Exp.Var id} ->
+        Dom.store_config pvar id astate
     | Call (_, Const (Cfun callee), _ :: (Const (Cint marker), _) :: _, location, _)
       when FbGKInteraction.is_marker_start tenv callee ->
         Dom.call_marker_start marker location astate
diff --git a/infer/src/opensource/FbGKInteraction.ml b/infer/src/opensource/FbGKInteraction.ml
index 8c3967b86..ba63de548 100644
--- a/infer/src/opensource/FbGKInteraction.ml
+++ b/infer/src/opensource/FbGKInteraction.ml
@@ -5,7 +5,19 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let is_config_class _ = false
+module F = Format
+
+module ConfigName = struct
+  type t = unit
+
+  let compare _ _ = 0
+
+  let equal _ _ = true
+
+  let pp f () = F.pp_print_string f "()"
+end
+
+let get_config _ = None
 
 let is_config_check _ _ = false
 
diff --git a/infer/src/opensource/FbGKInteraction.mli b/infer/src/opensource/FbGKInteraction.mli
index e1574dfe7..b88727841 100644
--- a/infer/src/opensource/FbGKInteraction.mli
+++ b/infer/src/opensource/FbGKInteraction.mli
@@ -5,7 +5,17 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-val is_config_class : 'pvar -> bool
+module ConfigName : sig
+  type t
+
+  val compare : t -> t -> int
+
+  val equal : t -> t -> bool
+
+  val pp : Format.formatter -> t -> unit
+end
+
+val get_config : 'exp -> 'config_name option
 
 val is_config_check : 'tenv -> 'pname -> bool