diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 823a4c4c8..502f6ff41 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index e4064b010..205c33e3e 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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 diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 7bb2c2abf..10016051f 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index ec39de095..b4e89a417 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr::~UniquePtr` here,parameter `this` of temporaries::UniquePtr::~UniquePtr,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr::__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::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,in call to `temporaries::UniquePtr::get`,parameter `this` of temporaries::UniquePtr::get,returned,return from call to `temporaries::UniquePtr::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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp b/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp index 942d6cfd1..1d757119c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp +++ b/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"); } diff --git a/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java b/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java index e397cd879..66f23b3f7 100644 --- a/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java +++ b/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(); diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 6f3863322..9d228f269 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp-isl b/infer/tests/codetoanalyze/java/pulse/issues.exp-isl index 7b07dcf6f..d700464d2 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp-isl +++ b/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]