Module Genarith

module Genarith: sig .. end

Generation of arithmetic programs

This module provides helper routines for generating arithmetic programs out of separation logic proofs following the work of Magill et al. Arithmetic program generation is turned off by default because it places a heavy burden on the garbage collector and, moreover, the generated programs are huge (mainly because the RGSep proof objects are huge).

val enabled : unit -> bool

Is arithmetic program generation enabled?

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

Graphs

type ga_node

Nodes

val new_node : Assertions.cform -> ga_node

Create a new node

val put_edge_skip : ga_node -> ga_node -> unit

Put an edge from n1 to n2

val put_edge_implication : ga_node -> Exp.subst -> Pure.t -> ga_node -> unit

Put an edge from n1 to n2

val pp_function : Format.formatter -> string * ga_node -> unit

Pretty print the generated integer program reachable from a node

Extended assertions

type eform = ga_node

type eprop = eform list

val cform_of_eform : eform -> Assertions.cform

val eprop_of_cprop : Assertions.cprop -> eprop

Generic constructor: create a new node for each disjunct

val eprop_of_cprop_at_start_node : Assertions.cprop -> ga_node * eprop

val eprop_false : eprop

val eprop_star : Assertions.cprop -> eprop -> eprop

val eprop_star_assume : Assertions.cprop -> eprop -> eprop

val eprop_or : eprop -> eprop -> eprop

val ext_append_return : eprop -> unit

val ext_append_comment : (unit -> string) -> eprop -> eprop

val ext_append_assign : (Exp.Id.t * Exp.exp option) list -> eprop -> eprop

val ext_append_case_split : eprop -> eprop * eprop

val ext_opt_transform1 : (Assertions.cform -> Assertions.cform list option) ->
       eform -> eform list option

val plain_ext_transform : (Assertions.cform -> Assertions.cprop) -> eprop -> eprop

val ext_transform : (Assertions.cform -> Assertions.cprop) -> eprop -> eprop

val remove_eform_duplicates : eform list -> eform list

Remove syntactically identical disjuncts (and add edges to the generated arithmetic program where necessary).

val map_eprop : (Exp.exp -> Exp.exp) -> eprop -> eprop

val naive_map_eprop : (Exp.exp -> Exp.exp) -> eprop -> eprop

val pp_eprop : Format.formatter -> eprop -> unit

Abstraction interface

type udom = Assertions.uform list * Assertions.uform list

Abstract domain corresponding to a disjunction of uforms for calculating fix-points.

NB: The two components of udom are to work round the possible non-transitivity of the prover's entailment checking.

val udom_of_uform_list : Assertions.uform list -> udom

val uform_list_of_udom : udom -> Assertions.uform list

type abstraction = {

	`uform_abs : bool -> Assertions.uform list -> Assertions.uform list;`
	`uform_join : udom -> Assertions.uform list -> udom * Assertions.uform list;`
	`prop_abs : eprop -> eprop;`
	`prop_join : eprop -> eprop -> eprop -> eprop * eprop * eprop;`
	`set_abs : Exp.IdSet.t -> Exp.exp list list -> Exp.subst;`
	`list_abs : Exp.exp list list -> Exp.subst;`

}

Interface provided by the abstraction module:

uform_abs is the analogue of prop_abs for formulas with no boxes. See below. The boolean argument tells whether the abstraction should be aggressive (disregard sentinel values).
uform_join is the analogue of prop_join for formulas with no boxes. See below.
prop_abs cp returns a cp' belonging to a smaller domain such that cp |- cp'
prop_join cp1a cp1b cp2 assumes that cp1a <==> cp1b and returns (cpa,cpb,cp2') such that cpa <==> cpb and cp1a |- cpa and cp2' |- cpa and (cp1b \/ cp2) ==> cpb and cpb ==> (cp1b \/ cp2')
set_abs returns a substitution that abstracts set values in the assertion
list_abs returns a substitution that abstract list values in the assertion

Imprint | Data protection