From 8cad1b5e6993ff77f1920421128ef17cf56cc4a8 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Tue, 12 Sep 2017 03:22:50 -0700 Subject: [PATCH] Remove ETX operator from AL Reviewed By: dulmarod Differential Revision: D5804550 fbshipit-source-id: 24f3b7f --- infer/lib/linter_rules/linters.al | 6 ++---- infer/src/clang/cFrontend_errors.ml | 5 +---- infer/src/clang/cTL.ml | 29 +---------------------------- infer/src/clang/cTL.mli | 5 +---- infer/src/clang/ctl_lexer.mll | 1 - infer/src/clang/ctl_parser.mly | 4 ---- 6 files changed, 5 insertions(+), 45 deletions(-) diff --git a/infer/lib/linter_rules/linters.al b/infer/lib/linter_rules/linters.al index 565ab3eb4..fcd208dee 100644 --- a/infer/lib/linter_rules/linters.al +++ b/infer/lib/linter_rules/linters.al @@ -61,10 +61,8 @@ DEFINE-CHECKER BAD_POINTER_COMPARISON = { is_nsnumber ); - LET etx = - IN-EXCLUSIVE-NODE IfStmt, ForStmt, WhileStmt, ConditionalOperator WITH-TRANSITION Cond - (eu) - HOLDS-EVENTUALLY; + LET etx = eu HOLDS-NEXT WITH-TRANSITION Cond; + SET report_when = WHEN diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 405f96bcc..1df8fc5a5 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -261,8 +261,7 @@ let rec apply_substitution f sub = -> EG (trans, apply_substitution f1 sub) | ET (ntl, sw, f1) -> ET (sub_list_param ntl, sw, apply_substitution f1 sub) - | ETX (ntl, sw, f1) - -> ETX (sub_list_param ntl, sw, apply_substitution f1 sub) + let expand_formula phi _map _error_msg = let fail_with_circular_macro_definition name error_msg = @@ -323,8 +322,6 @@ let expand_formula phi _map _error_msg = -> EG (trans, expand f1 map error_msg) | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map error_msg) - | ETX (tl, sw, f1) - -> ETX (tl, sw, expand f1 map error_msg) in expand phi _map _error_msg diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 707773553..58675765e 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -58,7 +58,7 @@ type t = | EU of transitions option * t * t | EH of ALVar.alexp list * t | ET of ALVar.alexp list * transitions option * t - | ETX of ALVar.alexp list * transitions option * t + let has_transition phi = match phi with @@ -81,7 +81,6 @@ let has_transition phi = | EG (trans_opt, _) | EU (trans_opt, _, _) | ET (_, trans_opt, _) - | ETX (_, trans_opt, _) -> Option.is_some trans_opt (* "set" clauses are used for defining mandatory variables that will be used @@ -193,9 +192,6 @@ module Debug = struct | ET (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" (Pp.comma_seq Format.pp_print_string) (nodes_to_string arglist) pp_transition trans pp_formula phi - | ETX (arglist, trans, phi) - -> Format.fprintf fmt "ETX[%a][%a](%a)" (Pp.comma_seq Format.pp_print_string) - (nodes_to_string arglist) pp_transition trans pp_formula phi let pp_ast ~ast_node_to_highlight ?(prettifier= Fn.id) fmt root = let pp_node_info fmt an = @@ -982,27 +978,6 @@ and eval_ET tl trs phi an lcxt = in eval_formula f an lcxt -and eval_ETX tl trs phi an lcxt = - let lcxt', tl' = - match (lcxt.CLintersContext.et_evaluation_node, Ctl_parser_types.ast_node_has_kind tl an) with - | None, true - -> let an_alexp = ALVar.Const (Ctl_parser_types.ast_node_kind an) in - ( { lcxt with - CLintersContext.et_evaluation_node= - Some (Ctl_parser_types.ast_node_unique_string_id an) } - , [an_alexp] ) - | _, _ - -> (lcxt, tl) - in - let f = - match trs with - | Some _ - -> EF (None, InNode (tl', EX (trs, phi))) - | None - -> EF (None, InNode (tl', phi)) - in - eval_formula f an lcxt' - (* Formulas are evaluated on a AST node an and a linter context lcxt *) and eval_formula f an lcxt : Ctl_parser_types.ast_node option = debug_eval_begin (debug_create_payload an f lcxt) ; @@ -1045,7 +1020,5 @@ and eval_formula f an lcxt : Ctl_parser_types.ast_node option = eval_formula (And (f1, EX (trans, EG (trans, f1)))) an lcxt | ET (tl, sw, phi) -> eval_ET tl sw phi an lcxt - | ETX (tl, sw, phi) - -> eval_ETX tl sw phi an lcxt in debug_eval_end res ; res diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 2cf5fb18d..ae1d8dfbd 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -71,10 +71,7 @@ type t = (** ET[T][l] phi <=> there exists a descentant an of the current node such that an is of type in set T making a transition to a node an' via label l, such that in an phi holds. *) - | ETX of ALVar.alexp list * transitions option * t - (** ET[T][l] phi <=> - there exists a descentant an of the current node such that an is of type in set T - making a transition to a node an' via label l, such that in an phi holds. *) + (* "set" clauses are used for defining mandatory variables that will be used by when reporting issues: eg for defining the condition. diff --git a/infer/src/clang/ctl_lexer.mll b/infer/src/clang/ctl_lexer.mll index 9834f683a..1c0842476 100644 --- a/infer/src/clang/ctl_lexer.mll +++ b/infer/src/clang/ctl_lexer.mll @@ -43,7 +43,6 @@ rule token = parse | "HOLDS-EVERYWHERE-ALWAYS" { AG } | "HOLDS-IN-SOME-SUPERCLASS-OF" { EH } | "IN-NODE" { ET } - | "IN-EXCLUSIVE-NODE" { ETX } | "WHEN" { WHEN } | "HOLDS-IN-NODE" { HOLDS_IN_NODE } | "WITH-TRANSITION" {WITH_TRANSITION} diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 53ed5e4aa..61673c887 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -51,7 +51,6 @@ %token LESS_THAN %token GREATER_THAN %token ET -%token ETX %token WITH_TRANSITION %token WHEN %token HOLDS_IN_NODE @@ -280,9 +279,6 @@ formula: | ET node_list WITH_TRANSITION transition_label formula_EF { L.(debug Linters Verbose) "\tParsed ET with transition '%a'@\n" CTL.Debug.pp_transition $4; CTL.ET ($2, $4, $5)} - | ETX node_list WITH_TRANSITION transition_label formula_EF - { L.(debug Linters Verbose) "\tParsed ETX ith transition '%a'@\n" CTL.Debug.pp_transition $4; - CTL.ETX ($2, $4, $5)} | EX WITH_TRANSITION transition_label formula_with_paren { L.(debug Linters Verbose) "\tParsed EX with transition '%a'@\n" CTL.Debug.pp_transition $3; CTL.EX ($3, $4)}