[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

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

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

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

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 =