pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Using checkers defined in linter.al and removed hard-coded checkers.

Browse Source 
Summary:
This diff allows to use the linters written in DSL to check for bugs.
Now new checkers can be written directly in the DSL.

The diff also remove some weirdness and simplify the CTL semantics.
For example no need to unwrap a node when evaluating the IN operator.
Also no need to distinguish anymore between stmt and decl in the
semantics of EX and EF.

Moreover, the diff de-couple hard-coded checkers (eg checks on component kit)
from those checkers parsed in the .al files.

Reviewed By: martinoluca

Differential Revision: D4375207

fbshipit-source-id: 9ac2d47
master
Dino Distefano 8 years ago committed by Facebook Github Bot
parent 7bcc7e421d
commit 45cf368ab9
13 changed files with 247 additions and 365 deletions
Show Stats Download Patch File Download Diff File

4
Makefile
Unescape View File

@ -256,6 +256,8 @@ ifeq ($(BUILD_C_ANALYZERS),yes)
test -d $(DESTDIR)$(libdir)/infer/$$i || \ test -d $(DESTDIR)$(libdir)/infer/$$i || \
$(MKDIR_P) $(DESTDIR)$(libdir)/infer/$$i; \ $(MKDIR_P) $(DESTDIR)$(libdir)/infer/$$i; \
done done
test -d $(DESTDIR)$(libdir)/infer/infer/lib/linter_rules/ || \
$(MKDIR_P) $(DESTDIR)$(libdir)/infer/infer/lib/linter_rules
endif endif
ifeq ($(BUILD_JAVA_ANALYZERS),yes) ifeq ($(BUILD_JAVA_ANALYZERS),yes)
test -d $(DESTDIR)$(libdir)/infer/infer/lib/java/ || \ test -d $(DESTDIR)$(libdir)/infer/infer/lib/java/ || \
@ -302,6 +304,8 @@ ifeq ($(BUILD_C_ANALYZERS),yes)
@for i in $$(find infer/models/cpp/include/ -not -type d); do \ @for i in $$(find infer/models/cpp/include/ -not -type d); do \
$(INSTALL_DATA) -C $$i $(DESTDIR)$(libdir)/infer/$$i; \ $(INSTALL_DATA) -C $$i $(DESTDIR)$(libdir)/infer/$$i; \
done done
$(INSTALL_DATA) -C infer/lib/linter_rules/linters.al \
$(DESTDIR)$(libdir)/infer/infer/lib/linter_rules/linters.al
$(INSTALL_PROGRAM) -C $(INFERCLANG_BIN) $(DESTDIR)$(libdir)/infer/infer/bin/ $(INSTALL_PROGRAM) -C $(INFERCLANG_BIN) $(DESTDIR)$(libdir)/infer/infer/bin/
(cd $(DESTDIR)$(libdir)/infer/infer/bin/ && \ (cd $(DESTDIR)$(libdir)/infer/infer/bin/ && \
$(LN_S) -f InferClang InferClang++) $(LN_S) -f InferClang InferClang++)

69
infer/src/clang/linter_rules/linters.al → infer/lib/linter_rules/linters.al
Unescape View File

