[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

@@ -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"

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
 
 
 

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

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

infer/src/clang/ctl_parser.mly

@@ -62,21 +62,13 @@ checkers_list:
   ;
 
 checker:
- DEFINE_CHECKER IDENTIFIER ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE
+ DEFINE_CHECKER identifier ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE
-  { let name = $2 in
+  {
-    let definitions = $5 in
+    Logging.out "\nParsed checker definition";
-    Logging.out "\nParsed checker definition: %s\n" name;
+    let c = { name = $2; definitions = $5 } in
-    IList.iter (fun d -> (match d with
+    print_checker c;
-      | Ctl_parser_types.CSet (clause_name, phi)
+    c
-      | 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 }
-    }
 ;
 
 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 { [$1] }
-  | IDENTIFIER COMMA params { $1 :: $3 }
+  | 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
+              }
+              ;
+
 %%

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"

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 =