From 3aa712c67ab4864119fd4d45a155929b69fe2dc5 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Mon, 22 Oct 2018 07:58:56 -0700
Subject: [PATCH] [pulse] define havoc and use in symbolic execution

Summary: Assigns non-deterministic value to some variable.

Reviewed By: mbouaziz

Differential Revision: D10483977

fbshipit-source-id: dc5050886
---
 infer/src/checkers/Pulse.ml        | 6 +++++-
 infer/src/checkers/PulseDomain.ml  | 2 ++
 infer/src/checkers/PulseDomain.mli | 2 ++
 infer/src/checkers/PulseModels.ml  | 2 +-
 4 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml
index 30d02b0ed..9967fb84e 100644
--- a/infer/src/checkers/Pulse.ml
+++ b/infer/src/checkers/Pulse.ml
@@ -39,7 +39,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | Direct callee_pname ->
           PulseModels.dispatch callee_pname
     in
-    match model with None -> Ok astate | Some model -> model call_loc ~ret ~actuals astate
+    match model with
+    | None ->
+        PulseDomain.havoc (fst ret) astate |> Result.return
+    | Some model ->
+        model call_loc ~ret ~actuals astate
 
 
   let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)
diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml
index e38021bf4..f4ad1da85 100644
--- a/infer/src/checkers/PulseDomain.ml
+++ b/infer/src/checkers/PulseDomain.ml
@@ -285,6 +285,8 @@ let write location access_expr addr astate =
   overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate
 
 
+let havoc var astate = {astate with stack= AliasingDomain.remove var astate.stack}
+
 let invalidate location access_expr astate =
   materialize_address astate access_expr location
   >>= fun (astate, addr) ->
diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli
index 81542e40e..90d7825a5 100644
--- a/infer/src/checkers/PulseDomain.mli
+++ b/infer/src/checkers/PulseDomain.mli
@@ -64,6 +64,8 @@ val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) acce
 
 val read_all : Location.t -> AccessExpression.t list -> t -> t access_result
 
+val havoc : Var.t -> t -> t
+
 val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result
 
 val invalidate : Location.t -> AccessExpression.t -> t -> t access_result
diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml
index 47ff0ae4b..767d799fc 100644
--- a/infer/src/checkers/PulseModels.ml
+++ b/infer/src/checkers/PulseModels.ml
@@ -45,7 +45,7 @@ module StdVector = struct
         PulseDomain.read location (deref_internal_array vector) astate
         >>= fun (astate, loc) -> PulseDomain.write location (AccessExpression.Base ret) loc astate
     | _ ->
-        Ok astate
+        Ok (PulseDomain.havoc (fst ret) astate)
 
 
   let push_back : model =