@ -40,13 +40,13 @@ DEFINE-CHECKER ASSIGN_POINTER_WARNING = {
// Fires whenever a NSNumber is dangerously coerced to a boolean in a comparison // Fires whenever a NSNumber is dangerously coerced to a boolean in a comparison
DEFINE-CHECKER BAD_POINTER_COMPARISON = { DEFINE-CHECKER BAD_POINTER_COMPARISON = {
LET is_binop = is_stmt(BinaryOperator); LET is_binop = in_node(BinaryOperator);
LET is_binop_eq = is_binop_with_kind(EQ); LET is_binop_eq = is_binop_with_kind(EQ);
LET is_binop_ne = is_binop_with_kind(NE); LET is_binop_ne = is_binop_with_kind(NE);
LET is_binop_neq = is_binop_eq OR is_binop_ne; LET is_binop_neq = is_binop_eq OR is_binop_ne;
LET is_unop_lnot = is_unop_with_kind(LNot); LET is_unop_lnot = is_unop_with_kind(LNot);
LET is_implicit_cast_expr = is_stmt(ImplicitCastExpr); LET is_implicit_cast_expr = in_node(ImplicitCastExpr);
LET is_expr_with_cleanups = is_stmt(ExprWithCleanups); LET is_expr_with_cleanups = in_node(ExprWithCleanups);
LET is_nsnumber = isa(NSNumber); LET is_nsnumber = isa(NSNumber);
LET eu =( LET eu =(
@ -135,7 +135,7 @@ DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = {
}; };
DEFINE-CHECKER strong_delegate_warning = { DEFINE-CHECKER STRONG_DELEGATE_WARNING = {
LET name_contains_delegate = property_name_contains_word(delegate); LET name_contains_delegate = property_name_contains_word(delegate);
LET name_does_not_contains_queue = NOT property_name_contains_word(queue); LET name_does_not_contains_queue = NOT property_name_contains_word(queue);
@ -150,17 +150,17 @@ DEFINE-CHECKER strong_delegate_warning = {
}; };
DEFINE-CHECKER global_var_init_with_calls_warning = { DEFINE-CHECKER GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL = {
LET is_global_var = LET is_global_var =
is_objc_extension() AND is_global_var() AND (NOT is_const_var()); is_objc_extension() AND is_global_var() AND (NOT is_const_var());
LET makes_an_expensive_call = LET makes_an_expensive_call =
(is_stmt(CallExpr) AND NOT call_function_named(CGPointMake)) (in_node(CallExpr) AND NOT call_function_named(CGPointMake))
OR is_stmt(CXXTemporaryObjectExpr) OR in_node(CXXTemporaryObjectExpr)
OR is_stmt(CXXMemberCallExpr) OR in_node(CXXMemberCallExpr)
OR is_stmt(CXXOperatorCallExpr) OR in_node(CXXOperatorCallExpr)
OR is_stmt(ObjCMessageExpr); OR in_node(ObjCMessageExpr);
LET is_initialized_with_expensive_call = LET is_initialized_with_expensive_call =
IN-NODE VarDecl WITH-TRANSITION InitExpr IN-NODE VarDecl WITH-TRANSITION InitExpr
@ -179,30 +179,43 @@ DEFINE-CHECKER global_var_init_with_calls_warning = {
}; };
DEFINE-CHECKER ctl_captured_cxx_ref_in_objc_block_warning = { DEFINE-CHECKER CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK = {
SET report_when = SET report_when =
WHEN WHEN
captures_cxx_references() ((in_node(BlockDecl) AND captures_cxx_references())
HOLDS-IN-NODE BlockDecl; HOLDS-NEXT)
HOLDS-IN-NODE BlockExpr;
// * Alternative ways of writing this check:
// SET report_when =
// WHEN
// captures_cxx_references()
// HOLDS-IN-NODE BlockDecl;
//
// SET report_when =
// in_node(BlockDecl) AND captures_cxx_references();
SET message = SET message =
"C++ Reference variable(s) %var_name% captured by Objective-C block"; "C++ Reference variable(s) %cxx_ref_captured_in_block% captured by Objective-C block";
SET suggestion = "C++ References are unmanaged and may be invalid by the time the block executes."; SET suggestion = "C++ References are unmanaged and may be invalid by the time the block executes.";
}; };
DEFINE-CHECKER ctl_unavailable_api_in_supported_ios_sdk_error = { //
SET report_when = // ** Commented for the moment. We use the hardcoded version
WHEN //
WITH-TRANSITION PointerToDecl decl_unavailable_in_supported_ios_sdk // DEFINE-CHECKER ctl_unavailable_api_in_supported_ios_sdk_error = {
HOLDS-IN-NODE DeclRefExpr, ObjCMessageExpr; // SET report_when =
// WHEN
SET message = // WITH-TRANSITION PointerToDecl decl_unavailable_in_supported_ios_sdk
"%decl_ref_or_selector_name% is available only starting \ // HOLDS-IN-NODE DeclRefExpr, ObjCMessageExpr;
from ios sdk %available_ios_sdk% but we support earlier versions from \ //
ios sdk %iphoneos_target_sdk_version%; // SET message =
// "%decl_ref_or_selector_name% is available only starting \
SET suggestion = "This could cause a crash."; // from ios sdk %available_ios_sdk% but we support earlier versions from \
// ios sdk %iphoneos_target_sdk_version%;
}; //
// SET suggestion = "This could cause a crash.";
//
// };

9
infer/src/base/Config.ml
Unescape View File

@ -270,6 +270,10 @@ let cpp_extra_include_dir = models_src_dir ^/ relative_cpp_extra_include_dir
let relative_cpp_models_dir = let relative_cpp_models_dir =
relative_cpp_extra_include_dir ^/ "infer_model" relative_cpp_extra_include_dir ^/ "infer_model"
let linters_def_dir = lib_dir ^/ "linter_rules"
let linters_def_default_file = linters_def_dir ^/ "linters.al"
let wrappers_dir = let wrappers_dir =
lib_dir ^/ "wrappers" lib_dir ^/ "wrappers"
@ -871,8 +875,9 @@ and latex =
"Write a latex report of the analysis results to a file" "Write a latex report of the analysis results to a file"
and linters_def_file = and linters_def_file =
CLOpt.mk_path_opt ~long:"linters-def-file" ~exes:CLOpt.[Clang] CLOpt.mk_path_list ~default: [linters_def_default_file]
~meta:"file" "Specify the file containing linters definition" ~long:"linters-def-file" ~exes:CLOpt.[Clang]
~meta:"file" "Specify the file containing linters definition (e.g. 'linters.al')"
and load_average = and load_average =
CLOpt.mk_float_opt ~long:"load-average" ~short:"l" CLOpt.mk_float_opt ~long:"load-average" ~short:"l"

2
infer/src/base/Config.mli
Unescape View File

@ -213,7 +213,7 @@ val javac_verbose_out : string
val jobs : int val jobs : int
val join_cond : int val join_cond : int
val latex : string option val latex : string option
val linters_def_file : string option val linters_def_file : string list
val load_analysis_results : string option val load_analysis_results : string option
val makefile_cmdline : string val makefile_cmdline : string
val merge : bool val merge : bool

207
infer/src/clang/cFrontend_checkers.ml
Unescape View File

@ -89,215 +89,16 @@ let ivar_name an =
| _ -> "") | _ -> "")
| _ -> "" | _ -> ""
let var_name an = let cxx_ref_captured_in_block an =
let capt_refs = match an with let capt_refs = match an with
| CTL.Stmt (Clang_ast_t.BlockExpr (_, _ , _, decl)) -> | CTL.Decl d -> Predicates.captured_variables_cxx_ref d
Predicates.captured_variables_cxx_ref decl | CTL.Stmt (Clang_ast_t.BlockExpr(_, _, _, d)) ->
Predicates.captured_variables_cxx_ref d
| _ -> [] in | _ -> [] in
let var_desc vars var_named_decl_info = let var_desc vars var_named_decl_info =
vars ^ "'" ^ var_named_decl_info.Clang_ast_t.ni_name ^ "'" in vars ^ "'" ^ var_named_decl_info.Clang_ast_t.ni_name ^ "'" in
IList.fold_left var_desc "" capt_refs IList.fold_left var_desc "" capt_refs
(* (is_CallExpr /\ not call_function_named) ||
is_CXXTemporaryObjectExpr || is_CXXMemberCallExpr
|| is_CXXOperatorCallExpr || is_ObjCMessageExpr *)
let ctl_makes_an_expensive_call () =
let open CTL in
let white_list_functions = ["CGPointMake"] in
Or (Or (Or (Or (And (Atomic ("in_node", ["CallExpr"]),
Not(Atomic("call_function_named", white_list_functions))),
Atomic ("in_node", ["CXXTemporaryObjectExpr"])),
Atomic ("in_node", ["CXXMemberCallExpr"])),
Atomic ("in_node", ["CXXOperatorCallExpr"])),
Atomic ("in_node", ["ObjCMessageExpr"]))
(*
ET([ObjCMethodDecl][->Body] (EF call_addObserver
Or EF call_addObserverForName)
=>
ET([ObjCImplementationDecl,ObjCProtocolDecl][->]
ET([ObjCMethodDecl][->Body] EF remove_observer) Or
EH([ObjCImplementationDecl, ObjCProtocolDecl] EF remove_observer)
*)
let ctl_ns_notification_warning lctx an =
let open CTL in
let exists_method_calling_addObserver =
EF (None, (Atomic ("call_method", ["addObserver:selector:name:object:"]))) in
let exists_method_calling_addObserverForName =
EF (None, (Atomic ("call_method", ["addObserverForName:object:queue:usingBlock:"]))) in
let add_observer = Or (exists_method_calling_addObserver,
exists_method_calling_addObserverForName) in
let eventually_addObserver = ET(["ObjCMethodDecl"], Some Body, add_observer) in
let exists_method_calling_removeObserver =
EF (None, (Atomic ("call_method", ["removeObserver:"]))) in
let exists_method_calling_removeObserverName =
EF (None, (Atomic ("call_method", ["removeObserver:name:object:"]))) in
let remove_observer = Or(exists_method_calling_removeObserver,
exists_method_calling_removeObserverName) in
let remove_observer_in_block = ET(["BlockDecl"], Some Body, remove_observer) in
let remove_observer' = Or(remove_observer, remove_observer_in_block) in
let remove_observer_in_method = ET(["ObjCMethodDecl"], Some Body, remove_observer') in
let eventually_removeObserver =
ET(["ObjCImplementationDecl"; "ObjCProtocolDecl"], None,
Or(remove_observer_in_method ,
EH(["ObjCImplementationDecl"; "ObjCProtocolDecl"], remove_observer_in_method))) in
let condition = InNode (["ObjCImplementationDecl"; "ObjCProtocolDecl"],
Not (Implies (eventually_addObserver, eventually_removeObserver))) in
let issue_desc = {
CIssue.name = "REGISTERED_OBSERVER_BEING_DEALLOCATED";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description =
"Object self is registered in a notification center but not being removed before deallocation";
suggestion =
Some "Consider removing the object from the notification center before its deallocation.";
loc = location_from_an lctx an;
} in
condition, Some issue_desc
(* BAD_POINTER_COMPARISON: Fires whenever a NSNumber is dangerously coerced to
a boolean in a comparison *)
let ctl_bad_pointer_comparison_warning lctx an =
let open CTL in
let is_binop = Atomic ("in_node", ["BinaryOperator"]) in
let is_binop_eq = Atomic ("is_binop_with_kind", ["EQ"]) in
let is_binop_ne = Atomic ("is_binop_with_kind", ["NE"]) in
let is_binop_neq = Or (is_binop_eq, is_binop_ne) in
let is_unop_lnot = Atomic ("is_unop_with_kind", ["LNot"]) in
let is_implicit_cast_expr = Atomic ("in_node", ["ImplicitCastExpr"]) in
let is_expr_with_cleanups = Atomic ("in_node", ["ExprWithCleanups"]) in
let is_nsnumber = Atomic ("isa", ["NSNumber"]) in
(*
NOT is_binop_neq AND
(is_expr_with_cleanups OR is_implicit_cast_expr OR is_binop OR is_unop_lnot)
UNTIL is_nsnumber
*)
let p = Or (is_expr_with_cleanups, Or (is_implicit_cast_expr, Or (is_binop, is_unop_lnot))) in
let p' = And (Not is_binop_neq, p) in
let etx = ETX (["IfStmt"; "ForStmt"; "WhileStmt"; "ConditionalOperator"], Some Cond,
EU (None, p', is_nsnumber)) in
let condition = InNode (["IfStmt"; "ForStmt"; "WhileStmt"; "ConditionalOperator"], etx) in
let issue_desc =
{ CIssue.
name = "BAD_POINTER_COMPARISON";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description = "Implicitly checking whether NSNumber pointer is nil";
suggestion =
Some ("Did you mean to compare against the unboxed value instead? " ^
"Please either explicitly compare the NSNumber instance to nil, " ^
"or use one of the NSNumber accessors before the comparison.");
loc = location_from_an lctx an
} in
condition, Some issue_desc
(* name_contains_delegate AND not name_contains_queue AND is_strong_property *)
let ctl_strong_delegate_warning lctx an =
let open CTL in
let name_contains_delegate =
Atomic ("property_name_contains_word", ["delegate"]) in
let name_does_not_contains_queue =
Not(Atomic ("property_name_contains_word", ["queue"])) in
let is_strong_property =
Atomic("is_strong_property", []) in
let condition = InNode (["ObjCPropertyDecl"], And (name_contains_delegate,
And (name_does_not_contains_queue,
is_strong_property))) in
let issue_desc = {
CIssue.name = "STRONG_DELEGATE_WARNING";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description =
"Property or ivar %decl_name% declared strong";
suggestion = Some "In general delegates should be declared weak or assign";
loc = location_from_an lctx an
} in
condition, Some issue_desc
(* (is_ObjC || is_Objc++) /\ is_global_var /\ not is_const_var /\
ET([VarDecl][->InitExpr] EF ctl_makes_an_expensive_call)
*)
let ctl_global_var_init_with_calls_warning lctx an =
let open CTL in
let ctl_is_global_var =
And (And (Atomic ("is_objc_extension", []), Atomic ("is_global_var", [])),
Not (Atomic ("is_const_var", []))) in
let ctl_is_initialized_with_expensive_call =
ET(["VarDecl"], Some InitExpr, EF (None, (ctl_makes_an_expensive_call ()))) in
let condition =
InNode (["VarDecl"], And (ctl_is_global_var, ctl_is_initialized_with_expensive_call)) in
let issue_desc = {
CIssue.name = "GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description =
"Global variable %decl_name% is initialized using a function or method call";
suggestion = Some
"If the function/method call is expensive, it can affect the starting time of the app.";
loc = location_from_an lctx an
} in
condition, Some issue_desc
(* is_assign_property AND is_property_pointer_type *)
let ctl_assign_pointer_warning lctx an =
let open CTL in
let condition = InNode(["ObjCPropertyDecl"],
And (Atomic ("is_assign_property", []),
Atomic ("is_property_pointer_type", []))) in
let issue_desc =
{ CIssue.name = "ASSIGN_POINTER_WARNING";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description =
"Property `%decl_name%` is a pointer type marked with the `assign` attribute";
suggestion = Some "Use a different attribute like `strong` or `weak`.";
loc = location_from_an lctx an
} in
condition, Some issue_desc
(*
not context_in_synchronized_block /\ not is_method_property_accessor_of_ivar
/\ not is_objc_constructor /\ not is_objc_dealloc
*)
let ctl_direct_atomic_property_access_warning lctx an =
let open CTL in
let condition = InNode (["ObjCIvarRefExpr"],
And (And (And (And (Not (Atomic ("context_in_synchronized_block", [])),
Atomic("is_ivar_atomic", [])),
Not (Atomic ("is_method_property_accessor_of_ivar", []))),
Not (Atomic ("is_objc_constructor", []))),
Not (Atomic ("is_objc_dealloc", [])))) in
let issue_desc = {
CIssue.name = "DIRECT_ATOMIC_PROPERTY_ACCESS";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description = "Direct access to ivar %ivar_name% of an atomic property";
suggestion =
Some "Accessing an ivar of an atomic property makes the property nonatomic";
loc = location_from_an lctx an
} in
condition, Some issue_desc
let ctl_captured_cxx_ref_in_objc_block_warning lctx an =
(* Fire if the list of captured references is not empty *)
let open CTL in
let condition = InNode (["BlockDecl"], Atomic ("captures_cxx_references", [])) in
let issue_desc = {
CIssue.name = "CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK";
severity = Exceptions.Kwarning;
mode = CIssue.On;
description =
"C++ Reference variable(s) %var_name% captured by Objective-C block";
suggestion = Some ("C++ References are unmanaged and may be invalid " ^
"by the time the block executes.");
loc = match an with
| Stmt (Clang_ast_t.BlockExpr (_, _ , _, decl)) -> location_from_an lctx (Decl decl)
| _ -> location_from_an lctx an;
} in
condition, Some issue_desc
(** If the declaration has avilability attributes, check that it's compatible with (** If the declaration has avilability attributes, check that it's compatible with
the iphoneos_target_sdk_version *) the iphoneos_target_sdk_version *)
let ctl_unavailable_api_in_supported_ios_sdk_error lctx an = let ctl_unavailable_api_in_supported_ios_sdk_error lctx an =

44
infer/src/clang/cFrontend_checkers.mli
Unescape View File

@ -9,52 +9,18 @@
open! IStd open! IStd
(* === Warnings on properties === *)
(* Strong Delegate Warning: a property with name delegate should not be declared strong *)
val ctl_strong_delegate_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
(* Assing Pointer Warning: a property with a pointer type should not be declared `assign` *)
val ctl_assign_pointer_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
(* Direct Atomic Property access:
a property declared atomic should not be accesses directly via its iva *)
val ctl_direct_atomic_property_access_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
(* CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK: C++ references
should not be captured in blocks. *)
val ctl_captured_cxx_ref_in_objc_block_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
(** Unavailable_api_in_supported_os_error :
If the declaration has avilability attributes, check that it's compatible with
the iphoneos_target_sdk_version *)
val ctl_unavailable_api_in_supported_ios_sdk_error : val ctl_unavailable_api_in_supported_ios_sdk_error :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
val ctl_bad_pointer_comparison_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
(* REGISTERED_OBSERVER_BEING_DEALLOCATED: an object is registered in a notification center
but not removed before deallocation *)
val ctl_ns_notification_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
(* GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL warning: a global variable initialization should not *)
(* contain calls to functions or methods as these can be expensive an delay the starting time *)
(* of a program *)
val ctl_global_var_init_with_calls_warning :
CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
val location_from_stmt : val location_from_stmt :
CLintersContext.context -> Clang_ast_t.stmt -> Location.t CLintersContext.context -> Clang_ast_t.stmt -> Location.t
val location_from_dinfo : val location_from_dinfo :
CLintersContext.context -> Clang_ast_t.decl_info -> Location.t CLintersContext.context -> Clang_ast_t.decl_info -> Location.t
val location_from_an :
CLintersContext.context -> CTL.ast_node -> Location.t
val location_from_decl : val location_from_decl :
CLintersContext.context -> Clang_ast_t.decl -> Location.t CLintersContext.context -> Clang_ast_t.decl -> Location.t
@ -62,10 +28,12 @@ val decl_name : CTL.ast_node -> string
val ivar_name : CTL.ast_node -> string val ivar_name : CTL.ast_node -> string
val var_name : CTL.ast_node -> string val cxx_ref_captured_in_block : CTL.ast_node -> string
val decl_ref_or_selector_name : CTL.ast_node -> string val decl_ref_or_selector_name : CTL.ast_node -> string
val iphoneos_target_sdk_version : CTL.ast_node -> string val iphoneos_target_sdk_version : CTL.ast_node -> string
val available_ios_sdk : CTL.ast_node -> string val available_ios_sdk : CTL.ast_node -> string
val tag_name_of_node : CTL.ast_node -> string

17
infer/src/clang/cFrontend_checkers_main.ml
Unescape View File

@ -12,7 +12,9 @@ open CFrontend_utils
open Lexing open Lexing
open Ctl_lexer open Ctl_lexer
let parse_ctl_file filename = (* Parse the file with linters definitions, and it returns a list
of checkers in the form of pairs (condition, issue_desc) *)
let parse_ctl_file linters_files =
let print_position _ lexbuf = let print_position _ lexbuf =
let pos = lexbuf.lex_curr_p in let pos = lexbuf.lex_curr_p in
Logging.err "%s:%d:%d" pos.pos_fname Logging.err "%s:%d:%d" pos.pos_fname
@ -25,21 +27,20 @@ let parse_ctl_file filename =
| Ctl_parser.Error -> | Ctl_parser.Error ->
Logging.err "%a: syntax error\n" print_position lexbuf; Logging.err "%a: syntax error\n" print_position lexbuf;
exit (-1) in exit (-1) in
match filename with IList.iter (fun fn ->
| Some fn -> Logging.out "Loading linters rules from %s\n" fn;
let inx = open_in fn in let inx = open_in fn in
let lexbuf = Lexing.from_channel inx in let lexbuf = Lexing.from_channel inx in
lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fn }; lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fn };
(match parse_with_error lexbuf with (match parse_with_error lexbuf with
| Some parsed_checkers -> | Some parsed_checkers ->
Logging.out "#### Start Expanding checkers #####\n"; Logging.out "#### Start Expanding checkers #####\n";
let checkers = CFrontend_errors.expand_checkers parsed_checkers in let exp_checkers = CFrontend_errors.expand_checkers parsed_checkers in
Logging.out "#### Checkers Expanded #####\n"; Logging.out "#### Checkers Expanded #####\n";
IList.iter Ctl_parser_types.print_checker checkers if Config.debug_mode then IList.iter Ctl_parser_types.print_checker exp_checkers;
CFrontend_errors.make_condition_issue_desc_pair exp_checkers;
| None -> Logging.out "No linters found.\n"); | None -> Logging.out "No linters found.\n");
In_channel.close inx In_channel.close inx) linters_files
| None ->
Logging.out "No linters file specified. Nothing to parse.\n"
let rec do_frontend_checks_stmt (context:CLintersContext.context) stmt = let rec do_frontend_checks_stmt (context:CLintersContext.context) stmt =

118
infer/src/clang/cFrontend_errors.ml
Unescape View File

@ -17,14 +17,11 @@ let single_to_multi checker =
(condition, Option.to_list issue_desc_opt) (condition, Option.to_list issue_desc_opt)
(* List of checkers on decls *that return 0 or 1 issue* *) (* List of checkers on decls *that return 0 or 1 issue* *)
let decl_single_checkers_list = [CFrontend_checkers.ctl_strong_delegate_warning; let decl_single_checkers_list =
CFrontend_checkers.ctl_assign_pointer_warning; [ComponentKit.component_with_unconventional_superclass_advice;
CFrontend_checkers.ctl_ns_notification_warning; ComponentKit.mutable_local_vars_advice;
CFrontend_checkers.ctl_global_var_init_with_calls_warning; ComponentKit.component_factory_function_advice;
ComponentKit.component_with_unconventional_superclass_advice; ComponentKit.component_file_cyclomatic_complexity_info;]
ComponentKit.mutable_local_vars_advice;
ComponentKit.component_factory_function_advice;
ComponentKit.component_file_cyclomatic_complexity_info;]
(* List of checkers on decls *) (* List of checkers on decls *)
let decl_checkers_list = let decl_checkers_list =
@ -32,23 +29,25 @@ let decl_checkers_list =
(IList.map single_to_multi decl_single_checkers_list) (IList.map single_to_multi decl_single_checkers_list)
(* List of checkers on stmts *that return 0 or 1 issue* *) (* List of checkers on stmts *that return 0 or 1 issue* *)
let stmt_single_checkers_list = [CFrontend_checkers.ctl_direct_atomic_property_access_warning; let stmt_single_checkers_list =
CFrontend_checkers.ctl_captured_cxx_ref_in_objc_block_warning; [ComponentKit.component_file_cyclomatic_complexity_info;
CFrontend_checkers.ctl_bad_pointer_comparison_warning; ComponentKit.component_initializer_with_side_effects_advice;
ComponentKit.component_file_cyclomatic_complexity_info; CFrontend_checkers.ctl_unavailable_api_in_supported_ios_sdk_error;]
ComponentKit.component_initializer_with_side_effects_advice;
CFrontend_checkers.ctl_unavailable_api_in_supported_ios_sdk_error;]
let stmt_checkers_list = IList.map single_to_multi stmt_single_checkers_list let stmt_checkers_list = IList.map single_to_multi stmt_single_checkers_list
(* List of checkers on translation unit that potentially output multiple issues *) (* List of checkers on translation unit that potentially output multiple issues *)
let translation_unit_checkers_list = [ComponentKit.component_file_line_count_info;] let translation_unit_checkers_list = [ComponentKit.component_file_line_count_info;]
(* List of checkers that will be filled after parsing them from a file *)
let checkers_decl_stmt = ref []
let evaluate_place_holder ph an = let evaluate_place_holder ph an =
match ph with match ph with
| "%ivar_name%" -> CFrontend_checkers.ivar_name an | "%ivar_name%" -> CFrontend_checkers.ivar_name an
| "%decl_name%" -> CFrontend_checkers.decl_name an | "%decl_name%" -> CFrontend_checkers.decl_name an
| "%var_name%" -> CFrontend_checkers.var_name an | "%cxx_ref_captured_in_block%" ->
CFrontend_checkers.cxx_ref_captured_in_block an
| "%decl_ref_or_selector_name%" -> | "%decl_ref_or_selector_name%" ->
CFrontend_checkers.decl_ref_or_selector_name an CFrontend_checkers.decl_ref_or_selector_name an
| "%iphoneos_target_sdk_version%" -> | "%iphoneos_target_sdk_version%" ->
@ -78,6 +77,57 @@ let rec expand_message_string message an =
expand_message_string message' an expand_message_string message' an
with Not_found -> message with Not_found -> message
let string_to_err_kind = function
| "WARNING" -> Exceptions.Kwarning
| "ERROR" -> Exceptions.Kerror
| "INFO" -> Exceptions.Kinfo
| "ADVICE" -> Exceptions.Kadvice
| s -> (Logging.err "\n[ERROR] Severity %s does not exist. Stop.\n" s;
assert false)
let string_to_issue_mode m =
match m with
| "ON" -> CIssue.On
| "OFF" -> CIssue.Off
| s ->
(Logging.err "\n[ERROR] Mode %s does not exist. Please specify ON/OFF\n" s;
assert false)
(** Convert a parsed checker in a pair (condition, issue_desc) *)
let make_condition_issue_desc_pair checkers =
let open CIssue in
let open Ctl_parser_types in
Logging.out "\n Converting checkers in (condition, issue) pairs\n";
let do_one_checker c =
let dummy_issue = {
name = c.Ctl_parser_types.name;
description = "";
suggestion = None;
loc = Location.dummy;
severity = Exceptions.Kwarning;
mode = CIssue.On;
} in
let issue, condition = IList.fold_left (fun (issue', cond') d ->
match d with
| CSet (s, phi) when String.equal s report_when_const ->
issue', phi
| CDesc (s, msg) when String.equal s message_const ->
{issue' with description = msg}, cond'
| CDesc (s, sugg) when String.equal s suggestion_const ->
{issue' with suggestion = Some sugg}, cond'
| CDesc (s, sev) when String.equal s severity_const ->
{issue' with severity = string_to_err_kind sev}, cond'
| CDesc (s, m) when String.equal s mode_const ->
{issue' with mode = string_to_issue_mode m }, cond'
| _ -> issue', cond') (dummy_issue, CTL.False) c.Ctl_parser_types.definitions in
if Config.debug_mode then (
Logging.out "\nMaking condition and issue desc for checker '%s'\n"
c.Ctl_parser_types.name;
Logging.out "\nCondition =\n %a\n" CTL.Debug.pp_formula condition;
Logging.out "\nIssue_desc = %a\n" CIssue.pp_issue issue);
condition, issue in
checkers_decl_stmt := IList.map do_one_checker checkers
(* expands use of let defined formula id in checkers with their definition *) (* expands use of let defined formula id in checkers with their definition *)
let expand_checkers checkers = let expand_checkers checkers =
@ -91,9 +141,8 @@ let expand_checkers checkers =
Logging.out " -Expanding formula identifier '%s'\n" name; Logging.out " -Expanding formula identifier '%s'\n" name;
(match Core.Std.String.Map.find map name with (match Core.Std.String.Map.find map name with
| Some f1 -> expand f1 map | Some f1 -> expand f1 map
| None -> | None -> failwith
Logging.out "[ERROR]: Formula identifier '%s' is undefined. Cannot expand." name; ("[ERROR]: Formula identifier '" ^ name ^ "' is undefined. Cannot expand."));
assert false);
| Atomic _ -> acc | Atomic _ -> acc
| Not f1 -> Not (expand f1 map) | Not f1 -> Not (expand f1 map)
| And (f1, f2) -> And (expand f1 map, expand f2 map) | And (f1, f2) -> And (expand f1 map, expand f2 map)
@ -148,7 +197,15 @@ let log_frontend_issue translation_unit_context method_decl_opt key issue_desc =
Reporting.log_issue_from_errlog err_kind errlog exn ~loc ~ltr:trace Reporting.log_issue_from_errlog err_kind errlog exn ~loc ~ltr:trace
~node_id:(0, key) ~node_id:(0, key)
let invoke_set_of_checkers_an an context = let fill_issue_desc_info_and_log context an key issue_desc loc =
let desc = expand_message_string issue_desc.CIssue.description an in
let issue_desc' =
{issue_desc with CIssue.description = desc; CIssue.loc = loc } in
log_frontend_issue context.CLintersContext.translation_unit_context
context.CLintersContext.current_method key issue_desc'
(* Calls the set of hard coded checkers (if any) *)
let invoke_set_of_hard_coded_checkers_an an context =
let checkers, key = match an with let checkers, key = match an with
| CTL.Decl dec -> decl_checkers_list, Ast_utils.generate_key_decl dec | CTL.Decl dec -> decl_checkers_list, Ast_utils.generate_key_decl dec
| CTL.Stmt st -> stmt_checkers_list, Ast_utils.generate_key_stmt st in | CTL.Stmt st -> stmt_checkers_list, Ast_utils.generate_key_stmt st in
@ -157,13 +214,28 @@ let invoke_set_of_checkers_an an context =
if CTL.eval_formula condition an context then if CTL.eval_formula condition an context then
IList.iter (fun issue_desc -> IList.iter (fun issue_desc ->
if CIssue.should_run_check issue_desc.CIssue.mode then if CIssue.should_run_check issue_desc.CIssue.mode then
let desc' = expand_message_string issue_desc.CIssue.description an in let loc = issue_desc.CIssue.loc in
let issue_desc' = {issue_desc with CIssue.description = desc'} in fill_issue_desc_info_and_log context an key issue_desc loc
log_frontend_issue context.CLintersContext.translation_unit_context
context.CLintersContext.current_method key issue_desc'
) issue_desc_list ) issue_desc_list
) checkers ) checkers
(* Calls the set of checkers parsed from files (if any) *)
let invoke_set_of_parsed_checkers_an an context =
let key = match an with
| CTL.Decl dec -> Ast_utils.generate_key_decl dec
| CTL.Stmt st -> Ast_utils.generate_key_stmt st in
IList.iter (fun (condition, issue_desc) ->
if CIssue.should_run_check issue_desc.CIssue.mode &&
CTL.eval_formula condition an context then
let loc = CFrontend_checkers.location_from_an context an in
fill_issue_desc_info_and_log context an key issue_desc loc
) !checkers_decl_stmt
(* We decouple the hardcoded checkers from the parsed ones *)
let invoke_set_of_checkers_an an context =
invoke_set_of_parsed_checkers_an an context;
invoke_set_of_hard_coded_checkers_an an context
let run_frontend_checkers_on_an (context: CLintersContext.context) an = let run_frontend_checkers_on_an (context: CLintersContext.context) an =
let open Clang_ast_t in let open Clang_ast_t in

3
infer/src/clang/cFrontend_errors.mli
Unescape View File

@ -23,3 +23,6 @@ val run_translation_unit_checker :
CLintersContext.context -> Clang_ast_t.decl -> unit CLintersContext.context -> Clang_ast_t.decl -> unit
val expand_checkers : Ctl_parser_types.ctl_checker list -> Ctl_parser_types.ctl_checker list val expand_checkers : Ctl_parser_types.ctl_checker list -> Ctl_parser_types.ctl_checker list
val make_condition_issue_desc_pair :
Ctl_parser_types.ctl_checker list -> unit

16
infer/src/clang/cIssue.ml
Unescape View File

@ -20,6 +20,22 @@ type issue_desc = {
loc : Location.t; (* location in the code *) loc : Location.t; (* location in the code *)
} }
let string_of_mode m =
match m with
| On -> "On"
| Off -> "Off"
let pp_issue fmt issue =
Format.fprintf fmt "{\n Name = %s\n" (issue.name);
Format.fprintf fmt " Severity = %s \n" (Exceptions.err_kind_string issue.severity);
Format.fprintf fmt " Mode = %s \n" (string_of_mode issue.mode);
Format.fprintf fmt " Descrption = %s \n" issue.description;
(match issue.suggestion with
| Some s -> Format.fprintf fmt " Suggestion = %s\n" s
| _ -> ());
Format.fprintf fmt " Loc = %s \n" (Location.to_string issue.loc);
Format.fprintf fmt "}\n"
let should_run_check mode = let should_run_check mode =
match mode with match mode with
| On -> true | On -> true

4
infer/src/clang/cIssue.mli
Unescape View File

@ -20,4 +20,8 @@ type issue_desc = {
loc : Location.t; (* location in the code *) loc : Location.t; (* location in the code *)
} }
val string_of_mode : mode -> string
val pp_issue : Format.formatter -> issue_desc -> unit
val should_run_check : mode -> bool val should_run_check : mode -> bool

115
infer/src/clang/cTL.ml
Unescape View File

@ -265,16 +265,24 @@ let save_dotty_when_in_debug_mode source_file =
(* Helper functions *) (* Helper functions *)
(* Sometimes we need to unwrap a node *) let get_successor_nodes an =
(* NOTE: when in the language it will be possible to define (* get_decl_of_stmt get declarations that are directly embedded
sintactic sugar than we can remove this and define it a as immediate children (i.e. distance 1) of an stmt (i.e., no transition).
transition from BlockExpr to BlockDecl *) TBD: check if a dual is needed for get_stmt_of_decl
let unwrap_node an = *)
let get_decl_of_stmt st =
match st with
| Clang_ast_t.BlockExpr (_, _, _, d) -> [Decl d]
| _ -> [] in
match an with match an with
| Stmt BlockExpr(_, _, _, d) -> | Stmt st ->
(* From BlockExpr we jump directly to its BlockDecl *) let _, succs_st = Clang_ast_proj.get_stmt_tuple st in
Decl d let succs = IList.map (fun s -> Stmt s) succs_st in
| _ -> an succs @ (get_decl_of_stmt st)
| Decl dec ->
(match Clang_ast_proj.get_decl_context_tuple dec with
| Some (decl_list, _) -> IList.map (fun d -> Decl d) decl_list
| None -> [])
let node_to_string an = let node_to_string an =
match an with match an with
@ -367,87 +375,67 @@ let next_state_via_transition an trans =
(* evaluate an atomic formula (i.e. a predicate) on a ast node an and a (* evaluate an atomic formula (i.e. a predicate) on a ast node an and a
linter context lcxt. That is: an, lcxt |= pred_name(params) *) linter context lcxt. That is: an, lcxt |= pred_name(params) *)
let eval_Atomic pred_name args an lcxt = let rec eval_Atomic pred_name args an lcxt =
match pred_name, args, an with match pred_name, args, an with
| "call_method", [m], Stmt st -> Predicates.call_method m st | "call_method", [m], Stmt st -> Predicates.call_method m st
(* Note: I think it should be better to change all predicated to be
evaluated in a node an. The predicate itself should decide if it's a
stmt or decl predicate and return false for an unappropriate node *)
| "call_method", _, Decl _ -> false
| "property_name_contains_word", [word], Decl d -> Predicates.property_name_contains_word word d | "property_name_contains_word", [word], Decl d -> Predicates.property_name_contains_word word d
| "property_name_contains_word", _, Stmt _ -> false
| "is_objc_extension", [], _ -> Predicates.is_objc_extension lcxt | "is_objc_extension", [], _ -> Predicates.is_objc_extension lcxt
| "is_global_var", [], Decl d -> Predicates.is_syntactically_global_var d | "is_global_var", [], Decl d -> Predicates.is_syntactically_global_var d
| "is_global_var", _, Stmt _ -> false
| "is_const_var", [], Decl d -> Predicates.is_const_expr_var d | "is_const_var", [], Decl d -> Predicates.is_const_expr_var d
| "is_const_var", _, Stmt _ -> false
| "call_function_named", args, Stmt st -> Predicates.call_function_named args st | "call_function_named", args, Stmt st -> Predicates.call_function_named args st
| "call_function_named", _, Decl _ -> false
| "is_strong_property", [], Decl d -> Predicates.is_strong_property d | "is_strong_property", [], Decl d -> Predicates.is_strong_property d
| "is_strong_property", _, Stmt _ -> false
| "is_assign_property", [], Decl d -> Predicates.is_assign_property d | "is_assign_property", [], Decl d -> Predicates.is_assign_property d
| "is_assign_property", _, Stmt _ -> false
| "is_property_pointer_type", [], Decl d -> Predicates.is_property_pointer_type d | "is_property_pointer_type", [], Decl d -> Predicates.is_property_pointer_type d
| "is_property_pointer_type", _, Stmt _ -> false
| "context_in_synchronized_block", [], _ -> Predicates.context_in_synchronized_block lcxt | "context_in_synchronized_block", [], _ -> Predicates.context_in_synchronized_block lcxt
| "is_ivar_atomic", [], Stmt st -> Predicates.is_ivar_atomic st | "is_ivar_atomic", [], Stmt st -> Predicates.is_ivar_atomic st
| "is_ivar_atomic", _, Decl _ -> false
| "is_method_property_accessor_of_ivar", [], Stmt st -> | "is_method_property_accessor_of_ivar", [], Stmt st ->
Predicates.is_method_property_accessor_of_ivar st lcxt Predicates.is_method_property_accessor_of_ivar st lcxt
| "is_method_property_accessor_of_ivar", _, Decl _ -> false
| "is_objc_constructor", [], _ -> Predicates.is_objc_constructor lcxt | "is_objc_constructor", [], _ -> Predicates.is_objc_constructor lcxt
| "is_objc_dealloc", [], _ -> Predicates.is_objc_dealloc lcxt | "is_objc_dealloc", [], _ -> Predicates.is_objc_dealloc lcxt
| "captures_cxx_references", [], Decl d -> Predicates.captures_cxx_references d | "captures_cxx_references", [], Decl d -> Predicates.captures_cxx_references d
| "captures_cxx_references", _, Stmt _ -> false
| "is_binop_with_kind", [str_kind], Stmt st -> Predicates.is_binop_with_kind str_kind st | "is_binop_with_kind", [str_kind], Stmt st -> Predicates.is_binop_with_kind str_kind st
| "is_binop_with_kind", _, Decl _ -> false
| "is_unop_with_kind", [str_kind], Stmt st -> Predicates.is_unop_with_kind str_kind st | "is_unop_with_kind", [str_kind], Stmt st -> Predicates.is_unop_with_kind str_kind st
| "is_unop_with_kind", _, Decl _ -> false
| "in_node", [nodename], Stmt st -> Predicates.is_stmt nodename st | "in_node", [nodename], Stmt st -> Predicates.is_stmt nodename st
| "in_node", [nodename], Decl d -> Predicates.is_decl nodename d | "in_node", [nodename], Decl d -> Predicates.is_decl nodename d
| "isa", [classname], Stmt st -> Predicates.isa classname st | "isa", [classname], Stmt st -> Predicates.isa classname st
| "isa", _, Decl _ -> false
| "decl_unavailable_in_supported_ios_sdk", [], Decl decl -> | "decl_unavailable_in_supported_ios_sdk", [], Decl decl ->
Predicates.decl_unavailable_in_supported_ios_sdk decl Predicates.decl_unavailable_in_supported_ios_sdk decl
| "decl_unavailable_in_supported_ios_sdk", _, Stmt _ -> false
| _ -> failwith ("ERROR: Undefined Predicate or wrong set of arguments: " ^ pred_name) | _ -> failwith ("ERROR: Undefined Predicate or wrong set of arguments: " ^ pred_name)
(* st, lcxt |= EF phi <=> (* an, lcxt |= EF phi <=>
st, lcxt |= phi or exists st' in Successors(st): st', lcxt |= EF phi an, lcxt |= phi or exists an' in Successors(st): an', lcxt |= EF phi
That is: a (st, lcxt) satifies EF phi if and only if That is: a (an, lcxt) satifies EF phi if and only if
either (st,lcxt) satifies phi or there is a child st' of the node st either (an,lcxt) satifies phi or there is a child an' of the node an
such that (st', lcxt) satifies EF phi such that (an', lcxt) satifies EF phi
*) *)
let rec eval_EF_st phi st lcxt trans =
let _, succs = Clang_ast_proj.get_stmt_tuple st in
eval_formula phi (Stmt st) lcxt
|| IList.exists (fun s -> eval_EF phi (Stmt s) lcxt trans) succs
(* dec, lcxt |= EF phi <=>
dec, lcxt |= phi or exists dec' in Successors(dec): dec', lcxt |= EF phi
This is as eval_EF_st but for decl.
*)
and eval_EF_decl phi dec lcxt trans =
eval_formula phi (Decl dec) lcxt ||
(match Clang_ast_proj.get_decl_context_tuple dec with
| Some (decl_list, _) ->
IList.exists (fun d -> eval_EF phi (Decl d) lcxt trans) decl_list
| None -> false)
(* an, lcxt |= EF phi evaluates on decl or stmt depending on an *)
and eval_EF phi an lcxt trans = and eval_EF phi an lcxt trans =
match trans, an with match trans, an with
| Some _, _ -> | Some _, _ ->
(* Using equivalence EF[->trans] phi = phi OR EX[->trans](EF[->trans] phi)*) (* Using equivalence EF[->trans] phi = phi OR EX[->trans](EF[->trans] phi)*)
let phi' = Or (phi, EX (trans, EF (trans, phi))) in let phi' = Or (phi, EX (trans, EF (trans, phi))) in
eval_formula phi' an lcxt eval_formula phi' an lcxt
| None, Stmt st -> eval_EF_st phi st lcxt trans | None, _ ->
| None, Decl dec -> eval_EF_decl phi dec lcxt trans eval_formula phi an lcxt
|| IList.exists (fun an' -> eval_EF phi an' lcxt trans) (get_successor_nodes an)
(* st, lcxt |= EX phi <=> exists st' in Successors(st): st', lcxt |= phi
That is: a (st, lcxt) satifies EX phi if and only if
there exists is a child st' of the node st
such that (st', lcxt) satifies phi
*)
and eval_EX_st phi st lcxt =
let _, succs = Clang_ast_proj.get_stmt_tuple st in
IList.exists (fun s -> eval_formula phi (Stmt s) lcxt) succs
(* dec, lcxt |= EX phi <=> exists dec' in Successors(dec): dec',lcxt|= phi
Same as eval_EX_st but for decl.
*)
and eval_EX_decl phi dec lcxt =
match Clang_ast_proj.get_decl_context_tuple dec with
| Some (decl_list, _) ->
IList.exists (fun d -> eval_formula phi (Decl d) lcxt) decl_list
| None -> false
(* Evaluate phi on node an' such that an -l-> an'. False if an' does not exists *) (* Evaluate phi on node an' such that an -l-> an'. False if an' does not exists *)
and evaluate_on_transition phi an lcxt l = and evaluate_on_transition phi an lcxt l =
@ -455,13 +443,17 @@ and evaluate_on_transition phi an lcxt l =
| Some succ -> eval_formula phi succ lcxt | Some succ -> eval_formula phi succ lcxt
| None -> false | None -> false
(* an |= EX phi evaluates on decl/stmt depending on the ast_node an *) (* an, lcxt |= EX phi <=> exists an' in Successors(st): an', lcxt |= phi
That is: a (an, lcxt) satifies EX phi if and only if
there exists is a child an' of the node an
such that (an', lcxt) satifies phi
*)
and eval_EX phi an lcxt trans = and eval_EX phi an lcxt trans =
match trans, an with match trans, an with
| Some _, _ -> evaluate_on_transition phi an lcxt trans | Some _, _ -> evaluate_on_transition phi an lcxt trans
| None, Stmt st -> eval_EX_st phi st lcxt | None, _ ->
| None, Decl decl -> eval_EX_decl phi decl lcxt IList.exists (fun an' -> eval_formula phi an' lcxt) (get_successor_nodes an)
(* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence (* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence
an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2))) an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2)))
@ -547,8 +539,7 @@ and eval_formula f an lcxt =
| Implies (f1, f2) -> | Implies (f1, f2) ->
not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt)
| InNode (node_type_list, f1) -> | InNode (node_type_list, f1) ->
let an' = unwrap_node an in in_node node_type_list f1 an lcxt
in_node node_type_list f1 an' lcxt
| AU (f1, f2) -> eval_AU f1 f2 an lcxt | AU (f1, f2) -> eval_AU f1 f2 an lcxt
| EU (trans, f1, f2) -> eval_EU f1 f2 an lcxt trans | EU (trans, f1, f2) -> eval_EU f1 f2 an lcxt trans
| EF (trans, f1) -> eval_EF f1 an lcxt trans | EF (trans, f1) -> eval_EF f1 an lcxt trans

4
infer/src/clang/ctl_parser_types.ml
Unescape View File

@ -41,6 +41,10 @@ type ctl_checker = {
let infer_prefix = "__infer_ctl_" let infer_prefix = "__infer_ctl_"
let formula_id_const = infer_prefix ^ "formula_id__" let formula_id_const = infer_prefix ^ "formula_id__"
let report_when_const = "report_when" let report_when_const = "report_when"
let message_const = "message"
let suggestion_const = "suggestion"
let severity_const = "severity"
let mode_const = "mode"
let print_checker c = let print_checker c =
Logging.out "\n-------------------- \n"; Logging.out "\n-------------------- \n";

Write Preview
Loading…
Cancel
Save