-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathassign.ml
166 lines (143 loc) · 6.56 KB
/
assign.ml
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
160
161
162
163
164
165
166
open Function
open Tuple
open Option
open Name
open Formula
open Location
open Listutils
(* This file is part of Arsenic, a proofchecker for New Lace logic.
Copyright (c) 2015 Richard Bornat.
Licensed under the MIT license (sic): see LICENCE.txt or
https://opensource.org/licenses/MIT
*)
type assign =
| RbecomesE of reg * formula (* real := pure or aux := auxpure *)
| LocbecomesEs of (* bool * *) (location * formula) list (* bool for load-reserved; first real/real or aux/auxpure, rest aux/auxpure *)
| RsbecomeLocs of (* bool * *) (reg list * location) list (* bool for store conditional; first real/real or aux/auxpure, rest aux/aux *)
(* type assignop =
| LoadReserve (* :=? *)
| StoreConditional (* ?:= *)
| LocalAssign (* := *)
*)
let string_of_assignop _ = ":=" (* function
| LoadReserve -> ":=?"
| StoreConditional -> "?:="
| LocalAssign -> ":="
*)
let string_of_assign a =
let soa assignop lhs rhs = Printf.sprintf "%s %s %s" lhs (string_of_assignop assignop) rhs in
match a with
| RbecomesE (r,f) -> soa (* LocalAssign *) () (Name.string_of_reg r) (string_of_formula f)
| LocbecomesEs ((* b,*) locfs) ->
(let op = () in (* if b then StoreConditional else LocalAssign in *)
match locfs with
| [loc,f] -> soa op (string_of_location loc) (string_of_formula f)
| _ ->
let locs, fs = List.split locfs in
let string_of_rhs f =
match f.fnode with
| Tuple _ -> "(" ^ string_of_formula f ^ ")"
| _ -> string_of_formula f
in
soa op (string_of_list string_of_location "," locs) (string_of_list string_of_rhs "," fs)
)
| RsbecomeLocs ((* b, *) rslocs) ->
(let op = () in (* if b then LoadReserve else LocalAssign in *)
match rslocs with
| [rs,loc] -> soa op (string_of_list Name.string_of_reg "," rs) (string_of_location loc)
| _ ->
let rss, locs = List.split rslocs in
let string_of_lhs rs =
match rs with
| [r] -> Name.string_of_reg r
| _ -> "(" ^ string_of_list Name.string_of_reg "," rs ^ ")"
in
soa op (string_of_list string_of_lhs "," rss) (string_of_list string_of_location "," locs)
)
let is_aux_assign = function
| RbecomesE (r,_) -> Name.is_auxreg r
| LocbecomesEs ((* _, *) (loc,_)::_) -> Location.is_auxloc loc
| RsbecomeLocs ((* _, *) ((r::_),_)::_) -> Name.is_auxreg r
| a -> raise (Invalid_argument ("Assign.is_aux_assign " ^ string_of_assign a))
let is_var_assign = function
| LocbecomesEs _ -> true
| _ -> false
let is_reg_assign = function
| RbecomesE _
| RsbecomeLocs _ -> true
| LocbecomesEs _ -> false
(* let is_loadreserved = function
| RsbecomeLocs (b,_) -> b
| _ -> false
let is_storeconditional = function
| LocbecomesEs (b,_) -> b
| _ -> false
let reserved = function
| LocbecomesEs (true, ((loc,e)::_)) -> loc
| RsbecomeLocs (true, ((_,loc)::_)) -> loc
| a -> raise (Invalid_argument ("Assign.reserved " ^ string_of_assign a))
let reserved_loaded = function
| RsbecomeLocs (true, ((rs,loc)::_)) -> singleton_or_tuple (List.map _recFname rs)
| a -> raise (Invalid_argument ("Assign.reserved_loaded " ^ string_of_assign a))
let conditionally_stored = function
| LocbecomesEs (true, ((loc,e)::_)) -> e
| a -> raise (Invalid_argument ("Assign.conditionally_stored " ^ string_of_assign a))
*)
let loces = function
| LocbecomesEs ((* b, *) loces) -> loces
| assign -> raise (Invalid_argument ("Assign.loces " ^ string_of_assign assign))
let foa frees assign =
let loc_frees = function
| VarLoc v -> NameSet.singleton v
in
match assign with
| RbecomesE (r,e) -> NameSet.add r (Formula.fof frees e)
| LocbecomesEs ((* b, *) loces) ->
List.fold_left (fun set (location,e) -> NameSet.union set (NameSet.union (loc_frees location) (Formula.frees e)))
frees
loces
| RsbecomeLocs ((* b, *) rsvs) ->
List.fold_left (fun set (rs,location) -> NameSet.union set (NameSet.union (loc_frees location) (NameSet.of_list rs)))
frees
rsvs
let frees = foa NameSet.empty
(* designed to be folded *)
let formulas fs = function
| RbecomesE (r,e) -> e::fs
| LocbecomesEs ((* b,*) loces) ->
List.fold_left (fun fs -> (function (v,e) -> e::fs))
fs
loces
| RsbecomeLocs ((* b, *) rslocs) ->
List.fold_left (fun fs -> (function (_,v) -> fs))
fs
rslocs
let assigned = function
| RbecomesE (r,e) -> NameSet.singleton r
| LocbecomesEs ((* b, *) loces) -> NameSet.of_list (List.map (function (VarLoc v,e) -> v) loces)
| RsbecomeLocs ((* b, *) rsv_s) -> NameSet.of_list (List.concat (fstof2 (List.split rsv_s)))
let optmap af ff a =
let opmloc = function VarLoc v -> None in
match af ff a with
| None -> (match a with
| RbecomesE (r,e) -> Formula.optmap ff e
&~~ (fun e' -> Some (RbecomesE (r,e')))
| LocbecomesEs ((* b, *) loces) -> let locs, es = List.split loces in
optionpair_either (optmap_any opmloc) locs
(optmap_any (Formula.optmap ff)) es
&~~ (fun (locs,es) -> Some (LocbecomesEs ((* b, *) List.combine locs es)))
| RsbecomeLocs ((* b, *) rslocs) -> let rss, locs = List.split rslocs in
optmap_any opmloc locs
&~~ (fun locs -> Some (RsbecomeLocs ((* b, *) List.combine rss locs)))
)
| r -> r
let map af ff = anyway (optmap af ff)
let substitute mapping = function (* does locs as well *) (* no it doesn't *)
| LocbecomesEs ((* b, *) loces) ->
LocbecomesEs ((* b, *) List.map (function (loc,e) -> loc, Formula.substitute mapping e)
loces
)
| a -> a
let optstripspos = optmap (fun ff a -> None) Formula.stripspos_opt
let stripspos = optstripspos ||~ id
let eq a1 a2 = stripspos a1 = stripspos a2