Poling/qualifier.mli at master · rowangithub/Poling · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
(* Poling: Proof Of Linearizability Generator
 * Poling is built on top of CAVE and shares the same license with CAVE
 * See LICENSE.txt for license.
 * Contact: He Zhu, Department of Computer Science, Purdue University
 * Email: zhu103@purdue.edu
 *)

(**
   This module implements our main algorithm based on CAVE
	 Read qualifiers from file
	 Qulifier Elimination
*)

open Assertions
open Genarith
open Exp
open Misc


(**********************************************************)
(***************** Shape Qualifier API ********************)
(**********************************************************)

(** Load user provided shape predicate from given qualifier file *)
val convert : Parsetree.a_proposition -> cform list

val compare : (Misc.component, cform list) Hashtbl.t -> (Misc.component, cform list) Hashtbl.t -> bool

(** Qualifier elimination: use prover to select qualifiers that overapproximates intermediate state *)
val eliminate1 : prover -> (Misc.component, cform list) Hashtbl.t -> eprop ->
									(Misc.component, cform list) Hashtbl.t

val eliminate_inplace : prover -> (Misc.component, cform list) Hashtbl.t -> eprop -> unit

val eliminate : prover -> cform list -> eprop -> eprop

val subtract : prover -> cform list -> cform list -> cform list

val subtract1 : prover -> cform list -> cform list -> bool

(** Qualifiers should be instantiated by context variables before use *)
val instantiate: cform list -> IdSet.t -> cform list

(** Expand user provided cform to cprop *)
val expand_shape_qualifier : cform -> cform list

(**********************************************************)
(***************** Pure Qualifier API *********************)
(**********************************************************)

type pure_qualifier_t = string * string * Predicate.t

val transl_pure_qualifiers : Parsetree.qualifier_declaration list -> pure_qualifier_t list

val print_pure_qual : pure_qualifier_t -> unit

(**********************************************************)
(***************** Specification API **********************)
(**********************************************************)

type spec_t = string * Predicate.t

val transl_specifications : Parsetree.specification_declaration list -> spec_t list

val print_spec : spec_t -> unit

(** Intepretation of specification:
 Idea: map  *)