From aa231e51291a25f4194d5427ce05b2566e54d7d1 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Mon, 12 Dec 2016 05:34:34 -0800 Subject: [PATCH] [CTL] Expanding formula id with their definition Summary: In checkers we use "let" clause to define formulas abbreviation. This diff expands the use of such formula id when used. This allows to evaluate the formula. For example. let f = f_def let g = g_def let h = f or g will expand the use of f and g with their definition. Reviewed By: martinoluca Differential Revision: D4299542 fbshipit-source-id: 9d37dd0 --- infer/src/clang/cFrontend_checkers_main.ml | 8 +++- infer/src/clang/cFrontend_errors.ml | 48 +++++++++++++++++++++- infer/src/clang/cFrontend_errors.mli | 2 + infer/src/clang/cTL.ml | 5 ++- infer/src/clang/ctl_parser.mly | 48 +++++++++++----------- infer/src/clang/ctl_parser_types.ml | 17 ++++++++ infer/src/clang/linter_rules/linters.al | 2 +- 7 files changed, 103 insertions(+), 27 deletions(-) diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index 433b8644f..9a58cdc1f 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -30,7 +30,13 @@ let parse_ctl_file filename = let inx = open_in fn in let lexbuf = Lexing.from_channel inx in lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fn }; - let _ = parse_with_error lexbuf in + (match parse_with_error lexbuf with + | Some parsed_checkers -> + Logging.out "#### Start Expanding checkers #####\n"; + let checkers = CFrontend_errors.expand_checkers parsed_checkers in + Logging.out "#### Checkers Expanded #####\n"; + IList.iter Ctl_parser_types.print_checker checkers + | None -> Logging.out "No linters found.\n"); In_channel.close inx | None -> Logging.out "No linters file specified. Nothing to parse.\n" diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 1c748d25e..02f88f514 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -33,7 +33,53 @@ let stmt_checkers_list = [CFrontend_checkers.ctl_direct_atomic_property_access_ let translation_unit_checkers_list = [ComponentKit.component_file_line_count_info;] - +(* expands use of let defined formula id in checkers with their definition *) +let expand_checkers checkers = + let open CTL in + let open Ctl_parser_types in + let rec expand acc map = + match acc with + | True + | False -> acc + | Atomic (name, [p]) when formula_id_const = p -> + Logging.out " -Expanding formula identifier '%s'\n" name; + (match Core.Std.String.Map.find map name with + | Some f1 -> expand f1 map + | None -> + Logging.out "[ERROR]: Formula identifier '%s' is undefined. Cannot expand." name; + assert false); + | Atomic _ -> acc + | Not f1 -> Not (expand f1 map) + | And (f1, f2) -> And (expand f1 map, expand f2 map) + | Or (f1, f2) -> Or (expand f1 map, expand f2 map) + | Implies (f1, f2) -> Implies (expand f1 map, expand f2 map) + | InNode (node_type_list, f1) -> InNode (node_type_list, expand f1 map) + | AU (f1, f2) -> AU (expand f1 map, expand f2 map) + | EU (trans, f1, f2) -> EU (trans, expand f1 map, expand f2 map) + | EF (trans, f1) -> EF (trans, expand f1 map) + | AF f1 -> AF (expand f1 map) + | AG f1 -> AG (expand f1 map) + | EX (trans, f1) -> EX (trans, expand f1 map) + | AX f1 -> AX (expand f1 map) + | EH (cl, f1) -> EH (cl, expand f1 map) + | EG (trans, f1) -> EG (trans, expand f1 map) + | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map) + | ETX (tl, sw, f1) -> ETX (tl, sw, expand f1 map) in + let expand_one_checker c = + Logging.out " +Start expanding %s\n" c.name; + let map : CTL.t Core.Std.String.Map.t = Core.Std.String.Map.empty in + let map = IList.fold_left (fun map' d -> match d with + | CLet (k,formula) -> Core.Std.Map.add map' ~key:k ~data:formula + | _ -> map') map c.Ctl_parser_types.definitions in + let exp_defs = IList.fold_left (fun defs clause -> + match clause with + | CSet (report_when_const, phi) -> + Logging.out " -Expanding report_when\n"; + CSet (report_when_const, expand phi map) :: defs + | cl -> cl :: defs) [] c.definitions in + { c with definitions = exp_defs} in + let expanded_checkers = IList.map expand_one_checker checkers in + expanded_checkers diff --git a/infer/src/clang/cFrontend_errors.mli b/infer/src/clang/cFrontend_errors.mli index 1b26126a8..30ba28717 100644 --- a/infer/src/clang/cFrontend_errors.mli +++ b/infer/src/clang/cFrontend_errors.mli @@ -21,3 +21,5 @@ val run_frontend_checkers_on_an : why special-casing is necessary here. *) val run_translation_unit_checker : CLintersContext.context -> Clang_ast_t.decl -> unit + +val expand_checkers : Ctl_parser_types.ctl_checker list -> Ctl_parser_types.ctl_checker list diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 985f25b78..bec2f061c 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -97,7 +97,10 @@ module Debug = struct | EH (arglist, phi) -> Format.fprintf fmt "EH[%a](%a)" (Pp.comma_seq Format.pp_print_string) arglist pp_formula phi - | ET (arglist, trans, phi) + | ET (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" + (Pp.comma_seq Format.pp_print_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) arglist pp_transition trans diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 13770cd4a..b9327d5af 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -62,21 +62,13 @@ checkers_list: ; checker: - DEFINE_CHECKER IDENTIFIER ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE - { let name = $2 in - let definitions = $5 in - Logging.out "\nParsed checker definition: %s\n" name; - IList.iter (fun d -> (match d with - | Ctl_parser_types.CSet (clause_name, phi) - | Ctl_parser_types.CLet (clause_name, phi) -> - Logging.out " %s= \n %a\n\n" - clause_name CTL.Debug.pp_formula phi - | Ctl_parser_types.CDesc (clause_name, s) -> - Logging.out " %s= \n %s\n\n" clause_name s) - ) definitions; - Logging.out "\n-------------------- \n"; - { name = name; definitions = definitions } - } + DEFINE_CHECKER identifier ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE + { + Logging.out "\nParsed checker definition"; + let c = { name = $2; definitions = $5 } in + print_checker c; + c + } ; clause_list: @@ -85,33 +77,34 @@ clause_list: ; clause: - | SET IDENTIFIER ASSIGNMENT formula + | SET identifier ASSIGNMENT formula { Logging.out "\tParsed set clause\n"; CSet ($2, $4) } - | SET IDENTIFIER ASSIGNMENT STRING + | SET identifier ASSIGNMENT STRING { Logging.out "\tParsed desc clause\n"; CDesc ($2, $4) } - | LET IDENTIFIER ASSIGNMENT formula + | LET identifier ASSIGNMENT formula { Logging.out "\tParsed let clause\n"; CLet ($2, $4) } ; atomic_formula: | TRUE { Logging.out "\tParsed True\n"; CTL.True } | FALSE { Logging.out "\tParsed False\n"; CTL.False } - | IDENTIFIER LEFT_PAREN params RIGHT_PAREN + | identifier LEFT_PAREN params RIGHT_PAREN { Logging.out "\tParsed predicate\n"; CTL.Atomic($1, $3) } ; formula_id: - | IDENTIFIER { Logging.out "\tParsed formula identifier '%s' \n" $1; CTL.Atomic($1, []) } + | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; + CTL.Atomic($1, [formula_id_const]) } ; params: | {[]} - | IDENTIFIER { [$1] } - | IDENTIFIER COMMA params { $1 :: $3 } + | identifier { [$1] } + | identifier COMMA params { $1 :: $3 } ; transition_label: - | IDENTIFIER { match $1 with + | identifier { match $1 with | "Body" | "body" -> Some CTL.Body | "InitExpr" | "initexpr" -> Some CTL.InitExpr | "Cond" | "cond" -> Some CTL.Cond @@ -147,4 +140,13 @@ formula: | NOT formula { Logging.out "\tParsed NOT\n"; CTL.Not ($2) } ; +identifier: + | IDENTIFIER { if Str.string_match (Str.regexp_string Ctl_parser_types.infer_prefix) $1 0 then ( + Logging.err + "ERROR: %s contains __infer_ctl_ that is a reserved keyword which cannot be used in identifiers." $1; + assert false) + else $1 + } + ; + %% diff --git a/infer/src/clang/ctl_parser_types.ml b/infer/src/clang/ctl_parser_types.ml index 04c9486ca..31bd4736e 100644 --- a/infer/src/clang/ctl_parser_types.ml +++ b/infer/src/clang/ctl_parser_types.ml @@ -37,3 +37,20 @@ type ctl_checker = { name : string; (* Checker's name *) definitions : clause list (* A list of let/set definitions *) } + +let infer_prefix = "__infer_ctl_" +let formula_id_const = infer_prefix ^ "formula_id__" +let report_when_const = "report_when" + +let print_checker c = + Logging.out "\n-------------------- \n"; + Logging.out "\nChecker name: %s\n" c.name; + IList.iter (fun d -> (match d with + | CSet (clause_name, phi) + | CLet (clause_name, phi) -> + Logging.out " %s= \n %a\n\n" + clause_name CTL.Debug.pp_formula phi + | CDesc (clause_name, s) -> + Logging.out " %s= \n %s\n\n" clause_name s) + ) c.definitions; + Logging.out "\n-------------------- \n" diff --git a/infer/src/clang/linter_rules/linters.al b/infer/src/clang/linter_rules/linters.al index 2f9b66ca9..a34ac052d 100644 --- a/infer/src/clang/linter_rules/linters.al +++ b/infer/src/clang/linter_rules/linters.al @@ -169,7 +169,7 @@ DEFINE-CHECKER global_var_init_with_calls_warning = { SET report_when = WHEN - (ctl_is_global_var AND ctl_is_initialized_with_expensive_call) + (is_global_var AND is_initialized_with_expensive_call) HOLDS-IN-NODE VarDecl; SET description =