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

Replacing strings by a new data type for AL variables

Browse Source 
Reviewed By: dulmarod

Differential Revision: D4737573

fbshipit-source-id: b9bf2fc
master
Dino Distefano 8 years ago committed by Facebook Github Bot
parent 5482f110c1
commit d32faf4f46
9 changed files with 322 additions and 99 deletions
Show Stats Download Patch File Download Diff File

78
infer/src/clang/ALVar.ml
Unescape View File

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

45
infer/src/clang/ALVar.mli
Unescape View File

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

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

@ -105,7 +105,6 @@ let string_to_issue_mode m =
let create_parsed_linters linters_def_file checkers : linter list = let create_parsed_linters linters_def_file checkers : linter list =
let open CIssue in let open CIssue in
let open CTL in let open CTL in
let open Ctl_parser_types in
Logging.out "\n Converting checkers in (condition, issue) pairs\n"; Logging.out "\n Converting checkers in (condition, issue) pairs\n";
let do_one_checker c = let do_one_checker c =
let dummy_issue = { let dummy_issue = {
@ -118,15 +117,15 @@ let create_parsed_linters linters_def_file checkers : linter list =
} in } in
let issue_desc, condition = List.fold ~f:(fun (issue', cond') d -> let issue_desc, condition = List.fold ~f:(fun (issue', cond') d ->
match d with 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 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' {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' {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' {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' with mode = string_to_issue_mode m }, cond'
| _ -> issue', cond') ~init:(dummy_issue, CTL.False) c.definitions in | _ -> issue', cond') ~init:(dummy_issue, CTL.False) c.definitions in
if Config.debug_mode then ( 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 {condition; issue_desc; def_file = Some linters_def_file} in
List.map ~f:do_one_checker checkers 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 rec apply_substitution f sub =
let sub_param p = try 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 with Not_found -> p in
let sub_list_param ps = let sub_list_param ps =
List.map ps ~f:sub_param in List.map ps ~f:sub_param in
@ -177,37 +229,26 @@ let expand_checkers checkers =
name error_msg; name error_msg;
failwith ("Cannot expand....\n") in failwith ("Cannot expand....\n") in
let open CTL in let open CTL in
let open Ctl_parser_types in
let rec expand acc map error_msg = let rec expand acc map error_msg =
match acc with match acc with
| True | True
| False -> acc | False -> acc
| Atomic (name, [p]) when String.equal formula_id_const p -> | Atomic (ALVar.Formula_id (name) as av, actual_param) -> (* it may be a macro *)
(* constant case, macro with no params *) (let error_msg' =
let error_msg' = error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in
(match Core.Std.String.Map.find map name with (try
| Some (true, _, _) -> match ALVar.FormulaIdMap.find av map with
fail_with_circular_macro_definition name error_msg' | (true, _, _) ->
| 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' fail_with_circular_macro_definition name error_msg'
| Some (false, formal_params, f1) -> (* in this case it should be a defined macro *) | (false, fparams, f1) -> (* in this case it should be a defined macro *)
(match List.zip formal_params actual_param with (match List.zip fparams actual_param with
| Some sub -> | Some sub ->
let f1_sub = apply_substitution f1 sub in let f1_sub = apply_substitution f1 sub in
let map' = Core.Std.String.Map.add map let map' = ALVar.FormulaIdMap.add av (true, fparams, f1) map in
~key:name ~data:(true, formal_params, f1) in
expand f1_sub map' error_msg' expand f1_sub map' error_msg'
| None -> failwith ("[ERROR]: Formula identifier '" ^ name ^ | None -> failwith ("[ERROR]: Formula identifier '" ^ name ^
"' is no called with the right number of parameters")) "' is not called with the right number of parameters"))
| None -> acc) (* in this case it should be a predicate *) with Not_found -> acc)) (* in this case it should be a predicate *)
| Not f1 -> Not (expand f1 map error_msg) | Not f1 -> Not (expand f1 map error_msg)
| And (f1, f2) -> And (expand f1 map error_msg, expand f2 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) | 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) | EG (trans, f1) -> EG (trans, expand f1 map error_msg)
| ET (tl, sw, f1) -> ET (tl, sw, 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 | ETX (tl, sw, f1) -> ETX (tl, sw, expand f1 map error_msg) in
let expand_one_checker c = let expand_one_checker checker =
Logging.out " +Start expanding %s\n" c.name; Logging.out " +Start expanding %s\n" checker.name;
(* Map a formula id to a triple (visited, parameters, definition). (* Map a formula id to a triple (visited, parameters, definition).
Visited is used during the expansion phase to understand if the Visited is used during the expansion phase to understand if the
formula was already expanded and, if yes we have a cyclic definifion *) 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 : (bool * ALVar.t list * CTL.t) ALVar.FormulaIdMap.t = ALVar.FormulaIdMap.empty in
let map = List.fold ~f:(fun map' d -> match d with let map, vars = List.fold ~f:(fun (map', vars') definition ->
| CLet (k, params, formula) -> Core.Std.Map.add map' ~key:k ~data:(false, params, formula) match definition with
| _ -> map') ~init:map c.definitions in | 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 -> let exp_defs = List.fold ~f:(fun defs clause ->
match clause with match clause with
| CSet (report_when_const, phi) -> | CSet (report_when_const, phi) ->
Logging.out " -Expanding report_when\n"; Logging.out " -Expanding report_when\n";
CSet (report_when_const, expand phi map "") :: defs let exp_report_when = expand phi map "" in
| cl -> cl :: defs) ~init:[] c.definitions in check_def_well_expanded vars exp_report_when;
{ c with definitions = exp_defs} in 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 let expanded_checkers = List.map ~f:expand_one_checker checkers in
expanded_checkers expanded_checkers

7
infer/src/clang/cPredicates.ml
Unescape View File

@ -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 *) (* true if and only if string contained occurs in container *)
let str_contains container contained = let str_contains container contained =
@ -68,7 +68,9 @@ let str_contains container contained =
Str.search_forward rexp container 0 >= 0 Str.search_forward rexp container 0 >= 0
with Not_found -> false 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 Format.fprintf fmt "%s(%a)" name (Pp.comma_seq Format.pp_print_string) arglist
let is_declaration_kind decl s = let is_declaration_kind decl s =
@ -122,7 +124,6 @@ let call_method an m =
_call_method (str_contains) an m _call_method (str_contains) an m
let _call_class_method comp an cname mname = let _call_class_method comp an cname mname =
Logging.out "...Evaluating call_class_method\n";
match an with match an with
| Ctl_parser_types.Stmt (Clang_ast_t.ObjCMessageExpr (_, receiver :: _, _, omei)) -> | Ctl_parser_types.Stmt (Clang_ast_t.ObjCMessageExpr (_, receiver :: _, _, omei)) ->
is_object_of_class_named receiver cname && is_object_of_class_named receiver cname &&

2
infer/src/clang/cPredicates.mli
Unescape View File

@ -9,7 +9,7 @@
open! IStd 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 val captured_variables_cxx_ref : Ctl_parser_types.ast_node -> Clang_ast_t.named_decl_info list

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

@ -35,7 +35,7 @@ type t = (* A ctl formula *)
| And of t * t | And of t * t
| Or of t * t | Or of t * t
| Implies of t * t | Implies of t * t
| InNode of string list * t | InNode of ALVar.alexp list * t
| AX of t | AX of t
| EX of transitions option * t | EX of transitions option * t
| AF of t | AF of t
@ -44,9 +44,9 @@ type t = (* A ctl formula *)
| EG of transitions option * t | EG of transitions option * t
| AU of t * t | AU of t * t
| EU of transitions option * t * t | EU of transitions option * t * t
| EH of string list * t | EH of ALVar.alexp list * t
| ET of string list * transitions option * t | ET of ALVar.alexp list * transitions option * t
| ETX of string list * transitions option * t | ETX of ALVar.alexp list * transitions option * t
(* "set" clauses are used for defining mandatory variables that will be used (* "set" clauses are used for defining mandatory variables that will be used
by when reporting issues: eg for defining the condition. by when reporting issues: eg for defining the condition.
@ -65,9 +65,9 @@ type t = (* A ctl formula *)
*) *)
type clause = type clause =
| CLet of string * string list * t (* Let clause: let id = definifion; *) | CLet of ALVar.formula_id * ALVar.t list * t (* Let clause: let id = definifion; *)
| CSet of string * t (* Set clause: set id = definition *) | CSet of ALVar.keyword * t (* Set clause: set id = definition *)
| CDesc of string * string (* Description clause eg: set message = "..." *) | CDesc of ALVar.keyword * string (* Description clause eg: set message = "..." *)
type ctl_checker = { type ctl_checker = {
name : string; (* Checker's name *) name : string; (* Checker's name *)
@ -92,6 +92,8 @@ module Debug = struct
let full_print = true let full_print = true
let rec pp_formula fmt phi = let rec pp_formula fmt phi =
let nodes_to_string nl =
List.map ~f:ALVar.alexp_to_string nl in
match phi with match phi with
| True -> Format.fprintf fmt "True" | True -> Format.fprintf fmt "True"
| False -> Format.fprintf fmt "False" | False -> Format.fprintf fmt "False"
@ -106,7 +108,8 @@ module Debug = struct
else Format.fprintf fmt "(... OR ...)" else Format.fprintf fmt "(... OR ...)"
| Implies (phi1, phi2) -> Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2 | Implies (phi1, phi2) -> Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2
| InNode (nl, phi) -> Format.fprintf fmt "IN-NODE %a: (%a)" | 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 pp_formula phi
| AX phi -> Format.fprintf fmt "AX(%a)" 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 | 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]" | EU (trs, phi1, phi2) -> Format.fprintf fmt "E[->%a][%a UNTIL %a]"
pp_transition trs pp_formula phi1 pp_formula phi2 pp_transition trs pp_formula phi1 pp_formula phi2
| EH (arglist, phi) -> Format.fprintf fmt "EH[%a](%a)" | 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 pp_formula phi
| ET (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" | 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_transition trans
pp_formula phi pp_formula phi
| ETX (arglist, trans, phi) -> Format.fprintf fmt "ETX[%a][%a](%a)" | 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_transition trans
pp_formula phi pp_formula phi
@ -154,7 +160,8 @@ module Debug = struct
forest: tree list; 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 = [] } let create () = {next_id = 0; eval_stack = Stack.create(); forest = [] }
@ -256,12 +263,17 @@ let print_checker c =
Logging.out "\n-------------------- \n"; Logging.out "\n-------------------- \n";
Logging.out "\nChecker name: %s\n" c.name; Logging.out "\nChecker name: %s\n" c.name;
List.iter ~f:(fun d -> (match d with List.iter ~f:(fun d -> (match d with
| CSet (clause_name, phi) | CSet (keyword, phi) ->
| CLet (clause_name, _, phi) -> let cn_str = ALVar.keyword_to_string keyword in
Logging.out " %s= \n %a\n\n" Logging.out " %s= \n %a\n\n"
clause_name Debug.pp_formula phi cn_str Debug.pp_formula phi
| CDesc (clause_name, s) -> | CLet (exp, _, phi) ->
Logging.out " %s= \n %s\n\n" clause_name s) 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; ) c.definitions;
Logging.out "\n-------------------- \n" 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 *) (* true iff an ast node is a node of type among the list tl *)
let node_has_type tl an = let node_has_type tl an =
let an_str = node_to_string an in let an_alexp = ALVar.Const (node_to_string an) in
List.mem ~equal:String.equal tl an_str List.mem ~equal:ALVar.equal tl an_alexp
(* given a decl returns a stmt such that decl--->stmt via label trs *) (* given a decl returns a stmt such that decl--->stmt via label trs *)
let transition_decl_to_stmt d 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 (* 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 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 match pred_name, args, an with
| "call_method", [m], an -> CPredicates.call_method an m | "call_method", [m], an -> CPredicates.call_method an m
| "call_method_strict", [m], an -> CPredicates.call_method_strict 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 = and eval_ETX tl trs phi an lcxt =
let lcxt', tl' = match lcxt.CLintersContext.et_evaluation_node, node_has_type tl an with let lcxt', tl' = match lcxt.CLintersContext.et_evaluation_node, node_has_type tl an with
| None, true -> | None, true ->
let an_str = node_to_string an in let an_alexp = ALVar.Const (node_to_string an) in
{lcxt with CLintersContext.et_evaluation_node = Some (node_to_unique_string_id an) }, [an_str] {lcxt with CLintersContext.et_evaluation_node = Some (node_to_unique_string_id an) }, [an_alexp]
| _, _ -> lcxt, tl in | _, _ -> lcxt, tl in
let f = match trs with let f = match trs with
| Some _ -> EF (None, (InNode (tl', EX (trs, phi)))) | Some _ -> EF (None, (InNode (tl', EX (trs, phi))))

14
infer/src/clang/cTL.mli
Unescape View File

@ -36,7 +36,7 @@ type t =
| And of t * t | And of t * t
| Or of t * t | Or of t * t
| Implies 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 *) | 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 *) | 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 *) | 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 *) for all paths from the current node phi1 holds in every node until ph2 holds *)
| EU of transitions option * t * t (** EU(phi1, phi2) <=> | EU of transitions option * t * t (** EU(phi1, phi2) <=>
there exists a path from the current node such that phi1 holds until phi2 holds *) there exists a path from the current node such that phi1 holds until phi2 holds *)
| EH of string list * t (** EH[classes]phi <=> | EH of ALVar.alexp list * t (** EH[classes]phi <=>
there exists a node defining a super class in the hierarchy of the class there exists a node defining a super class in the hierarchy of the class
defined by the current node (if any) where phi holds *) defined by the current node (if any) where phi holds *)
| ET of string list * transitions option * t (** ET[T][l] phi <=> | 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 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. *) 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 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. *) making a transition to a node an' via label l, such that in an phi holds. *)
@ -76,9 +76,9 @@ type t =
*) *)
type clause = type clause =
| CLet of string * string list * t (* Let clause: let id = definifion; *) | CLet of ALVar.formula_id * ALVar.t list * t (* Let clause: let id = definifion; *)
| CSet of string * t (* Set clause: set id = definition *) | CSet of ALVar.keyword * t (* Set clause: set id = definition *)
| CDesc of string * string (* Description clause eg: set message = "..." *) | CDesc of ALVar.keyword * string (* Description clause eg: set message = "..." *)
type ctl_checker = { type ctl_checker = {
name : string; (* Checker's name *) name : string; (* Checker's name *)

81
infer/src/clang/ctl_parser.mly
Unescape View File

@ -8,8 +8,7 @@
*/ */
%{ %{
open Ctl_parser_types let formal_params : (ALVar.t list) ref = ref []
%} %}
%token EU %token EU
@ -56,6 +55,16 @@
%start <CTL.ctl_checker list> checkers_list %start <CTL.ctl_checker list> 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: checkers_list:
| EOF { [] } | EOF { [] }
| checker SEMICOLON checkers_list { $1::$3 } | checker SEMICOLON checkers_list { $1::$3 }
@ -78,32 +87,64 @@ clause_list:
clause: clause:
| SET identifier ASSIGNMENT formula | 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 | SET identifier ASSIGNMENT STRING
{ Logging.out "\tParsed desc clause\n"; CTL.CDesc ($2, $4) } { Logging.out "\tParsed SET clause\n";
| LET identifier ASSIGNMENT formula let alvar = match $2 with
{ Logging.out "\tParsed let clause\n"; CTL.CLet ($2, [], $4) } | "message" -> ALVar.Message
| LET identifier LEFT_PAREN params RIGHT_PAREN ASSIGNMENT formula | "suggestion" -> ALVar.Suggestion
{ Logging.out "\tParsed let clause with formula identifier '%s(....)' \n" $2; | "severity" -> ALVar.Severity
CTL.CLet($2, $4, $7) } | "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: atomic_formula:
| TRUE { Logging.out "\tParsed True\n"; CTL.True } | TRUE { Logging.out "\tParsed True\n"; CTL.True }
| FALSE { Logging.out "\tParsed False\n"; CTL.False } | FALSE { Logging.out "\tParsed False\n"; CTL.False }
| identifier LEFT_PAREN params RIGHT_PAREN | identifier LEFT_PAREN actual_params RIGHT_PAREN
{ Logging.out "\tParsed predicate\n"; CTL.Atomic($1, $3) } { 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: formula_id:
| identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; | 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 { if (List.mem (ALVar.Var $1) !formal_params) then
| identifier COMMA params { $1 :: $3 } (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: transition_label:
@ -125,7 +166,7 @@ formula_with_paren:
formula: formula:
| formula_with_paren { $1 } | formula_with_paren { $1 }
| formula_id { $1 } | formula_id { CTL.Atomic($1, []) }
| atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 } | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 }
| formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU (None, $1, $3) } | 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) } | 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 AX { Logging.out "\tParsed AX\n"; CTL.AX ($1) }
| formula EG { Logging.out "\tParsed EG\n"; CTL.EG (None, $1) } | formula EG { Logging.out "\tParsed EG\n"; CTL.EG (None, $1) }
| formula AG { Logging.out "\tParsed AG\n"; CTL.AG ($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) } | 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)} { 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)} { 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)} { Logging.out "\tParsed ETX\n"; CTL.ETX ($2, $4, $5)}
| EX WITH_TRANSITION transition_label formula_with_paren | EX WITH_TRANSITION transition_label formula_with_paren
{ Logging.out "\tParsed EX\n"; CTL.EX ($3, $4)} { Logging.out "\tParsed EX\n"; CTL.EX ($3, $4)}

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

@ -19,7 +19,6 @@ type ast_node =
let infer_prefix = "__infer_ctl_" let infer_prefix = "__infer_ctl_"
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 message_const = "message"
let suggestion_const = "suggestion" let suggestion_const = "suggestion"

Write Preview
Loading…
Cancel
Save