From 53278f780c9ddc3241d61796154564898a60ad04 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Mon, 31 Jul 2017 12:13:26 -0700 Subject: [PATCH] [infer][biabduction] simplify the symbolic execution of the execute load instruction Summary: This was reusing the side effects of the `add_constraints_on_retval` for the final purpose of being angelic and just assigning a fresh value to the lhs of the load. Reviewed By: sblackshear Differential Revision: D5507037 fbshipit-source-id: ec1c89c --- infer/src/backend/symExec.ml | 32 +++++-------------- .../tests/codetoanalyze/java/infer/issues.exp | 2 +- 2 files changed, 9 insertions(+), 25 deletions(-) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 3c8259d98..0c25350e7 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -989,33 +989,17 @@ let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ lo match check_constant_string_dereference n_rhs_exp' with | Some value -> [Prop.conjoin_eq tenv (Exp.Var id) value prop] - | None - -> let exp_get_undef_attr exp = - let fold_undef_pname callee_opt atom = - match (callee_opt, atom) with - | None, Sil.Apred (Aundef _, _) - -> Some atom - | _ - -> callee_opt - in - List.fold ~f:fold_undef_pname ~init:None (Attribute.get_for_exp tenv prop exp) - in - let prop' = - if Config.angelic_execution && not (Exp.is_stack_addr n_rhs_exp') then - (* when we try to deref an undefined value, add it to the footprint *) - match exp_get_undef_attr n_rhs_exp' with - | Some Apred (Aundef (callee_pname, ret_annots, callee_loc, _), _) - -> let has_nullable_annot = Annotations.ia_is_nullable ret_annots in - add_constraints_on_retval tenv pdesc prop n_rhs_exp' ~has_nullable_annot typ - callee_pname callee_loc - | _ - -> prop - else prop - in + | None -> + try let iter_list = - Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop' loc + Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop loc in List.rev (List.fold ~f:(execute_load_ pdesc tenv id loc) ~init:[] iter_list) + with Exceptions.Symexec_memory_error _ -> + (* This should normally be a real alarm and should not be caught but currently happens + when the normalization drops hpreds of the form ident |-> footprint var. *) + let undef = Exp.get_undefined !Config.footprint in + [Prop.conjoin_eq tenv (Exp.Var id) undef prop] with Rearrange.ARRAY_ACCESS -> if Int.equal Config.array_level 0 then assert false else diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index b9f046e49..e98537a90 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -19,7 +19,7 @@ codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDeref codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(), 3, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipped call: function or method not found,Skipped call: function or method not found] codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 2, RETURN_VALUE_IGNORED, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative()] codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 3, RETURN_VALUE_IGNORED, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj()] -codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 26, DIVIDE_BY_ZERO, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),return from a call to void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...),return from a call to void AnalysisStops.divideByParam(int),return from a call to void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),return from a call to void AnalysisStops.castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),Skipped call: function or method not found,return from a call to void AnalysisStops.callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalseNegative(),Skipped call: function or method not found,start of procedure retZero(),return from a call to int AnalysisStops$MyObj.retZero(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure retOne(),return from a call to int AnalysisStops$MyObj.retOne(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldWriteOnUndefinedObjMayCauseFalseNegative(),Skipped call: function or method not found,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldWriteOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldReadOnUndefinedObjMayCauseFalseNegative(),Skipped call: function or method not found,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,Skipped call: function or method not found,start of procedure infiniteMaterializationMayCauseFalseNegative(...),Skipped call: function or method not found,Taking false branch,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalseNegative(boolean),start of procedure infiniteMaterializationMayCauseFalsePositive(...),Skipped call: function or method not found,Taking false branch,Skipped call: function or method not found,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalsePositive(boolean),start of procedure primitiveFieldOfAngelicObjMayCauseFalsePositive(),Skipped call: function or method not found,Taking true branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalsePositive(),start of procedure primitiveFieldOfAngelicObjMayCauseFalseNegative(),Skipped call: function or method not found,Taking false branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalseNegative(),start of procedure heapFieldOfAngelicObjMayCauseFalsePositive(),Skipped call: function or method not found,Taking false branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalsePositive(),start of procedure heapFieldOfAngelicObjMayCauseFalseNegative(),Skipped call: function or method not found,Taking true branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalseNegative(),Skipped call: function or method not found,start of procedure fieldReadInCalleeMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure derefParam(...),Skipped call: function or method not found,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeMayCauseFalsePositive(),start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure derefParam(...),Skipped call: function or method not found,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),start of procedure accessPathInCalleeMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure accessPathOnParam(...),Skipped call: function or method not found,return from a call to void AnalysisStops.accessPathOnParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.accessPathInCalleeMayCauseFalsePositive()] +codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 26, DIVIDE_BY_ZERO, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),return from a call to void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...),return from a call to void AnalysisStops.divideByParam(int),return from a call to void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),return from a call to void AnalysisStops.castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),Skipped call: function or method not found,return from a call to void AnalysisStops.callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalseNegative(),Skipped call: function or method not found,start of procedure retZero(),return from a call to int AnalysisStops$MyObj.retZero(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure retOne(),return from a call to int AnalysisStops$MyObj.retOne(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldWriteOnUndefinedObjMayCauseFalseNegative(),Skipped call: function or method not found,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldWriteOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldReadOnUndefinedObjMayCauseFalseNegative(),Skipped call: function or method not found,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipped call: function or method not found,Skipped call: function or method not found,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalsePositive(),start of procedure recursiveAngelicTypesMayCauseFalseNegative(),Skipped call: function or method not found,return from a call to void AnalysisStops.recursiveAngelicTypesMayCauseFalseNegative(),Skipped call: function or method not found,start of procedure infiniteMaterializationMayCauseFalseNegative(...),Skipped call: function or method not found,Taking false branch,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalseNegative(boolean),start of procedure infiniteMaterializationMayCauseFalsePositive(...),Skipped call: function or method not found,Taking false branch,Skipped call: function or method not found,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalsePositive(boolean),start of procedure primitiveFieldOfAngelicObjMayCauseFalsePositive(),Skipped call: function or method not found,Taking true branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalsePositive(),start of procedure primitiveFieldOfAngelicObjMayCauseFalseNegative(),Skipped call: function or method not found,Taking false branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalseNegative(),start of procedure heapFieldOfAngelicObjMayCauseFalsePositive(),Skipped call: function or method not found,Taking false branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalsePositive(),start of procedure heapFieldOfAngelicObjMayCauseFalseNegative(),Skipped call: function or method not found,Taking true branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalseNegative(),Skipped call: function or method not found,start of procedure fieldReadInCalleeMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure derefParam(...),Skipped call: function or method not found,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeMayCauseFalsePositive(),start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure derefParam(...),Skipped call: function or method not found,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),start of procedure accessPathInCalleeMayCauseFalsePositive(),Skipped call: function or method not found,start of procedure accessPathOnParam(...),Skipped call: function or method not found,return from a call to void AnalysisStops.accessPathOnParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.accessPathInCalleeMayCauseFalsePositive()] codetoanalyze/java/infer/ArrayOutOfBounds.java, int ArrayOutOfBounds.arrayOutOfBounds(), 2, ARRAY_OUT_OF_BOUNDS_L1, [start of procedure arrayOutOfBounds()] codetoanalyze/java/infer/Builtins.java, void Builtins.causeError(Object), 2, NULL_DEREFERENCE, [start of procedure causeError(...),Taking true branch] codetoanalyze/java/infer/Builtins.java, void Builtins.doNotBlockError(Object), 3, NULL_DEREFERENCE, [start of procedure doNotBlockError(...),Taking true branch]