Module Symbsimp

module Symbsimp: sig .. end

Symbolic execution

This module implements symbolic execution for RGSep assertions with and without action inference, and a linearizability verifier.

References:

Vafeiadis, V.: Automatically proving linearizability. In: CAV 2010. Springer, Heidelberg (2010)
Vafeiadis, V.: RGSep action inference. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 345-361. Springer, Heidelberg (2010)
Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., File, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233-248. Springer, Heidelberg (2007)

type global_env = {

`g_prover : Assertions.prover;`
`g_abstraction : Genarith.abstraction;`
`mutable g_globals : Exp.IdSet.t;`
`g_pro_ht : (string, Tycheck.protocol_item) Hashtbl.t;`
`g_esc_ht : (string, Tycheck.escrow_item) Hashtbl.t;`
`g_fun_ht : (string, Commands.fun_info) Hashtbl.t;`
`g_res_ht : (Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t;`
`g_renv : (Misc.component, Assertions.cprop) Hashtbl.t;`
`g_guar : Actions.guar_env;`
`mutable g_actinf : bool;`
`mutable g_params : Exp.IdSet.t;`
`g_no_interf_hack : bool;`	`(*`	Assume no interference occurs	`*)`
`g_por_hack : bool;`
`mutable g_linear_pure_code : Commands.can_cmd;`
`g_linear_pre : Assertions.cprop option;`	`(*`	Fail quickly for linearizability checking	`*)`

}

val all_fields : Misc.StringSet.t Pervasives.ref

val linear_symbexe : Assertions.prover ->
       Commands.can_stmt list ->
       Exp.IdSet.t -> Assertions.uform list -> Assertions.uform list

val check_no_inference : global_env ->
       (Misc.component * Commands.res_init) list ->
       (string * Commands.can_entailment) list -> bool

Check VCs without doing action inference.

val infer_actions_once : global_env ->
       (Misc.component * Commands.res_init) list ->
       (string * Commands.can_entailment) list -> bool

Check VCs without doing action inference.

val infer_actions : global_env ->
       (Misc.component * Commands.res_init) list ->
       (string * Commands.can_entailment) list -> bool

Executes RGSep action inference.

Configuration parameters & statistics

val verbose : int Pervasives.ref

val args : (Arg.key * Arg.spec * Arg.doc) list