[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

@@ -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
 
 

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 ->

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

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