Previous  Up  

Functor CfLazyModelChecker.Make_Lazy_Model_Checker


module Make_Lazy_Model_Checker: functor (Abstraction : sig  end) -> sig  end
Parameters:
Abstraction : sig end 
module Abstraction: sig  end
module Region: sig  end
module Operation: sig  end
module Tree: sig  end

type error_path = Region.t *
Operation.t list *
Region.t 
val fprintf : (unit, Format.formatter, unit) format -> unit
val valOf : 'a option -> 'a
module IntMap: sig  end

type node_set = tree_node
IntMap.t

type 'a node_map = (tree_node * 'a)
IntMap.t

type summary_path =
| ListPath of tree_node list
| ConsPath of summary_path
* summary_path


type pt_data = summary_path

type entry_node = {
   mutable call_sites : Region.t
node_map;
   mutable exit_pts : pt_data
node_map;
}

type exit_node = {
   mutable entry_pts : pt_data
node_map;
}

type node_kind =
| Node
| Entry of entry_node
| Exit of exit_node


type marking_data = {
   mutable time_stamp : int;
   mutable region : Region.t;
   mutable call_time_stamp : int option;
}
Information that interests us about a dag node. The time stamp ts of a processed covered node indicates that this node is covered by processed uncovered nodes of time stamp lesser than ts. Conversely, the time stamp ts of processed uncovered node indicates that this node may partially cover any processed covered of time stamp greater than ts.


type marking =
| Unprocessed
| Processed_Covered of marking_data
| Processed_Uncovered of marking_data
| Processed_Was_Covered_To_Reprocess of marking_data


type node_data = {
   id : int;
   mutable mark : marking;
   kind : node_kind;
}

type summary_data = {
   path : summary_path;
   n_in : tree_node;
   n_out : tree_node;
}

type edge =
| SummaryEdge of summary_data
| PathEdge of Operation.t


type tree_node = (node_data,
edge)
Tree.node

type flat_tree_node = (node_data,
Operation.t)
Tree.node 
val print_marking_data : Format.formatter ->
       marking_data -> unit
val print_marking : Format.formatter ->
       marking -> unit
val print_marking_short : Format.formatter ->
       marking -> unit
val print_node_data : Format.formatter ->
       node_data -> unit
