[pulse] preserve restricted variables across function calls

Summary:
When a variable (an `AbstractValue.t`) denotes a non-negative value,
nothing is recorded in the Pulse formula, we just represent that
variable with a *restricted* variable. We were losing information about
which variables are restricted when applying function calls as the
substitution would not take them into account and map them to
*unrestricted* variables.

Reviewed By: ezgicicek

Differential Revision: D32465508

fbshipit-source-id: e5bf5266c

infer/src/pulse/PulseAbstractValue.ml

@@ -33,6 +33,8 @@ let is_restricted v = v < 0
 
 let is_unrestricted v = v > 0
 
+let mk_fresh_same_kind v = if is_restricted v then mk_fresh_restricted () else mk_fresh ()
+
 let pp f v = if is_restricted v then F.fprintf f "a%d" (-v) else F.fprintf f "v%d" v
 
 let yojson_of_t l = `String (F.asprintf "%a" pp l)

infer/src/pulse/PulseAbstractValue.mli

@@ -7,17 +7,22 @@
 open! IStd
 module F = Format
 
-(** An abstract value, eg an address in memory. *)
+(** An abstract value (or "symbolic variable"), eg an address in memory. *)
 type t = private int [@@deriving compare, yojson_of]
 
 val equal : t -> t -> bool
 
 val mk_fresh : unit -> t
+(** create an abstract value guaranteed not to appear in the current state *)
 
 val mk_fresh_restricted : unit -> t
 (** a special class of variables that represent non-negative ("restricted") values; variables
     returned by [mk_fresh] are called "unrestricted" by opposition *)
 
+val mk_fresh_same_kind : t -> t
+(** creates a fresh restricted or unrestricted abstract value based on the kind of abstract value
+    given *)
+
 val is_restricted : t -> bool
 (** was the variable created with [mk_fresh_restricted], i.e. it represents non-negative values
     (hence its domain is {e restricted}) *)

infer/src/pulse/PulseInterproc.ml

@@ -154,7 +154,11 @@ let visit call_state ~pre ~addr_callee ~addr_hist_caller =
 let subst_find_or_new subst addr_callee ~default_hist_caller =
   match AddressMap.find_opt addr_callee subst with
   | None ->
-      let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in
+      (* map restricted (≥0) values to restricted values to preserve their semantics *)
+      let addr_caller = AbstractValue.mk_fresh_same_kind addr_callee in
+      L.d_printfln "new subst %a <-> %a (fresh)" AbstractValue.pp addr_callee AbstractValue.pp
+        addr_caller ;
+      let addr_hist_fresh = (addr_caller, default_hist_caller) in
       (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh)
   | Some addr_hist_caller ->
       (subst, addr_hist_caller)
@@ -513,7 +517,7 @@ let record_post_for_return ({PathContext.timestamp} as path) callee_proc_name ca
           | Some return_caller_hist ->
               return_caller_hist
           | None ->
-              (AbstractValue.mk_fresh (), ValueHistory.Epoch)
+              (AbstractValue.mk_fresh_same_kind return_callee, ValueHistory.Epoch)
         in
         L.d_printfln_escaped "Recording POST from [return] <-> %a" AbstractValue.pp return_caller ;
         let call_state =

infer/src/pulse/PulsePathCondition.ml

@@ -133,7 +133,11 @@ let simplify tenv ~can_be_pruned ~keep ~get_dynamic_type phi =
 let subst_find_or_new subst addr_callee =
   match AbstractValue.Map.find_opt addr_callee subst with
   | None ->
-      let addr_hist_fresh = (AbstractValue.mk_fresh (), ValueHistory.Epoch) in
+      (* map restricted (≥0) values to restricted values to preserve their semantics *)
+      let addr_caller = AbstractValue.mk_fresh_same_kind addr_callee in
+      L.d_printfln "new subst %a <-> %a (fresh)" AbstractValue.pp addr_callee AbstractValue.pp
+        addr_caller ;
+      let addr_hist_fresh = (addr_caller, ValueHistory.Epoch) in
       (AbstractValue.Map.add addr_callee addr_hist_fresh subst, fst addr_hist_fresh)
   | Some addr_hist_caller ->
       (subst, fst addr_hist_caller)

infer/tests/codetoanalyze/c/pulse/arithmetic.c

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <assert.h>
+#include <stdlib.h>
+
+int return_non_negative() {
+  int x = random();
+  if (x < 0) {
+    exit(1);
+  }
+  return x;
+}
+
+void return_non_negative_is_non_negative_ok() {
+  if (return_non_negative() < 0) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+void assume_non_negative(int x) {
+  if (x < 0) {
+    exit(1);
+  }
+}
+
+void assume_non_negative_is_non_negative_ok() {
+  int x = random();
+  assume_non_negative(x);
+  if (x < 0) {
+    int* p = NULL;
+    *p = 42;
+  }
+}