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:


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
Imprint | Data protection