From d32faf4f4616a37a716a8899b9b9007c58d80fb7 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Wed, 29 Mar 2017 03:23:14 -0700 Subject: [PATCH] Replacing strings by a new data type for AL variables Reviewed By: dulmarod Differential Revision: D4737573 fbshipit-source-id: b9bf2fc --- infer/src/clang/ALVar.ml | 78 +++++++++++++++++ infer/src/clang/ALVar.mli | 45 ++++++++++ infer/src/clang/cFrontend_errors.ml | 131 +++++++++++++++++++--------- infer/src/clang/cPredicates.ml | 7 +- infer/src/clang/cPredicates.mli | 2 +- infer/src/clang/cTL.ml | 58 +++++++----- infer/src/clang/cTL.mli | 18 ++-- infer/src/clang/ctl_parser.mly | 81 ++++++++++++----- infer/src/clang/ctl_parser_types.ml | 1 - 9 files changed, 322 insertions(+), 99 deletions(-) create mode 100644 infer/src/clang/ALVar.ml create mode 100644 infer/src/clang/ALVar.mli diff --git a/infer/src/clang/ALVar.ml b/infer/src/clang/ALVar.ml new file mode 100644 index 000000000..9b54e4f80 --- /dev/null +++ b/infer/src/clang/ALVar.ml @@ -0,0 +1,78 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) +open! IStd + +type keyword = + | Report_when + | Message + | Suggestion + | Severity + | Mode +[@@deriving compare] + +type formula_id = Formula_id of string[@@deriving compare] + +type alexp = + | Const of string + | Var of string + | FId of formula_id +[@@deriving compare] + +type t = alexp[@@deriving compare] + +let equal = [%compare.equal : t] + +let formula_id_to_string fid = + match fid with + | Formula_id s -> s + +let alexp_to_string e = + match e with + | Const s + | Var s + | FId (Formula_id s) -> s + +let keyword_to_string k = + match k with + | Report_when -> "report_when" + | Message -> "message" + | Suggestion -> "suggestion" + | Severity -> "severity" + | Mode -> "mode" + +let is_report_when_keyword k = + match k with + | Report_when -> true + | _ -> false + +let is_message_keyword k = + match k with + | Message -> true + | _ -> false + +let is_suggestion_keyword k = + match k with + | Suggestion -> true + | _ -> false + +let is_severity_keyword k = + match k with + | Severity -> true + | _ -> false + +let is_mode_keyword k = + match k with + | Mode -> true + | _ -> false + + +module FormulaIdMap = Caml.Map.Make ( + struct + type t = formula_id[@@deriving compare] + end) diff --git a/infer/src/clang/ALVar.mli b/infer/src/clang/ALVar.mli new file mode 100644 index 000000000..c3140ecbe --- /dev/null +++ b/infer/src/clang/ALVar.mli @@ -0,0 +1,45 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) +open! IStd + +type keyword = + | Report_when + | Message + | Suggestion + | Severity + | Mode + +type formula_id = Formula_id of string + +type alexp = + | Const of string + | Var of string + | FId of formula_id + +type t = alexp + +val equal : t -> t -> bool + +val formula_id_to_string : formula_id -> string + +val alexp_to_string : t -> string + +val keyword_to_string : keyword -> string + +val is_report_when_keyword : keyword -> bool + +val is_message_keyword : keyword -> bool + +val is_suggestion_keyword : keyword -> bool + +val is_severity_keyword : keyword -> bool + +val is_mode_keyword : keyword -> bool + +module FormulaIdMap : Caml.Map.S with type key = formula_id diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index bde074742..2e22d21c8 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -105,7 +105,6 @@ let string_to_issue_mode m = let create_parsed_linters linters_def_file checkers : linter list = let open CIssue in let open CTL 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 = { @@ -118,15 +117,15 @@ let create_parsed_linters linters_def_file checkers : linter list = } in let issue_desc, condition = List.fold ~f:(fun (issue', cond') d -> match d with - | CSet (s, phi) when String.equal s report_when_const -> + | CSet (av, phi) when ALVar.is_report_when_keyword av -> issue', phi - | CDesc (s, msg) when String.equal s message_const -> + | CDesc (av, msg) when ALVar.is_message_keyword av -> {issue' with description = msg}, cond' - | CDesc (s, sugg) when String.equal s suggestion_const -> + | CDesc (av, sugg) when ALVar.is_suggestion_keyword av -> {issue' with suggestion = Some sugg}, cond' - | CDesc (s, sev) when String.equal s severity_const -> + | CDesc (av, sev) when ALVar.is_severity_keyword av -> {issue' with severity = string_to_err_kind sev}, cond' - | CDesc (s, m) when String.equal s mode_const -> + | CDesc (av, m) when ALVar.is_mode_keyword av -> {issue' with mode = string_to_issue_mode m }, cond' | _ -> issue', cond') ~init:(dummy_issue, CTL.False) c.definitions in if Config.debug_mode then ( @@ -137,9 +136,62 @@ let create_parsed_linters linters_def_file checkers : linter list = {condition; issue_desc; def_file = Some linters_def_file} in List.map ~f:do_one_checker checkers +let check_def_well_expanded vars expanded_formula = + let open CTL in + let check_const c = + match c with + | ALVar.Const c when List.mem vars (ALVar.Var c) -> + failwith ("[ERROR]: Const '" ^ c ^ + "' is used as formal parameter of some LET definition.") + | ALVar.Const _ -> () + | ALVar.Var v + | ALVar.FId (Formula_id v) -> + failwith ("[ERROR]: Variable '" ^ v ^ + "' could not be substituted and cannot be evaluated") in + let rec check_expansion exp_f = + match exp_f with + | True + | False -> () + | Atomic (_, ps) -> List.iter ~f: check_const ps + | Not f1 -> check_expansion f1 + | And (f1, f2) -> + check_expansion f1; + check_expansion f2 + | Or (f1, f2) -> + check_expansion f1; + check_expansion f2 + | Implies (f1, f2) -> + check_expansion f1; + check_expansion f2 + | InNode (node_type_list, f1) -> + List.iter ~f:check_const node_type_list; + check_expansion f1 + | AU (f1, f2) -> + check_expansion f1; + check_expansion f2 + | EU (_, f1, f2) -> + check_expansion f1; + check_expansion f2 + | EF (_, f1) -> check_expansion f1 + | AF f1 -> check_expansion f1 + | AG f1 -> check_expansion f1 + | EX (_, f1) -> check_expansion f1 + | AX f1 -> check_expansion f1 + | EH (cl, f1) -> + List.iter ~f:check_const cl; + check_expansion f1 + | EG (_, f1) -> check_expansion f1 + | ET (ntl, _, f1) -> + List.iter ~f: check_const ntl; + check_expansion f1 + | ETX (ntl, _, f1) -> + List.iter ~f: check_const ntl; + check_expansion f1 in + check_expansion expanded_formula + let rec apply_substitution f sub = let sub_param p = try - snd (List.find_exn sub ~f:(fun (a,_) -> String.equal p a)) + snd (List.find_exn sub ~f:(fun (a,_) -> ALVar.equal p a)) with Not_found -> p in let sub_list_param ps = List.map ps ~f:sub_param in @@ -177,37 +229,26 @@ let expand_checkers checkers = name error_msg; failwith ("Cannot expand....\n") in let open CTL in - let open Ctl_parser_types in let rec expand acc map error_msg = match acc with | True | False -> acc - | Atomic (name, [p]) when String.equal formula_id_const p -> - (* constant case, macro with no params *) - let error_msg' = error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in - (match Core.Std.String.Map.find map name with - | Some (true, _, _) -> - fail_with_circular_macro_definition name error_msg' - | Some (false, params, f1) -> - let map' = Core.Std.String.Map.add map ~key:name ~data:(true, params, f1) in - expand f1 map' error_msg' - | None -> failwith - ("[ERROR]: Formula identifier '" ^ name ^ "' is undefined. Cannot expand.")) - | Atomic (name, actual_param) -> (* it may be a macro *) - let error_msg' = error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in - (match Core.Std.String.Map.find map name with - | Some (true, _, _) -> - fail_with_circular_macro_definition name error_msg' - | Some (false, formal_params, f1) -> (* in this case it should be a defined macro *) - (match List.zip formal_params actual_param with - | Some sub -> - let f1_sub = apply_substitution f1 sub in - let map' = Core.Std.String.Map.add map - ~key:name ~data:(true, formal_params, f1) in - expand f1_sub map' error_msg' - | None -> failwith ("[ERROR]: Formula identifier '" ^ name ^ - "' is no called with the right number of parameters")) - | None -> acc) (* in this case it should be a predicate *) + | Atomic (ALVar.Formula_id (name) as av, actual_param) -> (* it may be a macro *) + (let error_msg' = + error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in + (try + match ALVar.FormulaIdMap.find av map with + | (true, _, _) -> + fail_with_circular_macro_definition name error_msg' + | (false, fparams, f1) -> (* in this case it should be a defined macro *) + (match List.zip fparams actual_param with + | Some sub -> + let f1_sub = apply_substitution f1 sub in + let map' = ALVar.FormulaIdMap.add av (true, fparams, f1) map in + expand f1_sub map' error_msg' + | None -> failwith ("[ERROR]: Formula identifier '" ^ name ^ + "' is not called with the right number of parameters")) + with Not_found -> acc)) (* in this case it should be a predicate *) | Not f1 -> Not (expand f1 map error_msg) | And (f1, f2) -> And (expand f1 map error_msg, expand f2 map error_msg) | Or (f1, f2) -> Or (expand f1 map error_msg, expand f2 map error_msg) @@ -224,22 +265,26 @@ let expand_checkers checkers = | EG (trans, f1) -> 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 - let expand_one_checker c = - Logging.out " +Start expanding %s\n" c.name; + let expand_one_checker checker = + Logging.out " +Start expanding %s\n" checker.name; (* Map a formula id to a triple (visited, parameters, definition). Visited is used during the expansion phase to understand if the formula was already expanded and, if yes we have a cyclic definifion *) - let map : (bool * string list * CTL.t) Core.Std.String.Map.t = Core.Std.String.Map.empty in - let map = List.fold ~f:(fun map' d -> match d with - | CLet (k, params, formula) -> Core.Std.Map.add map' ~key:k ~data:(false, params, formula) - | _ -> map') ~init:map c.definitions in + let map : (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t = ALVar.FormulaIdMap.empty in + let map, vars = List.fold ~f:(fun (map', vars') definition -> + match definition with + | CLet (key, params, formula) -> + ALVar.FormulaIdMap.add key (false, params, formula) map', List.append vars' params + | _ -> map', vars') ~init:(map, []) checker.definitions in let exp_defs = List.fold ~f:(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) ~init:[] c.definitions in - { c with definitions = exp_defs} in + let exp_report_when = expand phi map "" in + check_def_well_expanded vars exp_report_when; + CSet (report_when_const, exp_report_when) :: defs + | cl -> cl :: defs) ~init:[] checker.definitions in + { checker with definitions = exp_defs} in let expanded_checkers = List.map ~f:expand_one_checker checkers in expanded_checkers diff --git a/infer/src/clang/cPredicates.ml b/infer/src/clang/cPredicates.ml index 42645586e..f9fac8e91 100644 --- a/infer/src/clang/cPredicates.ml +++ b/infer/src/clang/cPredicates.ml @@ -59,7 +59,7 @@ let captured_variables_cxx_ref an = -type t = string * string list (* (name, [param1,...,paramK]) *) +type t = ALVar.formula_id * ALVar.alexp list(* (name, [param1,...,paramK]) *) (* true if and only if string contained occurs in container *) let str_contains container contained = @@ -68,7 +68,9 @@ let str_contains container contained = Str.search_forward rexp container 0 >= 0 with Not_found -> false -let pp_predicate fmt (name, arglist) = +let pp_predicate fmt (_name, _arglist) = + let name = ALVar.formula_id_to_string _name in + let arglist = List.map ~f:ALVar.alexp_to_string _arglist in Format.fprintf fmt "%s(%a)" name (Pp.comma_seq Format.pp_print_string) arglist let is_declaration_kind decl s = @@ -122,7 +124,6 @@ let call_method an m = _call_method (str_contains) an m let _call_class_method comp an cname mname = - Logging.out "...Evaluating call_class_method\n"; match an with | Ctl_parser_types.Stmt (Clang_ast_t.ObjCMessageExpr (_, receiver :: _, _, omei)) -> is_object_of_class_named receiver cname && diff --git a/infer/src/clang/cPredicates.mli b/infer/src/clang/cPredicates.mli index d4591f30e..4ef229caa 100644 --- a/infer/src/clang/cPredicates.mli +++ b/infer/src/clang/cPredicates.mli @@ -9,7 +9,7 @@ open! IStd -type t = string * string list (* (name, [param1,...,paramK]) *) +type t = ALVar.formula_id * ALVar.alexp list (* (name, [param1,...,paramK]) *) val captured_variables_cxx_ref : Ctl_parser_types.ast_node -> Clang_ast_t.named_decl_info list diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index c0dc2a58f..a6041e2b8 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -35,7 +35,7 @@ type t = (* A ctl formula *) | And of t * t | Or of t * t | Implies of t * t - | InNode of string list * t + | InNode of ALVar.alexp list * t | AX of t | EX of transitions option * t | AF of t @@ -44,9 +44,9 @@ type t = (* A ctl formula *) | EG of transitions option * t | AU of t * t | EU of transitions option * t * t - | EH of string list * t - | ET of string list * transitions option * t - | ETX of string list * transitions option * t + | EH of ALVar.alexp list * t + | ET of ALVar.alexp list * transitions option * t + | ETX of ALVar.alexp list * transitions option * t (* "set" clauses are used for defining mandatory variables that will be used by when reporting issues: eg for defining the condition. @@ -65,9 +65,9 @@ type t = (* A ctl formula *) *) type clause = - | CLet of string * string list * t (* Let clause: let id = definifion; *) - | CSet of string * t (* Set clause: set id = definition *) - | CDesc of string * string (* Description clause eg: set message = "..." *) + | CLet of ALVar.formula_id * ALVar.t list * t (* Let clause: let id = definifion; *) + | CSet of ALVar.keyword * t (* Set clause: set id = definition *) + | CDesc of ALVar.keyword * string (* Description clause eg: set message = "..." *) type ctl_checker = { name : string; (* Checker's name *) @@ -92,6 +92,8 @@ module Debug = struct let full_print = true let rec pp_formula fmt phi = + let nodes_to_string nl = + List.map ~f:ALVar.alexp_to_string nl in match phi with | True -> Format.fprintf fmt "True" | False -> Format.fprintf fmt "False" @@ -106,7 +108,8 @@ module Debug = struct else Format.fprintf fmt "(... OR ...)" | Implies (phi1, phi2) -> Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2 | InNode (nl, phi) -> Format.fprintf fmt "IN-NODE %a: (%a)" - (Pp.comma_seq Format.pp_print_string) nl + (Pp.comma_seq Format.pp_print_string) + (nodes_to_string nl) pp_formula phi | AX phi -> Format.fprintf fmt "AX(%a)" pp_formula phi | EX (trs, phi) -> Format.fprintf fmt "EX[->%a](%a)" pp_transition trs pp_formula phi @@ -118,14 +121,17 @@ module Debug = struct | EU (trs, phi1, phi2) -> Format.fprintf fmt "E[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2 | EH (arglist, phi) -> Format.fprintf fmt "EH[%a](%a)" - (Pp.comma_seq Format.pp_print_string) arglist + (Pp.comma_seq Format.pp_print_string) + (nodes_to_string arglist) pp_formula phi | ET (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" - (Pp.comma_seq Format.pp_print_string) arglist + (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) arglist + (Pp.comma_seq Format.pp_print_string) + (nodes_to_string arglist) pp_transition trans pp_formula phi @@ -154,7 +160,8 @@ module Debug = struct forest: tree list; } - let create_content ast_node phi lcxt = {ast_node; phi; eval_result = Eval_undefined; lcxt = lcxt; } + let create_content ast_node phi lcxt = + {ast_node; phi; eval_result = Eval_undefined; lcxt = lcxt; } let create () = {next_id = 0; eval_stack = Stack.create(); forest = [] } @@ -256,12 +263,17 @@ let print_checker c = Logging.out "\n-------------------- \n"; Logging.out "\nChecker name: %s\n" c.name; List.iter ~f:(fun d -> (match d with - | CSet (clause_name, phi) - | CLet (clause_name, _, phi) -> + | CSet (keyword, phi) -> + let cn_str = ALVar.keyword_to_string keyword in Logging.out " %s= \n %a\n\n" - clause_name Debug.pp_formula phi - | CDesc (clause_name, s) -> - Logging.out " %s= \n %s\n\n" clause_name s) + cn_str Debug.pp_formula phi + | CLet (exp, _, phi) -> + let cn_str = ALVar.formula_id_to_string exp in + Logging.out " %s= \n %a\n\n" + cn_str Debug.pp_formula phi + | CDesc (keyword, s) -> + let cn_str = ALVar.keyword_to_string keyword in + Logging.out " %s= \n %s\n\n" cn_str s) ) c.definitions; Logging.out "\n-------------------- \n" @@ -335,8 +347,8 @@ let node_to_unique_string_id an = (* true iff an ast node is a node of type among the list tl *) let node_has_type tl an = - let an_str = node_to_string an in - List.mem ~equal:String.equal tl an_str + let an_alexp = ALVar.Const (node_to_string an) in + List.mem ~equal:ALVar.equal tl an_alexp (* given a decl returns a stmt such that decl--->stmt via label trs *) let transition_decl_to_stmt d trs = @@ -419,7 +431,9 @@ let next_state_via_transition an trans = (* 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) *) -let rec eval_Atomic pred_name args an lcxt = +let rec eval_Atomic _pred_name _args an lcxt = + let pred_name = ALVar.formula_id_to_string _pred_name in + let args = List.map ~f:ALVar.alexp_to_string _args in match pred_name, args, an with | "call_method", [m], an -> CPredicates.call_method an m | "call_method_strict", [m], an -> CPredicates.call_method_strict an m @@ -564,8 +578,8 @@ and eval_ET tl trs phi an lcxt = and eval_ETX tl trs phi an lcxt = let lcxt', tl' = match lcxt.CLintersContext.et_evaluation_node, node_has_type tl an with | None, true -> - let an_str = node_to_string an in - {lcxt with CLintersContext.et_evaluation_node = Some (node_to_unique_string_id an) }, [an_str] + let an_alexp = ALVar.Const (node_to_string an) in + {lcxt with CLintersContext.et_evaluation_node = Some (node_to_unique_string_id an) }, [an_alexp] | _, _ -> lcxt, tl in let f = match trs with | Some _ -> EF (None, (InNode (tl', EX (trs, phi)))) diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 9a7f8c367..5c96beb02 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -36,7 +36,7 @@ type t = | And of t * t | Or of t * t | Implies of t * t - | InNode of string list * t + | InNode of ALVar.alexp list * t | AX of t (** AX phi <=> for all children of the current node phi holds *) | EX of transitions option * t (** EX phi <=> exist a child of the current node such that phi holds *) | AF of t (** AF phi <=> for all path from the current node there is a descendant where phi holds *) @@ -48,13 +48,13 @@ type t = for all paths from the current node phi1 holds in every node until ph2 holds *) | EU of transitions option * t * t (** EU(phi1, phi2) <=> there exists a path from the current node such that phi1 holds until phi2 holds *) - | EH of string list * t (** EH[classes]phi <=> - there exists a node defining a super class in the hierarchy of the class - defined by the current node (if any) where phi holds *) - | ET of string list * transitions option * t (** ET[T][l] phi <=> + | EH of ALVar.alexp list * t (** EH[classes]phi <=> + there exists a node defining a super class in the hierarchy of the class + defined by the current node (if any) where phi holds *) + | ET 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. *) - | ETX of string list * transitions option * t (** ET[T][l] phi <=> + | 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. *) @@ -76,9 +76,9 @@ type t = *) type clause = - | CLet of string * string list * t (* Let clause: let id = definifion; *) - | CSet of string * t (* Set clause: set id = definition *) - | CDesc of string * string (* Description clause eg: set message = "..." *) + | CLet of ALVar.formula_id * ALVar.t list * t (* Let clause: let id = definifion; *) + | CSet of ALVar.keyword * t (* Set clause: set id = definition *) + | CDesc of ALVar.keyword * string (* Description clause eg: set message = "..." *) type ctl_checker = { name : string; (* Checker's name *) diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 2006221f2..19f495ac3 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -8,8 +8,7 @@ */ %{ - open Ctl_parser_types - + let formal_params : (ALVar.t list) ref = ref [] %} %token EU @@ -56,6 +55,16 @@ %start checkers_list %% + +var_list: + | identifier { [ALVar.Var $1] } + | identifier COMMA var_list { ALVar.Var($1) :: $3 } +; + +formal_params: + | var_list { formal_params := $1; $1} + + checkers_list: | EOF { [] } | checker SEMICOLON checkers_list { $1::$3 } @@ -78,32 +87,64 @@ clause_list: clause: | SET identifier ASSIGNMENT formula - { Logging.out "\tParsed set clause\n"; CTL.CSet ($2, $4) } + { Logging.out "\tParsed SET clause\n"; + let alvar = match $2 with + | "report_when" -> ALVar.Report_when + | _ -> failwith ("[ERROR] string '%s' cannot be set to a variable. " ^ + "Use the reserverd variable 'report_when'\n") in + CTL.CSet (alvar, $4) } | SET identifier ASSIGNMENT STRING - { Logging.out "\tParsed desc clause\n"; CTL.CDesc ($2, $4) } - | LET identifier ASSIGNMENT formula - { Logging.out "\tParsed let clause\n"; CTL.CLet ($2, [], $4) } - | LET identifier LEFT_PAREN params RIGHT_PAREN ASSIGNMENT formula - { Logging.out "\tParsed let clause with formula identifier '%s(....)' \n" $2; - CTL.CLet($2, $4, $7) } + { Logging.out "\tParsed SET clause\n"; + let alvar = match $2 with + | "message" -> ALVar.Message + | "suggestion" -> ALVar.Suggestion + | "severity" -> ALVar.Severity + | "mode" -> ALVar.Mode + | _ -> failwith ("[ERROR] string '%s' cannot be set in a SET clause. " ^ + "Use either of: 'message', 'suggestion', 'severity', or 'mode'\n") in + CTL.CDesc (alvar, $4) } + | LET formula_id_def ASSIGNMENT formula + { Logging.out "\tParsed LET clause\n"; CTL.CLet ($2, [], $4) } + | LET formula_id_def LEFT_PAREN formal_params RIGHT_PAREN ASSIGNMENT formula + { Logging.out "\tParsed let clause with formula identifier '%s(....)' \n" + (ALVar.formula_id_to_string $2); + CTL.CLet ($2, $4, $7) } ; atomic_formula: | TRUE { Logging.out "\tParsed True\n"; CTL.True } | FALSE { Logging.out "\tParsed False\n"; CTL.False } - | identifier LEFT_PAREN params RIGHT_PAREN - { Logging.out "\tParsed predicate\n"; CTL.Atomic($1, $3) } + | identifier LEFT_PAREN actual_params RIGHT_PAREN + { Logging.out "\tParsed predicate\n"; CTL.Atomic(ALVar.Formula_id $1, $3) } ; + formula_id_def: + | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; + formal_params := []; + ALVar.Formula_id $1 } + ; + formula_id: | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; - CTL.Atomic($1, [formula_id_const]) } + ALVar.Formula_id $1 } ; -params: +actual_params: | {[]} - | identifier { [$1] } - | identifier COMMA params { $1 :: $3 } + | identifier { if (List.mem (ALVar.Var $1) !formal_params) then + (Logging.out "\tParsed exp '%s' as variable \n" $1; + [ALVar.Var $1]) + else + (Logging.out "\tParsed exp '%s' as constant \n" $1; + [ALVar.Const $1]) + } + | identifier COMMA actual_params { + (if (List.mem (ALVar.Var $1) !formal_params) then + (Logging.out "\tParsed exp '%s' as variable \n" $1; + ALVar.Var $1) + else (Logging.out "\tParsed exp '%s' as constant \n" $1; + ALVar.Const $1) + ) :: $3 } ; transition_label: @@ -125,7 +166,7 @@ formula_with_paren: formula: | formula_with_paren { $1 } - | formula_id { $1 } + | formula_id { CTL.Atomic($1, []) } | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 } | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU (None, $1, $3) } | formula AU formula { Logging.out "\tParsed AU\n"; CTL.AU ($1, $3) } @@ -134,13 +175,13 @@ formula: | formula AX { Logging.out "\tParsed AX\n"; CTL.AX ($1) } | formula EG { Logging.out "\tParsed EG\n"; CTL.EG (None, $1) } | formula AG { Logging.out "\tParsed AG\n"; CTL.AG ($1) } - | formula EH params { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) } + | formula EH actual_params { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) } | formula EF { Logging.out "\tParsed EF\n"; CTL.EF (None, $1) } - | WHEN formula HOLDS_IN_NODE params + | WHEN formula HOLDS_IN_NODE actual_params { Logging.out "\tParsed InNode\n"; CTL.InNode ($4, $2)} - | ET params WITH_TRANSITION transition_label formula_EF + | ET actual_params WITH_TRANSITION transition_label formula_EF { Logging.out "\tParsed ET\n"; CTL.ET ($2, $4, $5)} - | ETX params WITH_TRANSITION transition_label formula_EF + | ETX actual_params WITH_TRANSITION transition_label formula_EF { Logging.out "\tParsed ETX\n"; CTL.ETX ($2, $4, $5)} | EX WITH_TRANSITION transition_label formula_with_paren { Logging.out "\tParsed EX\n"; CTL.EX ($3, $4)} diff --git a/infer/src/clang/ctl_parser_types.ml b/infer/src/clang/ctl_parser_types.ml index 1ffb49729..cef4792f3 100644 --- a/infer/src/clang/ctl_parser_types.ml +++ b/infer/src/clang/ctl_parser_types.ml @@ -19,7 +19,6 @@ type ast_node = let infer_prefix = "__infer_ctl_" -let formula_id_const = infer_prefix ^ "formula_id__" let report_when_const = "report_when" let message_const = "message" let suggestion_const = "suggestion"