Previous  Up  Next

Module Commands

module Commands: sig .. end
Representation of program commands
type can_goto =
| Cgo_break of int
| Cgo_continue of int
| Cgo_return
Kind of branches
type fld_assignments = (Exp.exp * Misc.component * Exp.exp) list
Field assignments
type read_memory_order =
| Crmo_nonatomic
| Crmo_relaxed
| Crmo_acquire
| Crmo_seq_cst
Kind of memory orders
type write_memory_order =
| Cwmo_nonatomic
| Cwmo_relaxed of (Misc.component * Misc.component * Exp.exp list) option
| Cwmo_release of (Misc.component * Misc.component * Exp.exp list) option
| Cwmo_seq_cst of (Misc.component * Misc.component * Exp.exp list) option 
type cas_memory_order =
| Ccmo_seq_cst
| Ccmo_rel_acq
| Ccmo_release
| Ccmo_acquire
| Ccmo_relaxed 
type fun_info = {
   fun_param : Exp.Id.t list * Exp.Id.t list; (*formal parameters (by reference, by value)*)
   fun_modif : Exp.IdSet.t; (*modified variables*)
   fun_pre : Assertions.cprop; (*precondition*)
   fun_post : Assertions.cprop; (*postcondition*)
   fun_loc : Location.t; (*location for error messages*)
}
Information about function declarations
type can_stmt = {
   can_st_desc : can_st_desc; (*statement descriptor*)
   mutable can_st_lv : Exp.IdSet.t; (*set of live variables*)
   can_st_loc : Location.t; (*location for error messages*)
}
Canonical statement
type can_cmd = can_stmt list
Canonical command: sequence of statements
type can_st_desc =
| Cst_nondet of can_cmd * can_cmd
| Cst_kill of Exp.IdSet.t
| Cst_assign of Exp.Id.t * Exp.exp
| Cst_fldlookup of Misc.component list * Exp.Id.t * Exp.exp * Misc.component
* read_memory_order
| Cst_fldassign of Misc.component list * fld_assignments
* (string * Assertions.cprop) list Pervasives.ref
* write_memory_order
| Cst_cas of Misc.component list * Exp.Id.t * Exp.exp * Misc.component * Exp.exp *
Exp.exp * cas_memory_order * read_memory_order
| Cst_new of Exp.Id.t * Exp.exp
| Cst_dispose of Exp.exp * Exp.exp
| Cst_pfcall of (Exp.Id.t option * string * fun_info * Exp.Id.t list * Exp.exp list)
list
| Cst_fcall2 of Exp.IdSet.t * Assertions.cprop * Assertions.cprop * string
| Cst_assume of Assertions.cprop
| Cst_assume_exp of Exp.exp
| Cst_assert_exp of Exp.exp
| Cst_interfere of Misc.component * string
| Cst_stabilize of Misc.component
| Cst_action_begin of Misc.component * Assertions.cprop * Assertions.cprop * Assertions.cprop
* Exp.IdSet.t
| Cst_action_end of Misc.component * Exp.IdSet.t (*free vars of postcondition*)
| Cst_loop of can_cmd * Assertions.cprop option (*infinite loop -- exit with break/return*)
| Cst_goto of can_goto
| Cst_comment of string
Statement descriptor
type can_entailment = Assertions.cprop * can_cmd * can_cmd * Assertions.cprop *
       Exp.IdSet.t * Location.t
Canonical entailments
type res_init =
| Cri_inv of Assertions.cprop * Location.t
| Cri_code of Exp.IdSet.t * can_cmd * Location.t
Resource initialization

Constructors


val mk_cmd : can_st_desc -> Location.t -> can_cmd
val mk_assume : Exp.exp -> Location.t -> can_cmd
val mk_loop : can_cmd ->
       Assertions.cprop option -> Location.t -> Exp.IdSet.t -> can_cmd
val mk_nondet : can_cmd -> can_cmd -> Location.t -> can_cmd
val cmd_copy : can_cmd -> can_cmd
Make a deep copy of a command (preserve lvs and actions)
val cmd_clear_copy : can_cmd -> can_cmd
Make a deep copy of a command (clear lvs and actions)

Inferred actions annotations


val actlr_clear : (string * can_entailment) list -> unit
val actlr_iter : (string * Assertions.cprop -> unit) ->
       (string * can_entailment) list -> unit
val actlr_upd : (Assertions.cprop -> Assertions.cprop) ->
       (string * can_entailment) list -> unit
val actlr_print : (string * can_entailment) list -> unit

Linearizability


val ident_lin_res : Exp.Id.t
val linear_fun_pre : Assertions.cprop
val linear_fun_post : Assertions.cprop
val linear_parse_spec : can_cmd -> can_cmd list * can_cmd list
Check that a linearizability specification contains no loops and return its effectful & pure execution paths
val insert_pure_code : can_cmd -> can_cmd -> can_cmd
insert_pure_code pure_code c copies c and insert pure_code before every atomic_block exit

Other operations


val pp_cmd : Format.formatter -> can_cmd -> unit
val pp_linear_annot : Format.formatter -> can_cmd -> unit
val mark_live_vars : Exp.IdSet.t -> can_cmd -> unit
mark_live_vars fv_post c updates c in place by marking its live variables at each program point.
val insert_kill_dead_vars : can_cmd -> Exp.IdSet.t -> can_cmd
val clarify_cmd : can_cmd -> can_cmd

Unroll the last iteration of all the loops in c
val actlr_merge_linear : (Assertions.cprop -> can_cmd -> 'a) ->
       ('a -> Assertions.cprop -> Assertions.cprop) ->
       can_cmd ->
       string * can_entailment -> (string * can_entailment) list
val left_mover_optimization : (string * can_entailment) list ->
       (string * can_entailment) list
val add_prophecy : can_cmd -> can_cmd
val map_cmd : Exp.subst -> can_cmd -> can_cmd
Assumes that variables affected by the substitution are not on LHS of assignments
val cmd_fcall_concat : can_cmd -> can_cmd -> can_cmd
Imprint | Data protection