Summary: The debugger in the middle of the evaluation makes working on that file difficult. Separating modules a bit, so that we can change the code easier. This is in preparation to trying to add aliases and witnesses to formulas in a next diff. Reviewed By: jvillard Differential Revision: D18708542 fbshipit-source-id: 523f30fc9master
Dulma Churchill
5 years ago
committed by
Facebook Github Bot
parent
c3e16dbdbc
commit
75794301dc
@ -0,0 +1,340 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the MIT license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree.
|
||||||
|
*)
|
||||||
|
open! IStd
|
||||||
|
module L = Logging
|
||||||
|
|
||||||
|
let pp_ast ~ast_node_to_highlight ?(prettifier = Fn.id) fmt root =
|
||||||
|
let open Ctl_parser_types in
|
||||||
|
let pp_node_info fmt an =
|
||||||
|
let name = Ctl_parser_types.ast_node_name an in
|
||||||
|
let typ = Ctl_parser_types.ast_node_type an in
|
||||||
|
let cast_kind = Ctl_parser_types.ast_node_cast_kind an in
|
||||||
|
Format.fprintf fmt " %s %s %s" name typ cast_kind
|
||||||
|
in
|
||||||
|
let rec pp_children pp_node wrapper fmt level nodes =
|
||||||
|
match nodes with
|
||||||
|
| [] ->
|
||||||
|
()
|
||||||
|
| node :: nodes ->
|
||||||
|
pp_node fmt (wrapper node) level "|-" ;
|
||||||
|
pp_children pp_node wrapper fmt level nodes
|
||||||
|
in
|
||||||
|
let rec pp_ast_aux fmt root level prefix =
|
||||||
|
let get_node_name (an : ast_node) =
|
||||||
|
match an with
|
||||||
|
| Stmt stmt ->
|
||||||
|
Clang_ast_proj.get_stmt_kind_string stmt
|
||||||
|
| Decl decl ->
|
||||||
|
Clang_ast_proj.get_decl_kind_string decl
|
||||||
|
in
|
||||||
|
let should_highlight =
|
||||||
|
match (root, ast_node_to_highlight) with
|
||||||
|
| Stmt r, Stmt n ->
|
||||||
|
phys_equal r n
|
||||||
|
| Decl r, Decl n ->
|
||||||
|
phys_equal r n
|
||||||
|
| _ ->
|
||||||
|
false
|
||||||
|
in
|
||||||
|
let node_name =
|
||||||
|
let node_name = get_node_name root in
|
||||||
|
if should_highlight then prettifier node_name else node_name
|
||||||
|
in
|
||||||
|
let spaces = String.make (level * String.length prefix) ' ' in
|
||||||
|
let next_level = level + 1 in
|
||||||
|
Format.fprintf fmt "%s%s%s %a@\n" spaces prefix node_name pp_node_info root ;
|
||||||
|
match root with
|
||||||
|
| Stmt (DeclStmt (_, stmts, ([VarDecl _] as var_decl))) ->
|
||||||
|
(* handling special case of DeclStmt with VarDecl: emit the VarDecl node
|
||||||
|
then emit the statements in DeclStmt as children of VarDecl. This is
|
||||||
|
because despite being equal, the statements inside VarDecl and those
|
||||||
|
inside DeclStmt belong to different instances, hence they fail the
|
||||||
|
phys_equal check that should colour them *)
|
||||||
|
pp_children pp_ast_aux (fun n -> Decl n) fmt next_level var_decl ;
|
||||||
|
pp_stmts fmt (next_level + 1) stmts
|
||||||
|
| Stmt stmt ->
|
||||||
|
let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in
|
||||||
|
pp_stmts fmt next_level stmts
|
||||||
|
| Decl decl ->
|
||||||
|
let decls =
|
||||||
|
Clang_ast_proj.get_decl_context_tuple decl
|
||||||
|
|> Option.map ~f:(fun (decls, _) -> decls)
|
||||||
|
|> Option.value ~default:[]
|
||||||
|
in
|
||||||
|
pp_decls fmt next_level decls
|
||||||
|
and pp_stmts fmt level stmts = pp_children pp_ast_aux (fun n -> Stmt n) fmt level stmts
|
||||||
|
and pp_decls fmt level decls = pp_children pp_ast_aux (fun n -> Decl n) fmt level decls in
|
||||||
|
pp_ast_aux fmt root 0 ""
|
||||||
|
|
||||||
|
|
||||||
|
module EvaluationTracker = struct
|
||||||
|
exception Empty_stack of string
|
||||||
|
|
||||||
|
type eval_result = Eval_undefined | Eval_true | Eval_false
|
||||||
|
|
||||||
|
type content =
|
||||||
|
{ ast_node: Ctl_parser_types.ast_node
|
||||||
|
; phi: CTLTypes.t
|
||||||
|
; lcxt: CLintersContext.context
|
||||||
|
; eval_result: eval_result
|
||||||
|
; witness: Ctl_parser_types.ast_node option }
|
||||||
|
|
||||||
|
type eval_node = {id: int; content: content}
|
||||||
|
|
||||||
|
type tree = Tree of eval_node * tree list
|
||||||
|
|
||||||
|
type ast_node_to_display =
|
||||||
|
(* the node can be used to describe further sub calls in the evaluation stack *)
|
||||||
|
| Carry_forward of Ctl_parser_types.ast_node
|
||||||
|
(* the node cannot be further used to describe sub calls in the evaluation stack *)
|
||||||
|
| Last_occurrence of Ctl_parser_types.ast_node
|
||||||
|
|
||||||
|
type t =
|
||||||
|
{ next_id: int
|
||||||
|
; eval_stack: (tree * ast_node_to_display) Stack.t
|
||||||
|
; forest: tree list
|
||||||
|
; breakpoint_line: int option
|
||||||
|
; debugger_active: bool }
|
||||||
|
|
||||||
|
let create_content ast_node phi lcxt =
|
||||||
|
{ast_node; phi; eval_result= Eval_undefined; lcxt; witness= None}
|
||||||
|
|
||||||
|
|
||||||
|
let create source_file =
|
||||||
|
let breakpoint_token = "INFER_BREAKPOINT" in
|
||||||
|
let breakpoint_line =
|
||||||
|
In_channel.read_lines (SourceFile.to_abs_path source_file)
|
||||||
|
|> List.findi ~f:(fun _ line -> String.is_substring line ~substring:breakpoint_token)
|
||||||
|
|> Option.map ~f:(fun (i, _) -> i + 1)
|
||||||
|
in
|
||||||
|
{next_id= 0; eval_stack= Stack.create (); forest= []; breakpoint_line; debugger_active= false}
|
||||||
|
|
||||||
|
|
||||||
|
let explain t ~eval_node ~ast_node_to_display =
|
||||||
|
let open Ctl_parser_types in
|
||||||
|
let line_number an =
|
||||||
|
let line_of_source_range (sr : Clang_ast_t.source_range) =
|
||||||
|
let loc_info, _ = sr in
|
||||||
|
loc_info.sl_line
|
||||||
|
in
|
||||||
|
match an with
|
||||||
|
| Stmt stmt ->
|
||||||
|
let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
|
||||||
|
line_of_source_range stmt_info.si_source_range
|
||||||
|
| Decl decl ->
|
||||||
|
let decl_info = Clang_ast_proj.get_decl_tuple decl in
|
||||||
|
line_of_source_range decl_info.di_source_range
|
||||||
|
in
|
||||||
|
let stop_and_explain_step () =
|
||||||
|
let highlight_style =
|
||||||
|
match eval_node.content.eval_result with
|
||||||
|
| Eval_undefined ->
|
||||||
|
ANSITerminal.[Bold]
|
||||||
|
| Eval_true ->
|
||||||
|
ANSITerminal.[Bold; green]
|
||||||
|
| Eval_false ->
|
||||||
|
ANSITerminal.[Bold; red]
|
||||||
|
in
|
||||||
|
let ast_node_to_highlight = eval_node.content.ast_node in
|
||||||
|
let ast_root, is_last_occurrence =
|
||||||
|
match ast_node_to_display with
|
||||||
|
| Carry_forward n ->
|
||||||
|
(n, false)
|
||||||
|
| Last_occurrence n ->
|
||||||
|
(n, true)
|
||||||
|
in
|
||||||
|
let witness_str =
|
||||||
|
match eval_node.content.witness with
|
||||||
|
| Some witness ->
|
||||||
|
"\n- witness: "
|
||||||
|
^ Ctl_parser_types.ast_node_kind witness
|
||||||
|
^ " "
|
||||||
|
^ Ctl_parser_types.ast_node_name witness
|
||||||
|
| None ->
|
||||||
|
""
|
||||||
|
in
|
||||||
|
let ast_str =
|
||||||
|
Format.asprintf "%a %s"
|
||||||
|
(pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
|
||||||
|
ast_root witness_str
|
||||||
|
in
|
||||||
|
L.progress "@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n"
|
||||||
|
eval_node.id (Stack.length t.eval_stack)
|
||||||
|
(Option.value_map ~default:"Unknown" ~f:string_of_int (line_number ast_node_to_highlight)) ;
|
||||||
|
let is_eval_result_undefined =
|
||||||
|
match eval_node.content.eval_result with Eval_undefined -> true | _ -> false
|
||||||
|
in
|
||||||
|
if is_last_occurrence && is_eval_result_undefined then
|
||||||
|
L.progress "From this step, a transition to a different part of the AST may follow.@\n" ;
|
||||||
|
let phi_str = Format.asprintf "%a" CTLTypes.pp_formula eval_node.content.phi in
|
||||||
|
L.progress "CTL Formula: %s@\n@\n" phi_str ;
|
||||||
|
L.progress "%s@\n" ast_str ;
|
||||||
|
let quit_token = "q" in
|
||||||
|
L.progress "Press Enter to continue or type %s to quit... @?" quit_token ;
|
||||||
|
match In_channel.input_line_exn In_channel.stdin |> String.lowercase with
|
||||||
|
| s when String.equal s quit_token ->
|
||||||
|
L.exit 0
|
||||||
|
| _ ->
|
||||||
|
(* Remove the line at the bottom of terminal with the debug instructions *)
|
||||||
|
let open ANSITerminal in
|
||||||
|
(* move one line up, as current line is the one generated by pressing enter *)
|
||||||
|
move_cursor 0 (-1) ;
|
||||||
|
move_bol () ;
|
||||||
|
(* move to the beginning of the line *)
|
||||||
|
erase Below
|
||||||
|
(* erase what follows the cursor's position *)
|
||||||
|
in
|
||||||
|
match (t.debugger_active, t.breakpoint_line, line_number eval_node.content.ast_node) with
|
||||||
|
| false, Some break_point_ln, Some ln when ln >= break_point_ln ->
|
||||||
|
L.progress "Attaching debugger at line %d" ln ;
|
||||||
|
stop_and_explain_step () ;
|
||||||
|
{t with debugger_active= true}
|
||||||
|
| true, _, _ ->
|
||||||
|
stop_and_explain_step () ; t
|
||||||
|
| _ ->
|
||||||
|
t
|
||||||
|
|
||||||
|
|
||||||
|
let eval_begin t content =
|
||||||
|
let node = {id= t.next_id; content} in
|
||||||
|
let create_subtree root = Tree (root, []) in
|
||||||
|
let subtree' = create_subtree node in
|
||||||
|
let ast_node_from_previous_call =
|
||||||
|
match Stack.top t.eval_stack with
|
||||||
|
| Some (_, Last_occurrence _) ->
|
||||||
|
content.ast_node
|
||||||
|
| Some (_, Carry_forward an) ->
|
||||||
|
an
|
||||||
|
| None ->
|
||||||
|
content.ast_node
|
||||||
|
in
|
||||||
|
let ast_node_to_display =
|
||||||
|
if CTLTypes.has_transition content.phi then Last_occurrence ast_node_from_previous_call
|
||||||
|
else Carry_forward ast_node_from_previous_call
|
||||||
|
in
|
||||||
|
Stack.push t.eval_stack (subtree', ast_node_to_display) ;
|
||||||
|
let t' = explain t ~eval_node:node ~ast_node_to_display in
|
||||||
|
{t' with next_id= t.next_id + 1}
|
||||||
|
|
||||||
|
|
||||||
|
let eval_end t result =
|
||||||
|
let result_bool = Option.is_some result in
|
||||||
|
let eval_result_of_bool = function true -> Eval_true | false -> Eval_false in
|
||||||
|
if Stack.is_empty t.eval_stack then
|
||||||
|
raise (Empty_stack "Unbalanced number of eval_begin/eval_end invocations") ;
|
||||||
|
let evaluated_tree, eval_node, ast_node_to_display =
|
||||||
|
match Stack.pop_exn t.eval_stack with
|
||||||
|
| Tree (({id= _; content} as eval_node), children), ast_node_to_display ->
|
||||||
|
let content' =
|
||||||
|
{content with eval_result= eval_result_of_bool result_bool; witness= result}
|
||||||
|
in
|
||||||
|
let eval_node' = {eval_node with content= content'} in
|
||||||
|
(Tree (eval_node', children), eval_node', ast_node_to_display)
|
||||||
|
in
|
||||||
|
let t' = explain t ~eval_node ~ast_node_to_display in
|
||||||
|
let forest' =
|
||||||
|
if Stack.is_empty t'.eval_stack then evaluated_tree :: t'.forest
|
||||||
|
else
|
||||||
|
let parent =
|
||||||
|
match Stack.pop_exn t'.eval_stack with
|
||||||
|
| Tree (node, children), ntd ->
|
||||||
|
(Tree (node, evaluated_tree :: children), ntd)
|
||||||
|
in
|
||||||
|
Stack.push t'.eval_stack parent ; t'.forest
|
||||||
|
in
|
||||||
|
{t' with forest= forest'}
|
||||||
|
|
||||||
|
|
||||||
|
let equal_ast_node = Poly.equal
|
||||||
|
|
||||||
|
module DottyPrinter = struct
|
||||||
|
let dotty_of_ctl_evaluation t =
|
||||||
|
let open CTLTypes in
|
||||||
|
let open Ctl_parser_types in
|
||||||
|
let buffer_content buf =
|
||||||
|
let result = Buffer.contents buf in
|
||||||
|
Buffer.reset buf ; result
|
||||||
|
in
|
||||||
|
let dotty_of_tree cluster_id tree =
|
||||||
|
let get_root tree = match tree with Tree (root, _) -> root in
|
||||||
|
let get_children tree = match tree with Tree (_, children) -> List.rev children in
|
||||||
|
(* shallow: emit dotty about root node and edges to its children *)
|
||||||
|
let shallow_dotty_of_tree tree =
|
||||||
|
let root_node = get_root tree in
|
||||||
|
let children = get_children tree in
|
||||||
|
let edge child_node =
|
||||||
|
if equal_ast_node root_node.content.ast_node child_node.content.ast_node then
|
||||||
|
Printf.sprintf "%d -> %d [style=dotted]" root_node.id child_node.id
|
||||||
|
else Printf.sprintf "%d -> %d [style=bold]" root_node.id child_node.id
|
||||||
|
in
|
||||||
|
let color =
|
||||||
|
match root_node.content.eval_result with
|
||||||
|
| Eval_true ->
|
||||||
|
"green"
|
||||||
|
| Eval_false ->
|
||||||
|
"red"
|
||||||
|
| _ ->
|
||||||
|
L.(die InternalError) "Tree is not fully evaluated"
|
||||||
|
in
|
||||||
|
let label =
|
||||||
|
let string_of_lcxt c =
|
||||||
|
match c.CLintersContext.et_evaluation_node with
|
||||||
|
| Some s ->
|
||||||
|
"et_evaluation_node = " ^ s
|
||||||
|
| _ ->
|
||||||
|
"et_evaluation_node = NONE"
|
||||||
|
in
|
||||||
|
let string_of_ast_node an =
|
||||||
|
match an with
|
||||||
|
| Stmt stmt ->
|
||||||
|
Clang_ast_proj.get_stmt_kind_string stmt
|
||||||
|
| Decl decl ->
|
||||||
|
Clang_ast_proj.get_decl_kind_string decl
|
||||||
|
in
|
||||||
|
let smart_string_of_formula phi =
|
||||||
|
let num_children = List.length children in
|
||||||
|
match phi with
|
||||||
|
| And _ when Int.equal num_children 2 ->
|
||||||
|
"(...) AND (...)"
|
||||||
|
| Or _ when Int.equal num_children 2 ->
|
||||||
|
"(...) OR (...)"
|
||||||
|
| Implies _ when Int.equal num_children 2 ->
|
||||||
|
"(...) ==> (...)"
|
||||||
|
| Not _ ->
|
||||||
|
"NOT(...)"
|
||||||
|
| _ ->
|
||||||
|
Format.asprintf "%a" CTLTypes.pp_formula phi
|
||||||
|
in
|
||||||
|
Format.sprintf "(%d)\\n%s\\n%s\\n%s" root_node.id
|
||||||
|
(Escape.escape_dotty (string_of_ast_node root_node.content.ast_node))
|
||||||
|
(Escape.escape_dotty (string_of_lcxt root_node.content.lcxt))
|
||||||
|
(Escape.escape_dotty (smart_string_of_formula root_node.content.phi))
|
||||||
|
in
|
||||||
|
let edges =
|
||||||
|
let buf = Buffer.create 16 in
|
||||||
|
List.iter
|
||||||
|
~f:(fun subtree -> Buffer.add_string buf (edge (get_root subtree) ^ "\n"))
|
||||||
|
children ;
|
||||||
|
buffer_content buf
|
||||||
|
in
|
||||||
|
Printf.sprintf "%d [label=\"%s\" shape=box color=%s]\n%s\n" root_node.id label color edges
|
||||||
|
in
|
||||||
|
let rec traverse buf tree =
|
||||||
|
Buffer.add_string buf (shallow_dotty_of_tree tree) ;
|
||||||
|
List.iter ~f:(traverse buf) (get_children tree)
|
||||||
|
in
|
||||||
|
let buf = Buffer.create 16 in
|
||||||
|
traverse buf tree ;
|
||||||
|
Printf.sprintf "subgraph cluster_%d {\n%s\n}" cluster_id (buffer_content buf)
|
||||||
|
in
|
||||||
|
let buf = Buffer.create 16 in
|
||||||
|
List.iteri
|
||||||
|
~f:(fun cluster_id tree -> Buffer.add_string buf (dotty_of_tree cluster_id tree ^ "\n"))
|
||||||
|
(List.rev t.forest) ;
|
||||||
|
Printf.sprintf "digraph CTL_Evaluation {\n%s\n}\n" (buffer_content buf)
|
||||||
|
end
|
||||||
|
end
|
||||||
@ -0,0 +1,48 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the MIT license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree.
|
||||||
|
*)
|
||||||
|
|
||||||
|
open! IStd
|
||||||
|
|
||||||
|
module EvaluationTracker : sig
|
||||||
|
type eval_result = Eval_undefined | Eval_true | Eval_false
|
||||||
|
|
||||||
|
type content =
|
||||||
|
{ ast_node: Ctl_parser_types.ast_node
|
||||||
|
; phi: CTLTypes.t
|
||||||
|
; lcxt: CLintersContext.context
|
||||||
|
; eval_result: eval_result
|
||||||
|
; witness: Ctl_parser_types.ast_node option }
|
||||||
|
|
||||||
|
type eval_node = {id: int; content: content}
|
||||||
|
|
||||||
|
type tree = Tree of eval_node * tree list
|
||||||
|
|
||||||
|
type ast_node_to_display =
|
||||||
|
(* the node can be used to describe further sub calls in the evaluation stack *)
|
||||||
|
| Carry_forward of Ctl_parser_types.ast_node
|
||||||
|
(* the node cannot be further used to describe sub calls in the evaluation stack *)
|
||||||
|
| Last_occurrence of Ctl_parser_types.ast_node
|
||||||
|
|
||||||
|
type t =
|
||||||
|
{ next_id: int
|
||||||
|
; eval_stack: (tree * ast_node_to_display) Stack.t
|
||||||
|
; forest: tree list
|
||||||
|
; breakpoint_line: int option
|
||||||
|
; debugger_active: bool }
|
||||||
|
|
||||||
|
val create : SourceFile.t -> t
|
||||||
|
|
||||||
|
val create_content : Ctl_parser_types.ast_node -> CTLTypes.t -> CLintersContext.context -> content
|
||||||
|
|
||||||
|
val eval_begin : t -> content -> t
|
||||||
|
|
||||||
|
val eval_end : t -> Ctl_parser_types.ast_node option -> t
|
||||||
|
|
||||||
|
module DottyPrinter : sig
|
||||||
|
val dotty_of_ctl_evaluation : t -> string
|
||||||
|
end
|
||||||
|
end
|
||||||
@ -0,0 +1,62 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the MIT license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree.
|
||||||
|
*)
|
||||||
|
|
||||||
|
open! IStd
|
||||||
|
|
||||||
|
(**
|
||||||
|
This module defines a language to define checkers. These checkers are interpreted over the AST of
|
||||||
|
the program. A checker is defined by a CTL formula which expresses a condition saying when the
|
||||||
|
checker should report a problem.
|
||||||
|
*)
|
||||||
|
|
||||||
|
(** "set" clauses are used for defining mandatory variables that will be used
|
||||||
|
by when reporting issues: eg for defining the condition.
|
||||||
|
|
||||||
|
"desc" clauses are used for defining the error message,
|
||||||
|
the suggestion, the severity.
|
||||||
|
|
||||||
|
"let" clauses are used to define temporary formulas which are then
|
||||||
|
used to abbreviate the another formula. For example
|
||||||
|
|
||||||
|
let f = a And B
|
||||||
|
|
||||||
|
set formula = f OR f
|
||||||
|
|
||||||
|
set message = "bla"
|
||||||
|
|
||||||
|
*)
|
||||||
|
|
||||||
|
type clause =
|
||||||
|
| CLet of ALVar.formula_id * ALVar.t list * CTLTypes.t (** Let clause: let id = definifion; *)
|
||||||
|
| CSet of ALVar.keyword * CTLTypes.t (** Set clause: set id = definition *)
|
||||||
|
| CDesc of ALVar.keyword * string (** Description clause eg: set message = "..." *)
|
||||||
|
| CPath of [`WhitelistPath | `BlacklistPath] * ALVar.t list
|
||||||
|
|
||||||
|
type ctl_checker =
|
||||||
|
{id: string (** Checker's id *); definitions: clause list (** A list of let/set definitions *)}
|
||||||
|
|
||||||
|
type al_file =
|
||||||
|
{ import_files: string list
|
||||||
|
; global_macros: clause list
|
||||||
|
; global_paths: (string * ALVar.alexp list) list
|
||||||
|
; checkers: ctl_checker list }
|
||||||
|
|
||||||
|
val print_checker : ctl_checker -> unit
|
||||||
|
|
||||||
|
val eval_formula :
|
||||||
|
CTLTypes.t
|
||||||
|
-> Ctl_parser_types.ast_node
|
||||||
|
-> CLintersContext.context
|
||||||
|
-> Ctl_parser_types.ast_node option
|
||||||
|
(** return the evaluation of the formula and a witness *)
|
||||||
|
|
||||||
|
val save_dotty_when_in_debug_mode : SourceFile.t -> unit
|
||||||
|
|
||||||
|
val next_state_via_transition :
|
||||||
|
Ctl_parser_types.ast_node -> CTLTypes.transitions -> Ctl_parser_types.ast_node list
|
||||||
|
|
||||||
|
val create_ctl_evaluation_tracker : SourceFile.t -> unit
|
||||||
@ -0,0 +1,177 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the MIT license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree.
|
||||||
|
*)
|
||||||
|
|
||||||
|
open! IStd
|
||||||
|
|
||||||
|
(** Transition labels used for example to switch from decl to stmt *)
|
||||||
|
type transitions =
|
||||||
|
| AccessorForProperty of ALVar.alexp (** decl to decl *)
|
||||||
|
| Body (** decl to stmt *)
|
||||||
|
| FieldName of ALVar.alexp (** stmt to stmt, decl to decl *)
|
||||||
|
| Fields (** stmt to stmt, decl to decl *)
|
||||||
|
| InitExpr (** decl to stmt *)
|
||||||
|
| Super (** decl to decl *)
|
||||||
|
| ParameterName of ALVar.alexp (** stmt to stmt, decl to decl *)
|
||||||
|
| ParameterPos of ALVar.alexp (** stmt to stmt, decl to decl *)
|
||||||
|
| Parameters (** stmt to stmt, decl to decl *)
|
||||||
|
| Cond
|
||||||
|
| PointerToDecl (** stmt to decl *)
|
||||||
|
| Protocol (** decl to decl *)
|
||||||
|
| Sibling (** decl to decl *)
|
||||||
|
| SourceExpr
|
||||||
|
[@@deriving compare]
|
||||||
|
|
||||||
|
let is_transition_to_successor trans =
|
||||||
|
match trans with
|
||||||
|
| Body
|
||||||
|
| InitExpr
|
||||||
|
| FieldName _
|
||||||
|
| Fields
|
||||||
|
| ParameterName _
|
||||||
|
| ParameterPos _
|
||||||
|
| Parameters
|
||||||
|
| Cond
|
||||||
|
| SourceExpr ->
|
||||||
|
true
|
||||||
|
| Super | PointerToDecl | Protocol | AccessorForProperty _ | Sibling ->
|
||||||
|
false
|
||||||
|
|
||||||
|
|
||||||
|
(* In formulas below prefix
|
||||||
|
"E" means "exists a path"
|
||||||
|
"A" means "for all path" *)
|
||||||
|
|
||||||
|
type t =
|
||||||
|
(* A ctl formula *)
|
||||||
|
| True
|
||||||
|
| False
|
||||||
|
(* not really necessary but it makes it evaluation faster *)
|
||||||
|
| Atomic of CPredicates.t
|
||||||
|
| Not of t
|
||||||
|
| And of t * t
|
||||||
|
| Or of t * t
|
||||||
|
| Implies of t * t
|
||||||
|
| InNode of ALVar.alexp list * t
|
||||||
|
| AX of transitions option * t
|
||||||
|
| EX of transitions option * t
|
||||||
|
| AF of transitions option * t
|
||||||
|
| EF of transitions option * t
|
||||||
|
| AG of transitions option * t
|
||||||
|
| EG of transitions option * t
|
||||||
|
| AU of transitions option * t * t
|
||||||
|
| EU of transitions option * t * t
|
||||||
|
| EH of ALVar.alexp list * t
|
||||||
|
| ET of ALVar.alexp list * transitions option * t
|
||||||
|
| InObjCClass of t * t
|
||||||
|
[@@deriving compare]
|
||||||
|
|
||||||
|
let equal = [%compare.equal: t]
|
||||||
|
|
||||||
|
let has_transition phi =
|
||||||
|
match phi with
|
||||||
|
| True | False | Atomic _ | Not _ | And _ | Or _ | Implies _ | InNode _ | EH _ | InObjCClass _ ->
|
||||||
|
false
|
||||||
|
| AX (trans_opt, _)
|
||||||
|
| AF (trans_opt, _)
|
||||||
|
| AG (trans_opt, _)
|
||||||
|
| AU (trans_opt, _, _)
|
||||||
|
| EX (trans_opt, _)
|
||||||
|
| EF (trans_opt, _)
|
||||||
|
| EG (trans_opt, _)
|
||||||
|
| EU (trans_opt, _, _)
|
||||||
|
| ET (_, trans_opt, _) ->
|
||||||
|
Option.is_some trans_opt
|
||||||
|
|
||||||
|
|
||||||
|
let pp_transition fmt trans_opt =
|
||||||
|
let pp_aux fmt trans =
|
||||||
|
match trans with
|
||||||
|
| AccessorForProperty kind ->
|
||||||
|
Format.pp_print_string fmt ("AccessorForProperty " ^ ALVar.alexp_to_string kind)
|
||||||
|
| Body ->
|
||||||
|
Format.pp_print_string fmt "Body"
|
||||||
|
| FieldName name ->
|
||||||
|
Format.pp_print_string fmt ("FieldName " ^ ALVar.alexp_to_string name)
|
||||||
|
| Fields ->
|
||||||
|
Format.pp_print_string fmt "Fields"
|
||||||
|
| InitExpr ->
|
||||||
|
Format.pp_print_string fmt "InitExpr"
|
||||||
|
| Super ->
|
||||||
|
Format.pp_print_string fmt "Super"
|
||||||
|
| ParameterName name ->
|
||||||
|
Format.pp_print_string fmt ("ParameterName " ^ ALVar.alexp_to_string name)
|
||||||
|
| ParameterPos pos ->
|
||||||
|
Format.pp_print_string fmt ("ParameterPos " ^ ALVar.alexp_to_string pos)
|
||||||
|
| Parameters ->
|
||||||
|
Format.pp_print_string fmt "Parameters"
|
||||||
|
| Cond ->
|
||||||
|
Format.pp_print_string fmt "Cond"
|
||||||
|
| Protocol ->
|
||||||
|
Format.pp_print_string fmt "Protocol"
|
||||||
|
| PointerToDecl ->
|
||||||
|
Format.pp_print_string fmt "PointerToDecl"
|
||||||
|
| Sibling ->
|
||||||
|
Format.pp_print_string fmt "Sibling"
|
||||||
|
| SourceExpr ->
|
||||||
|
Format.pp_print_string fmt "SourceExpr"
|
||||||
|
in
|
||||||
|
match trans_opt with Some trans -> pp_aux fmt trans | None -> Format.pp_print_char fmt '_'
|
||||||
|
|
||||||
|
|
||||||
|
(* a flag to print more or less in the dotty graph *)
|
||||||
|
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.pp_print_string fmt "True"
|
||||||
|
| False ->
|
||||||
|
Format.pp_print_string fmt "False"
|
||||||
|
| Atomic p ->
|
||||||
|
CPredicates.pp_predicate fmt p
|
||||||
|
| Not phi ->
|
||||||
|
if full_print then Format.fprintf fmt "NOT(%a)" pp_formula phi
|
||||||
|
else Format.pp_print_string fmt "NOT(...)"
|
||||||
|
| And (phi1, phi2) ->
|
||||||
|
if full_print then Format.fprintf fmt "(%a AND %a)" pp_formula phi1 pp_formula phi2
|
||||||
|
else Format.pp_print_string fmt "(... AND ...)"
|
||||||
|
| Or (phi1, phi2) ->
|
||||||
|
if full_print then Format.fprintf fmt "(%a OR %a)" pp_formula phi1 pp_formula phi2
|
||||||
|
else Format.pp_print_string 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)
|
||||||
|
(nodes_to_string nl) pp_formula phi
|
||||||
|
| AX (trs, phi) ->
|
||||||
|
Format.fprintf fmt "AX[->%a](%a)" pp_transition trs pp_formula phi
|
||||||
|
| EX (trs, phi) ->
|
||||||
|
Format.fprintf fmt "EX[->%a](%a)" pp_transition trs pp_formula phi
|
||||||
|
| AF (trs, phi) ->
|
||||||
|
Format.fprintf fmt "AF[->%a](%a)" pp_transition trs pp_formula phi
|
||||||
|
| EF (trs, phi) ->
|
||||||
|
Format.fprintf fmt "EF[->%a](%a)" pp_transition trs pp_formula phi
|
||||||
|
| AG (trs, phi) ->
|
||||||
|
Format.fprintf fmt "AG[->%a](%a)" pp_transition trs pp_formula phi
|
||||||
|
| EG (trs, phi) ->
|
||||||
|
Format.fprintf fmt "EG[->%a](%a)" pp_transition trs pp_formula phi
|
||||||
|
| AU (trs, phi1, phi2) ->
|
||||||
|
Format.fprintf fmt "A[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
|
||||||
|
| 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)
|
||||||
|
(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)
|
||||||
|
(nodes_to_string arglist) pp_transition trans pp_formula phi
|
||||||
|
| InObjCClass (phi1, phi2) ->
|
||||||
|
if full_print then Format.fprintf fmt "InObjCClass(%a, %a)" pp_formula phi1 pp_formula phi2
|
||||||
Loading…
Reference in new issue