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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
open Cil_types
open Cil_datatype
type clause =
| Body of logic_info
| Prop of Property.t
| Call of stmt * kernel_function * Property.t
let compare_clause a b =
match a, b with
| Body f , Body g -> Logic_info.compare f g
| Body _ , _ -> (-1)
| _ , Body _ -> (+1)
| Prop f , Prop g -> Property.compare f g
| Prop _ , _ -> (-1)
| _ , Prop _ -> (+1)
| Call(s1,kf1,p1) , Call(s2,kf2,p2) ->
let c = Stmt.compare s1 s2 in
if c <> 0 then c else
let c = Kernel_function.compare kf1 kf2 in
if c <> 0 then c else
Property.compare p1 p2
type acs =
| Exp of Stmt.t * exp
| Ret of Stmt.t * exp
| Lval of Stmt.t * lval
| Init of Stmt.t * lval * exp
| Term of clause * term_lval
let compare a b =
match a, b with
| Init(sa,la,va), Init(sb,lb,vb) ->
let cmp = Stmt.compare sa sb in
if cmp <> 0 then cmp else
let cmp = Lval.compare la lb in
if cmp <> 0 then cmp else
Exp.compare va vb
| Init _ , _ -> (-1)
| _ , Init _ -> (+1)
| Lval(sa,la), Lval(sb,lb) ->
let cmp = Stmt.compare sa sb in
if cmp <> 0 then cmp else Lval.compare la lb
| Lval _ , _ -> (-1)
| _ , Lval _ -> (+1)
| Exp(sa,ea), Exp(sb,eb) ->
let cmp = Stmt.compare sa sb in
if cmp <> 0 then cmp else Exp.compare ea eb
| Exp _ , _ -> (-1)
| _ , Exp _ -> (+1)
| Ret(sa,ea), Ret(sb,eb) ->
let cmp = Stmt.compare sa sb in
if cmp <> 0 then cmp else Exp.compare ea eb
| Ret _ , _ -> (-1)
| _ , Ret _ -> (+1)
| Term(ca,ta), Term(cb,tb) ->
let cmp = compare_clause ca cb in
if cmp <> 0 then cmp else Term_lval.compare ta tb
module Set = Set.Make(struct type t = acs let compare = compare end)
let pp_label fmt (s : stmt) =
match s.labels with
| Label(l,_,_)::_ -> Format.pp_print_string fmt l
| _ ->
let line = Stmt.loc s |> Fileloc.line in
Format.fprintf fmt "L%d" line
let pp_clause fmt = function
| Body l -> Format.pp_print_string fmt "logic:" ; Logic_info.pretty fmt l
| Prop p -> Format.pp_print_string fmt @@ Property.Names.get_prop_name_id p
| Call(st,kf,prop) ->
Format.fprintf fmt "%a@%a@%s"
Kernel_function.pretty kf pp_label st
(Property.Names.get_prop_name_id prop)
let pretty fmt = function
| Init(s,l,v) ->
Format.fprintf fmt "(%a=%a)@%a" Lval.pretty l Exp.pretty v pp_label s
| Lval(s,l) ->
Format.fprintf fmt "%a@%a" Lval.pretty l pp_label s
| Exp(s,e) ->
Format.fprintf fmt "(%a)@%a" Exp.pretty e pp_label s
| Ret(s,e) ->
Format.fprintf fmt "(return %a)@%a" Exp.pretty e pp_label s
| Term(c,l) ->
Format.fprintf fmt "(%a)@%a" Term_lval.pretty l pp_clause c
let pp_access fmt = function
| Exp(_,e) -> Printer.pp_exp fmt e
| Ret(_,e) -> Format.fprintf fmt "return %a" Printer.pp_exp e
| Lval(_,l) -> Printer.pp_lval fmt l
| Init(_,l,v) ->
Format.fprintf fmt "init %a=%a" Printer.pp_lval l Printer.pp_exp v
| Term(Prop _,t) -> Printer.pp_term_lval fmt t
| Term(Body fn,t) ->
Format.fprintf fmt "%a { %a }" Logic_info.pretty fn Printer.pp_term_lval t
| Term(Call(_,kf,_),t) ->
Format.fprintf fmt "%a { %a }" Kernel_function.pretty kf Printer.pp_term_lval t
let pp_line fmt stmt =
let line = Stmt.loc stmt |> Fileloc.line in
List.iter (Format.fprintf fmt "%a " Printer.pp_label) stmt.labels ;
Format.fprintf fmt "s%d, line %d" stmt.sid line
let pp_source fmt = function
| Init(stmt,_,_) | Ret(stmt,_) | Exp(stmt,_) | Lval(stmt,_) ->
pp_line fmt stmt
| Term(Prop ip,_) -> Description.pp_local fmt ip
| Term(Body fn,_) ->
if fn.l_type = None then
Format.fprintf fmt "predicate %a" Logic_info.pretty fn
else
Format.fprintf fmt "logic %a" Logic_info.pretty fn
| Term(Call(stmt,_,_),_) ->
Format.fprintf fmt "call at %a" pp_line stmt
let ctype_of = function
| Ctype t -> t
| _ -> Cil_const.voidType
let location = function
| Body _ -> Fileloc.unknown
| Prop ip | Call(_,_,ip) -> Property.location ip
let typeof = function
| Init(_,lv,_) | Lval(_,lv) -> Cil.typeOfLval lv
| Exp(_,e) | Ret(_,e) -> Cil.typeOf e
| Term(_,lv) ->
Logic_const.plain_or_set ctype_of @@ Cil.typeOfTermLval lv
open Printer_tag
let marker = function
| Exp(stmt,e) | Ret(stmt,e) -> PExp(None,Kstmt stmt,e)
| Init (stmt,(Var vi,_),_) -> PVDecl(None,Kstmt stmt,vi)
| Init (stmt,(Mem e,_),_) -> PExp(None,Kstmt stmt,e)
| Lval(stmt,_) | Term (Call (stmt, _, _), _) ->
PStmtStart(Kernel_function.find_englobing_kf stmt, stmt)
| Term (Body fn, _) ->
PGlobal(GAnnot(Dfun_or_pred(fn,Fileloc.unknown),Fileloc.unknown))
| Term (Prop ip, _) -> PIP ip
let rank = function
| Term (Body _, _) | Term(Prop _, _) -> 0
| Exp(s,_) | Ret(s,_) | Init(s,_,_) | Lval(s,_) | Term(Call(s,_,_),_)
-> s.sid