From 98e27f5c4ab6970b28add66329eeb9b7c9931b9c Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Tue, 15 Oct 2019 03:36:45 -0700
Subject: [PATCH] [pulse] record equality to constants as attributes

Summary:
First step in having a value domain: record concrete values. We record
them as equalities to abstract values using a new attribute `Constant`.
In a way, attributes are already our "pure" part in the "formulas" that
are pulse abstract domains, so this is reminiscent of existing
separation logic implementations. Trying to add values directly in the
"heap" part proved very cumbersome whereas this approach is very simple,
allowing us to ignore values most of the time except when we actually
care.

Reviewed By: skcho

Differential Revision: D17665473

fbshipit-source-id: b8033ad9c
---
 infer/src/pulse/PulseAbductiveDomain.ml | 7 ++++---
 infer/src/pulse/PulseDomain.ml          | 3 +++
 infer/src/pulse/PulseDomain.mli         | 1 +
 infer/src/pulse/PulseOperations.ml      | 7 ++++++-
 4 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index eb162b81b..109168ac9 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -578,12 +578,13 @@ module PrePost = struct
               PulseDomain.InterprocAction.ViaCall
                 {action= trace.action; f= Call proc_name; location}
           ; history= trace.history }
-    | MustBeValid _
-    | WrittenTo _
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
     | Closure _
-    | StdVectorReserve ->
+    | Constant _
+    | MustBeValid _
+    | StdVectorReserve
+    | WrittenTo _ ->
         attr
 
 
diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml
index f9955f296..af42b0a77 100644
--- a/infer/src/pulse/PulseDomain.ml
+++ b/infer/src/pulse/PulseDomain.ml
@@ -255,6 +255,7 @@ module Attribute = struct
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t
     | Closure of Typ.Procname.t
+    | Constant of Const.t
     | Invalid of Invalidation.t Trace.t
     | MustBeValid of unit InterprocAction.t
     | StdVectorReserve
@@ -293,6 +294,8 @@ module Attribute = struct
         F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location
     | Closure pname ->
         Typ.Procname.pp f pname
+    | Constant c ->
+        F.fprintf f "=%a" (Const.pp Pp.text) c
     | Invalid invalidation ->
         (Trace.pp Invalidation.pp) f invalidation
     | MustBeValid action ->
diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli
index 8cae2c2ea..7db9cca01 100644
--- a/infer/src/pulse/PulseDomain.mli
+++ b/infer/src/pulse/PulseDomain.mli
@@ -84,6 +84,7 @@ module Attribute : sig
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t
     | Closure of Typ.Procname.t
+    | Constant of Const.t
     | Invalid of Invalidation.t Trace.t
     | MustBeValid of unit InterprocAction.t
     | StdVectorReserve
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 3c6b2adcb..d32016d1b 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -146,7 +146,12 @@ let eval location exp0 astate =
         Closures.record location name (List.rev rev_captured) astate
     | Cast (_, exp') ->
         eval exp' astate
-    | Sizeof _ | UnOp _ | BinOp _ | Exn _ | Const _ ->
+    | Const c ->
+        (* TODO: make identical const the same address *)
+        let addr = AbstractAddress.mk_fresh () in
+        let astate = Memory.add_attribute addr (Constant c) astate in
+        Ok (astate, (addr, []))
+    | Sizeof _ | UnOp _ | BinOp _ | Exn _ ->
         Ok (astate, (AbstractAddress.mk_fresh (), (* TODO history *) []))
   in
   eval exp0 astate