[pulse] Add semantic models for C++ string length

Summary:
This diff adds some semantic models for C++ string length. It introduces
an virtual field for string length and use the value in the models.

* basic_string constructor given a constant string
* string.empty
* string.length

Reviewed By: jvillard

Differential Revision: D29390815

fbshipit-source-id: 99d67e48e

infer/src/pulse/PulseModels.ml

@@ -23,8 +23,6 @@ type model = model_data -> AbductiveDomain.t -> ExecutionDomain.t AccessResult.t
 
 let ok_continue post = [Ok (ContinueProgram post)]
 
-let cpp_model_namespace = QualifiedCppName.of_list ["__infer_pulse_model"]
-
 module Misc = struct
   let shallow_copy_value path location event ret_id dest_pointer_hist src_value_hist astate =
     let<*> astate, obj_copy = PulseOperations.shallow_copy path location src_value_hist astate in
@@ -311,7 +309,7 @@ module ObjC = struct
 end
 
 module Optional = struct
-  let internal_value = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_value"
+  let internal_value = Fieldname.make PulseOperations.pulse_model_type "backing_value"
 
   let internal_value_access = HilExp.Access.FieldAccess internal_value
 
@@ -625,10 +623,29 @@ module StdBasicString = struct
 
   let internal_string_access = HilExp.Access.FieldAccess internal_string
 
+  let string_length_access = HilExp.Access.FieldAccess PulseOperations.ModeledField.string_length
+
   let to_internal_string path location bstring astate =
     PulseOperations.eval_access path Read location bstring internal_string_access astate
 
 
+  (* constructor from constant string *)
+  let constructor this_hist init_hist : model =
+   fun {path; location} astate ->
+    let event =
+      ValueHistory.Call {f= Model "std::basic_string::basic_string()"; location; in_call= []}
+    in
+    let<*> astate, (addr, hist) =
+      PulseOperations.eval_access path Write location this_hist Dereference astate
+    in
+    let<+> astate =
+      PulseOperations.write_field path location
+        ~ref:(addr, event :: hist)
+        internal_string ~obj:init_hist astate
+    in
+    astate
+
+
   let data this_hist : model =
    fun {path; location; ret= ret_id, _} astate ->
     let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in
@@ -657,6 +674,37 @@ module StdBasicString = struct
         location CppDelete string_addr_hist astate
     in
     astate
+
+
+  let empty this_hist : model =
+   fun {path; location; ret= ret_id, _} astate ->
+    let event = ValueHistory.Call {f= Model "std::basic_string::empty()"; location; in_call= []} in
+    let<*> astate, internal_string = to_internal_string path location this_hist astate in
+    let<*> astate, (len_addr, hist) =
+      PulseOperations.eval_access path Read location internal_string string_length_access astate
+    in
+    let ((ret_addr, _) as ret_hist) = (AbstractValue.mk_fresh (), event :: hist) in
+    let astate_empty =
+      let<*> astate = PulseArithmetic.prune_eq_zero len_addr astate in
+      let<+> astate = PulseArithmetic.and_eq_int ret_addr IntLit.one astate in
+      PulseOperations.write_id ret_id ret_hist astate
+    in
+    let astate_non_empty =
+      let<*> astate = PulseArithmetic.prune_positive len_addr astate in
+      let<+> astate = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate in
+      PulseOperations.write_id ret_id ret_hist astate
+    in
+    List.rev_append astate_empty astate_non_empty
+
+
+  let length this_hist : model =
+   fun {path; location; ret= ret_id, _} astate ->
+    let event = ValueHistory.Call {f= Model "std::basic_string::length()"; location; in_call= []} in
+    let<*> astate, internal_string = to_internal_string path location this_hist astate in
+    let<+> astate, (length, hist) =
+      PulseOperations.eval_access path Read location internal_string string_length_access astate
+    in
+    PulseOperations.write_id ret_id (length, event :: hist) astate
 end
 
 module StdFunction = struct
@@ -704,11 +752,11 @@ module StdFunction = struct
 end
 
 module GenericArrayBackedCollection = struct
-  let field = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_array"
+  let field = Fieldname.make PulseOperations.pulse_model_type "backing_array"
 
-  let last_field = Fieldname.make (Typ.CStruct cpp_model_namespace) "past_the_end"
+  let last_field = Fieldname.make PulseOperations.pulse_model_type "past_the_end"
 
-  let is_empty = Fieldname.make (Typ.CStruct cpp_model_namespace) "is_empty"
+  let is_empty = Fieldname.make PulseOperations.pulse_model_type "is_empty"
 
   let access = HilExp.Access.FieldAccess field
 
@@ -741,7 +789,7 @@ module GenericArrayBackedCollection = struct
 end
 
 module GenericArrayBackedCollectionIterator = struct
-  let internal_pointer = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_pointer"
+  let internal_pointer = Fieldname.make PulseOperations.pulse_model_type "backing_pointer"
 
   let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer
 
@@ -1607,7 +1655,11 @@ module ProcNameDispatcher = struct
         ; -"std" &:: "optional" &:: "value_or" $ capt_arg_payload $+ capt_arg_payload
           $+...$--> Optional.value_or ~desc:"std::optional::value_or()"
           (* end std::optional *)