val print_option : ('a -> unit) -> Format.formatter -> 'a option -> unit
val print_node : Format.formatter ->
       (node_data,
        edge)
       Tree.node -> unit
val tree_node_table : (int, tree_node Pervasives.ref)
       Hashtbl.t
val get_node_data : ('a, 'b) Tree.node -> 'a
val edge_to_op : edge ->
       Operation.t
val get_edge_op : ('a, edge)
       Tree.incoming_edge ->
       Operation.t
val get_op : ('a, edge)
       Tree.node ->
       Operation.t
val get_parent : ('a, 'b) Tree.node ->
       ('a, 'b) Tree.node
val get_parent_edge : ('a, 'b) Tree.node -> 'b
val get_children : ('a, 'b) Tree.node ->
       ('a, 'b) Tree.node list
val get_id : (node_data, 'a)
       Tree.node -> int
val get_marking : (node_data, 'a)
       Tree.node ->
       marking
val get_marking_data : (node_data, 'a)
       Tree.node ->
       marking_data
val get_time_stamp : (node_data, 'a)
       Tree.node -> int
val min : 'a -> 'a -> 'a
val max : 'a -> 'a -> 'a
val update_caller : (node_data, 'a)
       Tree.node -> int option -> unit
val called_after : marking_data -> int -> bool
val print_tree_node : Format.formatter ->
       (node_data,
        edge)
       Tree.node -> unit
val node_equal : (node_data, 'a)
       Tree.node ->
       (node_data, 'b)
       Tree.node -> bool
val get_kind : (node_data, 'a)
       Tree.node ->
       node_kind
val get_entry : (node_data, 'a)
       Tree.node ->
       entry_node
val get_exit : (node_data, 'a)
       Tree.node ->
       exit_node
val get_region : (node_data, 'a)
       Tree.node ->
       Region.t
val get_region_opt : (node_data, 'a)
       Tree.node ->
       Region.t option

type nset = tree_node
IntMap.t 
val nset_empty : 'a IntMap.t
val nset_add : (node_data, 'a)
       Tree.node
       IntMap.t ->
       (node_data, 'a)
       Tree.node ->
       (node_data, 'a)
       Tree.node
       IntMap.t
val nset_mem : 'a IntMap.t ->
       (node_data, 'b)
       Tree.node -> bool
val nset_remove : 'a IntMap.t ->
       (node_data, 'b)
       Tree.node ->
       'a IntMap.t
val nset_iter : ('a -> unit) ->
       'a IntMap.t -> unit
val nset_map : ('a -> 'b) ->
       'c IntMap.t ->
       ('a -> 'b) IntMap.t
val nset_fold : ('a -> 'b -> 'a) ->
       'a -> 'b IntMap.t -> 'a
val nset_choose : 'a IntMap.t -> 'a option
val nset_filter : ((node_data, 'a)
        Tree.node -> bool) ->
       (node_data, 'a)
       Tree.node
       IntMap.t ->
       (node_data, 'a)
       Tree.node
       IntMap.t
val nset_join : (node_data, 'a)
       Tree.node
       IntMap.t ->
       (node_data, 'a)
       Tree.node
       IntMap.t ->
       (node_data, 'a)
       Tree.node
       IntMap.t
val nset_to_list : node_set ->
       (node_data,
        edge)
       Tree.node list
val nset_size : 'a IntMap.t -> int
val nmap_empty : 'a IntMap.t
val nmap_add : ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t ->
       (node_data, 'a)
       Tree.node ->
       'b ->
       ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t
val nmap_mem : 'a IntMap.t ->
       (node_data, 'b)
       Tree.node -> bool
val nmap_remove : 'a IntMap.t ->
       (node_data, 'b)
       Tree.node ->
       'a IntMap.t
val nmap_iter : ('a -> 'b -> unit) ->
       ('a * 'b) IntMap.t -> unit
val nmap_map : ('a -> 'b) ->
       'c IntMap.t ->
       ('d * 'a -> 'd * 'b) IntMap.t
val nmap_fold : ('a -> 'b -> 'c -> 'a) ->
       'a -> ('b * 'c) IntMap.t -> 'a
val nmap_filter : ((node_data, 'a)
        Tree.node -> 'b -> bool) ->
       ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t ->
       ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t
val nmap_join : ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t ->
       ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t ->
       ((node_data, 'a)
        Tree.node * 'b)
       IntMap.t
val nmap_to_list : pt_data
       node_map ->
       (tree_node *
        pt_data)
       list
val nmap_size : ('a * 'b) IntMap.t -> int
val nmap_isEmpty : ('a * 'b) IntMap.t -> bool
val nmap_choose : ('a -> bool) ->
       ('b * 'a) IntMap.t -> 'b option
class tree_node_creator : object  end
val entry_pts_node : (node_data,
        edge)
       Tree.node ->
       ((node_data,
         edge)
        Tree.node *
        summary_path)
       list
val single_child : ('a, 'b) Tree.node ->
       ('a, 'b) Tree.node
val single_child_edge : ('a, 'b) Tree.node -> 'b
val parent_edge : ('a, 'b) Tree.node -> 'b
val tlSafe : 'a list -> 'a list
val exit_pts_node : (node_data,
        edge)
       Tree.node ->
       ((node_data,
         edge)
        Tree.node *
        summary_path)
       list
exception RestartException
val stats_nb_iterations : int Pervasives.ref
val stats_nb_iterations_of_outer_loop : int Pervasives.ref
val stats_nb_created_nodes : int Pervasives.ref
val stats_nb_refinment_processes : int Pervasives.ref
val stats_nb_refined_nodes : int Pervasives.ref
val stats_nb_proof_tree_nodes : int Pervasives.ref
val stats_nb_proof_tree_covered_nodes : int Pervasives.ref
val stats_nb_deleted_nodes : int Pervasives.ref
val reset_stats : unit
val print_stats : Format.formatter -> unit -> unit

Model checker data types *

include BlastArch.ModelCheckOutcome

type model_check_outcome = error_path outcome 
exception Exit_from_check_concurrent_access of model_check_outcome

type 'a currentApproximation = {
   read_whole : Region.t;
   write_whole : Region.t;
   read_accesses : ('a * Region.t) list;
   write_accesses : ('a * Region.t) list;
}

type raceKind =
| Read
| Write
| Both
| NoDistinction 

exception RaceConditionException of model_check_outcome

Data structures to hold the phi's for lvalues *

val global_variable_table : Abstraction.phi_table
val iter_global_variables : (Ast.Expression.lval ->
        Abstraction.Region.t
        Pervasives.ref -> unit) ->
       unit
val get_global_var_phi : Ast.Expression.lval ->
       Abstraction.Region.t
       Pervasives.ref
val global_lock_asm_table : (Ast.Expression.lval,
        Abstraction.Region.t)
       Hashtbl.t
val process_env_assumptions : (Ast.Expression.lval * Ast.Predicate.predicate) list -> unit
val print_phis : bool -> string

type error_check =
| EmptyErrorAtNode of Region.t
* tree_node
* tree_node list
* tree_node list
| NonEmptyErrorAtRoot of Region.t
* tree_node
* tree_node list


Checks whether a reached error region corresponds to a real error path. This function takes a node and an error region contained in the node's region as arguments, and does a backward pre computation from that node, along the branch from the root to that node, until it gets an empty region or reaches the root. It returns the obtained region at the reached ancestor along with the path from this ancestor to the initial node. 



val is_entry : (node_data, 'a)
       Tree.node -> bool
val get_outgoing : ('a, edge)
       Tree.node ->
       Operation.t
val expand_summary_path : summary_path ->
       tree_node list
val expand_path_with_old : (node_data,
        edge)
       Tree.node list ->
       ((node_data,
         edge)
        Tree.node,
        edge)
       Tree.node list
val expand_path : (node_data,
        edge)
       Tree.node list ->
       (node_data,
        edge)
       Tree.node list
val path_to_root : (node_data,
        edge)
       Tree.node ->
       (node_data,
        edge)
       Tree.node list
val check_error : tree_node ->
       Region.t ->
       error_check
val refine_path : (node_data,
        edge)
       Tree.node ->
       (node_data,
        edge)
       Tree.node list -> unit
val add_pt : ('a,
        (node_data, 'b)
        Tree.node
        IntMap.t)
       Hashtbl.t ->
       'a ->
       (node_data, 'b)
       Tree.node -> unit
val has_pt : ('a, 'b IntMap.t) Hashtbl.t ->
       'a ->
       (node_data, 'c)
       Tree.node -> bool
val remove_pt : ('a, 'b IntMap.t) Hashtbl.t ->
       'a ->
       (node_data, 'c)
       Tree.node -> unit
val clear_pts : ('a, 'b) Hashtbl.t -> unit
val get_pts : ('a, 'b IntMap.t) Hashtbl.t ->
       'a -> 'b IntMap.t
val iter_pts : ('a -> 'b -> unit) -> ('a, 'b) Hashtbl.t -> unit
val print_summaries : Format.formatter ->
       (string,
        (node_data,
         edge)
        Tree.node
        IntMap.t)
       Hashtbl.t -> unit
val update_tree_after_refinment : (string,
        (node_data,
         edge)
        Tree.node
        IntMap.t)
       Hashtbl.t ->
       < add_element : (node_data,
                        edge)
                       Tree.node -> 
                       unit;
         .. > ->
       int ->
       (node_data,
        edge)
       Tree.node
       Region.coverers -> unit

type proof_tree_node_data = {
   pt_id : int;
   pt_region : Abstraction.proof_region;
   covering_nodes : (Abstraction.lemma_index *
proof_tree_node Pervasives.ref
list)
option;
}

type proof_tree_edge = Operation.t *
Abstraction.lemma_index

type proof_tree_node = (proof_tree_node_data,
proof_tree_edge)
Tree.node 
val print_proof_tree : proof_tree_node -> unit
val count_tree_nodes : ('a, 'b) Tree.node -> unit
val build_proof_tree : unit ->
       (node_data,
        edge)
       Tree.node -> unit
val dumptrace : 'a *
       Abstraction.Operation.t list *
       Region.t list -> unit
val dumppath : (node_data,
        edge)
       Tree.node ->
       Region.t -> unit
val dump_trace_to_node : (node_data,
        edge)
       Tree.node ->
       Region.t -> 'a -> unit
val demo_process : (node_data,
        edge)
       Tree.node ->
       Region.t -> bool -> unit
val model_check : Region.t ->
       Region.t option ->
       (Region.t *
        Operation.t list *
        Region.t)
       outcome