+        ; -"std" &:: "basic_string" &:: "basic_string" $ capt_arg_payload $+ capt_arg_payload
+          $--> StdBasicString.constructor
         ; -"std" &:: "basic_string" &:: "data" <>$ capt_arg_payload $--> StdBasicString.data
+        ; -"std" &:: "basic_string" &:: "empty" <>$ capt_arg_payload $--> StdBasicString.empty
+        ; -"std" &:: "basic_string" &:: "length" <>$ capt_arg_payload $--> StdBasicString.length
         ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_arg_payload
           $--> StdBasicString.destructor
         ; -"std" &:: "function" &:: "function" $ capt_arg_payload $+ capt_arg

infer/src/pulse/PulseOperations.ml

@@ -172,6 +172,12 @@ module Closures = struct
     (astate, closure_addr_hist)
 end
 
+let pulse_model_type = Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"])
+
+module ModeledField = struct
+  let string_length = Fieldname.make pulse_model_type "__infer_model_string_length"
+end
+
 let eval_access path ?must_be_valid_reason mode location addr_hist access astate =
   let+ astate = check_addr_access path ?must_be_valid_reason mode location addr_hist astate in
   Memory.eval_edge addr_hist access astate
@@ -236,6 +242,16 @@ let eval path mode location exp0 astate =
                 invalidation location
         in
         (astate, (v, [ValueHistory.Invalidated (invalidation, location)]))
+    | Const (Cstr s) ->
+        let v = AbstractValue.mk_fresh () in
+        let* astate, (len_addr, hist) =
+          eval_access path Write location
+            (v, [Assignment location])
+            (FieldAccess ModeledField.string_length) astate
+        in
+        let len_int = IntLit.of_int (String.length s) in
+        let+ astate = PulseArithmetic.and_eq_int len_addr len_int astate in
+        (astate, (v, hist))
     | UnOp (unop, exp, _typ) ->
         let* astate, (addr, hist) = eval path Read exp astate in
         let unop_addr = AbstractValue.mk_fresh () in

infer/src/pulse/PulseOperations.mli

@@ -83,6 +83,14 @@ module Closures : sig
   (** assert the validity of the addresses captured by the lambda *)
 end
 
+val pulse_model_type : Typ.name
+(** Struct type name of "__infer_pulse_model" *)
+
+module ModeledField : sig
+  val string_length : Fieldname.t
+  (** Modeled field for string length *)
+end
+
 val eval :
      PathContext.t
   -> access_mode

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -102,8 +102,6 @@ codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_te
 codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `temporaries::mk_UniquePtr_A`,allocated by call to `new` (modelled),in call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr<temporaries::A>::~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::~UniquePtr,when calling `temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `temporaries::mk_UniquePtr_A`,allocated by call to `new` (modelled),in call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,in call to `temporaries::UniquePtr<temporaries::A>::get`,parameter `this` of temporaries::UniquePtr<temporaries::A>::get,returned,return from call to `temporaries::UniquePtr<temporaries::A>::get`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,in call to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/traces.cpp, access_destructed_string, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,in call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,in call to `std::basic_string::data()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/uninit.cpp, Uninit2::not_read_f1_ok_FP, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f1` created,when calling `Uninit2::may_read_f1` here,parameter `this` of Uninit2::may_read_f1,read to uninitialized value occurs here]
-codetoanalyze/cpp/pulse/uninit.cpp, Uninit2::not_read_f2_ok_FP, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f1` created,when calling `Uninit2::may_read_f2` here,parameter `this` of Uninit2::may_read_f2,read to uninitialized value occurs here]
 codetoanalyze/cpp/pulse/uninit.cpp, Uninit2::read_f1_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f1` created,when calling `Uninit2::may_read_f1` here,parameter `this` of Uninit2::may_read_f1,read to uninitialized value occurs here]
 codetoanalyze/cpp/pulse/uninit.cpp, Uninit2::read_f2_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f1` created,when calling `Uninit2::may_read_f2` here,parameter `this` of Uninit2::may_read_f2,read to uninitialized value occurs here]
 codetoanalyze/cpp/pulse/uninit.cpp, Uninit::call_init_by_store_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `i` created,read to uninitialized value occurs here]

infer/tests/codetoanalyze/cpp/pulse/uninit.cpp

@@ -46,7 +46,7 @@ class Uninit2 {
     }
   }
 
-  void not_read_f1_ok_FP() {
+  void not_read_f1_ok() {
     Uninit2 o;
     o.may_read_f1("non empty string");
   }
@@ -62,7 +62,7 @@ class Uninit2 {
     }
   }
 
-  void not_read_f2_ok_FP() {
+  void not_read_f2_ok() {
     Uninit2 o;
     o.may_read_f2("non empty string");
   }

infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java

@@ -23,7 +23,7 @@ public class TextUtilsExample {
     }
   }
 
-  public void testTextUtilsIsEmptyEmptyStrBad() {
+  public void FN_testTextUtilsIsEmptyEmptyStrBad() {
     if (TextUtils.isEmpty("")) {
       Object o = null;
       o.toString();

infer/tests/codetoanalyze/java/pulse/issues.exp

@@ -67,5 +67,4 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]

infer/tests/codetoanalyze/java/pulse/issues.exp-isl

@@ -67,5 +67,4 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp
 codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]