Revision ca7ff3f7
Added by Lélio Brun 7 months ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 1 |
|
|
| 2 | 1 |
(********************************************************************) |
| 3 | 2 |
(* *) |
| 4 | 3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
| ... | ... | |
| 23 | 22 |
|
| 24 | 23 |
(**************************************************************************) |
| 25 | 24 |
|
| 26 |
(* TODO ACSL |
|
| 27 |
Return updates machines (eg with local annotations) and acsl preamble *)
|
|
| 25 |
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
|
|
| 26 |
preamble *) |
|
| 28 | 27 |
let preprocess_acsl machines = machines, [] |
| 29 |
|
|
| 28 |
|
|
| 30 | 29 |
let pp_acsl_basic_type_desc t_desc = |
| 31 | 30 |
if Types.is_bool_type t_desc then |
| 32 | 31 |
(* if !Options.cpp then "bool" else "_Bool" *) |
| ... | ... | |
| 36 | 35 |
if t_desc.tid = -1 then "int" else "integer" |
| 37 | 36 |
else if Types.is_real_type t_desc then |
| 38 | 37 |
if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type |
| 39 |
else |
|
| 40 |
assert false (* Not a basic C type. Do not handle arrays or pointers *)
|
|
| 38 |
else assert false
|
|
| 39 |
(* Not a basic C type. Do not handle arrays or pointers *) |
|
| 41 | 40 |
|
| 42 |
let pp_acsl pp fmt = |
|
| 43 |
fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp |
|
| 41 |
let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp |
|
| 44 | 42 |
|
| 45 |
let pp_acsl_cut pp fmt = |
|
| 46 |
fprintf fmt "%a@," (pp_acsl pp) |
|
| 43 |
let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp) |
|
| 47 | 44 |
|
| 48 |
let pp_acsl_line pp fmt = |
|
| 49 |
fprintf fmt "//%@ @[<h>%a@]" pp |
|
| 45 |
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp |
|
| 50 | 46 |
|
| 51 |
let pp_acsl_line' pp fmt = |
|
| 52 |
fprintf fmt "/*%@ @[<h>%a@] */" pp |
|
| 47 |
let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp |
|
| 53 | 48 |
|
| 54 |
let pp_acsl_line_cut pp fmt = |
|
| 55 |
fprintf fmt "%a@," (pp_acsl_line pp) |
|
| 49 |
let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp) |
|
| 56 | 50 |
|
| 57 |
let pp_requires pp_req fmt = |
|
| 58 |
fprintf fmt "requires %a;" pp_req |
|
| 51 |
let pp_requires pp_req fmt = fprintf fmt "requires %a;" pp_req |
|
| 59 | 52 |
|
| 60 |
let pp_ensures pp_ens fmt = |
|
| 61 |
fprintf fmt "ensures %a;" pp_ens |
|
| 53 |
let pp_ensures pp_ens fmt = fprintf fmt "ensures %a;" pp_ens |
|
| 62 | 54 |
|
| 63 |
let pp_assumes pp_asm fmt = |
|
| 64 |
fprintf fmt "assumes %a;" pp_asm |
|
| 55 |
let pp_assumes pp_asm fmt = fprintf fmt "assumes %a;" pp_asm |
|
| 65 | 56 |
|
| 66 | 57 |
let pp_assigns pp = |
| 67 | 58 |
pp_comma_list |
| 68 | 59 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ") |
| 69 |
~pp_epilogue:pp_print_semicolon' |
|
| 70 |
pp |
|
| 60 |
~pp_epilogue:pp_print_semicolon' pp |
|
| 71 | 61 |
|
| 72 |
let pp_ghost pp_gho fmt = |
|
| 73 |
fprintf fmt "ghost %a" pp_gho |
|
| 62 |
let pp_ghost pp_gho fmt = fprintf fmt "ghost %a" pp_gho |
|
| 74 | 63 |
|
| 75 |
let pp_assert pp_ast fmt = |
|
| 76 |
fprintf fmt "assert %a;" pp_ast |
|
| 64 |
let pp_assert pp_ast fmt = fprintf fmt "assert %a;" pp_ast |
|
| 77 | 65 |
|
| 78 | 66 |
let pp_mem_valid pp_var fmt (name, var) = |
| 79 | 67 |
fprintf fmt "%s_valid(%a)" name pp_var var |
| ... | ... | |
| 90 | 78 |
|
| 91 | 79 |
let pp_access' = pp_access pp_print_string pp_print_string |
| 92 | 80 |
|
| 93 |
let pp_var_decl fmt v = |
|
| 94 |
pp_print_string fmt v.var_id |
|
| 81 |
let pp_var_decl fmt v = pp_print_string fmt v.var_id |
|
| 95 | 82 |
|
| 96 | 83 |
let pp_reg self fmt field = |
| 97 | 84 |
pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field) |
| 98 | 85 |
|
| 99 |
let pp_true fmt () = |
|
| 100 |
pp_print_string fmt "\\true" |
|
| 86 |
let pp_true fmt () = pp_print_string fmt "\\true" |
|
| 101 | 87 |
|
| 102 |
let pp_false fmt () = |
|
| 103 |
pp_print_string fmt "\\false" |
|
| 88 |
let pp_false fmt () = pp_print_string fmt "\\false" |
|
| 104 | 89 |
|
| 105 |
let pp_at pp_v fmt (v, l) = |
|
| 106 |
fprintf fmt "\\at(%a, %s)" pp_v v l |
|
| 90 |
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l |
|
| 107 | 91 |
|
| 108 | 92 |
let instances machines m = |
| 109 | 93 |
let open List in |
| 110 | 94 |
let grow paths i td mems = |
| 111 | 95 |
match paths with |
| 112 |
| [] -> [[i, (td, mems)]] |
|
| 113 |
| _ -> map (cons (i, (td, mems))) paths |
|
| 96 |
| [] -> |
|
| 97 |
[ [ i, (td, mems) ] ] |
|
| 98 |
| _ -> |
|
| 99 |
map (cons (i, (td, mems))) paths |
|
| 114 | 100 |
in |
| 115 | 101 |
let rec aux paths m = |
| 116 |
map (fun (i, (td, _)) -> |
|
| 102 |
map |
|
| 103 |
(fun (i, (td, _)) -> |
|
| 117 | 104 |
try |
| 118 | 105 |
let m = find (fun m -> m.mname.node_id = node_name td) machines in |
| 119 | 106 |
aux (grow paths i td m.mmemory) m |
| 120 | 107 |
with Not_found -> grow paths i td []) |
| 121 |
m.minstances |> flatten |
|
| 108 |
m.minstances |
|
| 109 |
|> flatten |
|
| 122 | 110 |
in |
| 123 | 111 |
aux [] m |> map rev |
| 124 | 112 |
|
| 125 | 113 |
let memories insts = |
| 126 |
List.(map (fun path -> |
|
| 127 |
let _, (_, mems) = hd (rev path) in |
|
| 128 |
map (fun mem -> path, mem) mems) insts |> flatten) |
|
| 129 |
|
|
| 130 |
let pp_instance ?(indirect=true) ptr = |
|
| 114 |
List.( |
|
| 115 |
map |
|
| 116 |
(fun path -> |
|
| 117 |
let _, (_, mems) = hd (rev path) in |
|
| 118 |
map (fun mem -> path, mem) mems) |
|
| 119 |
insts |
|
| 120 |
|> flatten) |
|
| 121 |
|
|
| 122 |
let pp_instance ?(indirect = true) ptr = |
|
| 131 | 123 |
pp_print_list |
| 132 | 124 |
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr) |
| 133 | 125 |
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else ".")) |
| 134 | 126 |
(fun fmt (i, _) -> pp_print_string fmt i) |
| 135 | 127 |
|
| 136 |
let pp_memory ?(indirect=true) ptr fmt (path, mem) =
|
|
| 128 |
let pp_memory ?(indirect = true) ptr fmt (path, mem) =
|
|
| 137 | 129 |
pp_access |
| 138 | 130 |
((if indirect then pp_indirect else pp_access) |
| 139 |
(pp_instance ~indirect ptr) pp_print_string) |
|
| 140 |
pp_var_decl |
|
| 141 |
fmt ((path, "_reg"), mem) |
|
| 131 |
(pp_instance ~indirect ptr) |
|
| 132 |
pp_print_string) |
|
| 133 |
pp_var_decl fmt |
|
| 134 |
((path, "_reg"), mem) |
|
| 142 | 135 |
|
| 143 | 136 |
let prefixes l = |
| 144 | 137 |
let rec pref acc = function |
| 145 |
| x :: l -> pref ([x] :: List.map (List.cons x) acc) l |
|
| 146 |
| [] -> acc |
|
| 138 |
| x :: l -> |
|
| 139 |
pref ([ x ] :: List.map (List.cons x) acc) l |
|
| 140 |
| [] -> |
|
| 141 |
acc |
|
| 147 | 142 |
in |
| 148 | 143 |
pref [] (List.rev l) |
| 149 | 144 |
|
| 150 |
let powerset_instances paths = |
|
| 151 |
List.map prefixes paths |> List.flatten |
|
| 145 |
let powerset_instances paths = List.map prefixes paths |> List.flatten |
|
| 152 | 146 |
|
| 153 | 147 |
let pp_separated self mem fmt (paths, ptrs) = |
| 154 |
fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" |
|
| 155 |
self |
|
| 156 |
mem |
|
| 157 |
(pp_comma_list |
|
| 158 |
~pp_prologue:pp_print_comma' |
|
| 159 |
(pp_instance self)) |
|
| 148 |
fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])" self mem |
|
| 149 |
(pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance self)) |
|
| 160 | 150 |
paths |
| 161 |
(pp_comma_list |
|
| 162 |
~pp_prologue:pp_print_comma' |
|
| 163 |
pp_var_decl) |
|
| 151 |
(pp_comma_list ~pp_prologue:pp_print_comma' pp_var_decl) |
|
| 164 | 152 |
ptrs |
| 165 | 153 |
|
| 166 | 154 |
let pp_separated' = |
| 167 | 155 |
pp_comma_list |
| 168 | 156 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
|
| 169 |
~pp_epilogue:pp_print_cpar |
|
| 170 |
pp_var_decl |
|
| 157 |
~pp_epilogue:pp_print_cpar pp_var_decl |
|
| 171 | 158 |
|
| 172 |
let pp_par pp fmt = |
|
| 173 |
fprintf fmt "(%a)" pp |
|
| 159 |
let pp_par pp fmt = fprintf fmt "(%a)" pp |
|
| 174 | 160 |
|
| 175 | 161 |
let pp_forall pp_l pp_r fmt (l, r) = |
| 176 |
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" |
|
| 177 |
pp_l l |
|
| 178 |
pp_r r |
|
| 162 |
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r |
|
| 179 | 163 |
|
| 180 | 164 |
let pp_exists pp_l pp_r fmt (l, r) = |
| 181 |
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" |
|
| 182 |
pp_l l |
|
| 183 |
pp_r r |
|
| 165 |
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r |
|
| 184 | 166 |
|
| 185 |
let pp_equal pp_l pp_r fmt (l, r) = |
|
| 186 |
fprintf fmt "%a == %a" |
|
| 187 |
pp_l l |
|
| 188 |
pp_r r |
|
| 167 |
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r |
|
| 189 | 168 |
|
| 190 |
let pp_different pp_l pp_r fmt (l, r) = |
|
| 191 |
fprintf fmt "%a != %a" |
|
| 192 |
pp_l l |
|
| 193 |
pp_r r |
|
| 169 |
let pp_different pp_l pp_r fmt (l, r) = fprintf fmt "%a != %a" pp_l l pp_r r |
|
| 194 | 170 |
|
| 195 | 171 |
let pp_implies pp_l pp_r fmt (l, r) = |
| 196 |
fprintf fmt "@[<v>%a ==>@ %a@]" |
|
| 197 |
pp_l l |
|
| 198 |
pp_r r |
|
| 172 |
fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r |
|
| 199 | 173 |
|
| 200 |
let pp_and pp_l pp_r fmt (l, r) = |
|
| 201 |
fprintf fmt "@[<v>%a @ && %a@]" |
|
| 202 |
pp_l l |
|
| 203 |
pp_r r |
|
| 174 |
let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r |
|
| 204 | 175 |
|
| 205 | 176 |
let pp_and_l pp_v fmt = |
| 206 |
pp_print_list |
|
| 207 |
~pp_open_box:pp_open_vbox0 |
|
| 177 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
| 208 | 178 |
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ") |
| 209 |
pp_v |
|
| 210 |
fmt |
|
| 179 |
pp_v fmt |
|
| 211 | 180 |
|
| 212 |
let pp_or pp_l pp_r fmt (l, r) = |
|
| 213 |
fprintf fmt "@[<v>%a @ || %a@]" |
|
| 214 |
pp_l l |
|
| 215 |
pp_r r |
|
| 181 |
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r |
|
| 216 | 182 |
|
| 217 | 183 |
let pp_or_l pp_v fmt = |
| 218 |
pp_print_list |
|
| 219 |
~pp_open_box:pp_open_vbox0 |
|
| 184 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
| 220 | 185 |
~pp_sep:(fun fmt () -> fprintf fmt "@,|| ") |
| 221 |
pp_v |
|
| 222 |
fmt |
|
| 186 |
pp_v fmt |
|
| 223 | 187 |
|
| 224 |
let pp_not pp fmt = |
|
| 225 |
fprintf fmt "!%a" pp |
|
| 188 |
let pp_not pp fmt = fprintf fmt "!%a" pp |
|
| 226 | 189 |
|
| 227 | 190 |
let pp_valid pp = |
| 228 | 191 |
pp_and_l |
| 229 |
(* pp_print_list *) |
|
| 192 |
(* pp_print_list *)
|
|
| 230 | 193 |
(* ~pp_sep:pp_print_cut *) |
| 231 | 194 |
(fun fmt x -> fprintf fmt "\\valid(%a)" pp x) |
| 232 | 195 |
|
| 233 |
let pp_old pp fmt = |
|
| 234 |
fprintf fmt "\\old(%a)" pp |
|
| 196 |
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp |
|
| 235 | 197 |
|
| 236 | 198 |
let pp_ite pp_c pp_t pp_f fmt (c, t, f) = |
| 237 |
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" |
|
| 238 |
pp_c c |
|
| 239 |
pp_t t |
|
| 240 |
pp_f f |
|
| 199 |
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f |
|
| 241 | 200 |
|
| 242 |
let pp_paren pp fmt v = |
|
| 243 |
fprintf fmt "(%a)" pp v |
|
| 201 |
let pp_paren pp fmt v = fprintf fmt "(%a)" pp v |
|
| 244 | 202 |
|
| 245 | 203 |
let pp_initialization pp_mem fmt (name, mem) = |
| 246 | 204 |
fprintf fmt "%s_initialization(%a)" name pp_mem mem |
| ... | ... | |
| 251 | 209 |
pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m |
| 252 | 210 |
|
| 253 | 211 |
let pp_locals m = |
| 254 |
pp_comma_list |
|
| 255 |
~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) |
|
| 256 |
(pp_local m) |
|
| 212 |
pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m) |
|
| 257 | 213 |
|
| 258 |
let pp_ptr_decl fmt v = |
|
| 259 |
pp_ptr fmt v.var_id |
|
| 214 |
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id |
|
| 260 | 215 |
|
| 261 | 216 |
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value = |
| 262 |
if Types.is_real_type typ && !Options.mpfr |
|
| 263 |
then |
|
| 264 |
assert false |
|
| 217 |
if Types.is_real_type typ && !Options.mpfr then assert false |
|
| 265 | 218 |
(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *) |
| 266 |
else |
|
| 267 |
pp_equal pp_l pp_r fmt (var_name, value) |
|
| 219 |
else pp_equal pp_l pp_r fmt (var_name, value) |
|
| 268 | 220 |
|
| 269 | 221 |
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt |
| 270 | 222 |
(var_type, var_name, value) = |
| ... | ... | |
| 275 | 227 |
match vars with |
| 276 | 228 |
| [] -> |
| 277 | 229 |
pp_basic_assign_spec |
| 278 |
(pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars pp_var_l) |
|
| 279 |
(pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars pp_var_r) |
|
| 230 |
(pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars |
|
| 231 |
pp_var_l) |
|
| 232 |
(pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars |
|
| 233 |
pp_var_r) |
|
| 280 | 234 |
fmt typ var_name value |
| 281 | 235 |
| (_d, LVar _i) :: _q -> |
| 282 | 236 |
assert false |
| 283 |
(* let typ' = Types.array_element_type typ in
|
|
| 284 |
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
|
| 285 |
* i i i pp_c_dimension d i
|
|
| 286 |
* (aux typ') q *)
|
|
| 237 |
(* let typ' = Types.array_element_type typ in |
|
| 238 |
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
|
| 239 |
* i i i pp_c_dimension d i |
|
| 240 |
* (aux typ') q *) |
|
| 287 | 241 |
| (_d, LInt _r) :: _q -> |
| 288 | 242 |
assert false |
| 289 |
(* let typ' = Types.array_element_type typ in |
|
| 290 |
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in |
|
| 291 |
* fprintf fmt "@[<v 2>{@,%a@]@,}"
|
|
| 292 |
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *) |
|
| 293 |
| _ -> assert false |
|
| 243 |
(* let typ' = Types.array_element_type typ in |
|
| 244 |
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in |
|
| 245 |
* fprintf fmt "@[<v 2>{@,%a@]@,}"
|
|
| 246 |
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *) |
|
| 247 |
| _ -> |
|
| 248 |
assert false |
|
| 294 | 249 |
in |
| 295 |
begin |
|
| 296 |
reset_loop_counter (); |
|
| 297 |
aux var_type fmt reordered_loop_vars; |
|
| 298 |
end |
|
| 250 |
reset_loop_counter (); |
|
| 251 |
aux var_type fmt reordered_loop_vars |
|
| 299 | 252 |
|
| 300 |
let pp_nothing fmt () = |
|
| 301 |
pp_print_string fmt "\\nothing" |
|
| 253 |
let pp_nothing fmt () = pp_print_string fmt "\\nothing" |
|
| 302 | 254 |
|
| 303 | 255 |
let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) = |
| 304 |
fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" |
|
| 305 |
name |
|
| 306 |
(pp_print_option pp_print_int) i |
|
| 307 |
pp_mem mem |
|
| 308 |
pp_self self |
|
| 256 |
fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])" name |
|
| 257 |
(pp_print_option pp_print_int) |
|
| 258 |
i pp_mem mem pp_self self |
|
| 309 | 259 |
|
| 310 | 260 |
let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) = |
| 311 | 261 |
pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt |
| ... | ... | |
| 313 | 263 |
|
| 314 | 264 |
let pp_memory_pack_aux' ?i fmt = |
| 315 | 265 |
pp_memory_pack_aux ?i pp_print_string pp_print_string fmt |
| 316 |
let pp_memory_pack' fmt = |
|
| 317 |
pp_memory_pack pp_print_string pp_print_string fmt
|
|
| 266 |
|
|
| 267 |
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
|
|
| 318 | 268 |
|
| 319 | 269 |
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt |
| 320 | 270 |
(name, inputs, locals, outputs, mem_in, mem_out) = |
| 321 | 271 |
let stateless = fst (get_stateless_status m) in |
| 322 |
fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" |
|
| 323 |
name
|
|
| 324 |
(pp_print_option pp_print_int) i
|
|
| 272 |
fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
|
|
| 273 |
(pp_print_option pp_print_int)
|
|
| 274 |
i |
|
| 325 | 275 |
(fun fmt -> if not stateless then pp_mem_in fmt mem_in) |
| 326 | 276 |
(pp_comma_list |
| 327 | 277 |
~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ()) |
| 328 |
pp_input) inputs |
|
| 278 |
pp_input) |
|
| 279 |
inputs |
|
| 329 | 280 |
(pp_print_option (fun fmt _ -> |
| 330 | 281 |
pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals)) |
| 331 | 282 |
i |
| 332 | 283 |
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out) |
| 333 |
(pp_comma_list ~pp_prologue:pp_print_comma pp_output) outputs |
|
| 284 |
(pp_comma_list ~pp_prologue:pp_print_comma pp_output) |
|
| 285 |
outputs |
|
| 334 | 286 |
|
| 335 | 287 |
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt |
| 336 | 288 |
(t, mem_in, mem_out) = |
| ... | ... | |
| 339 | 291 |
|
| 340 | 292 |
let pp_transition_aux' ?i m = |
| 341 | 293 |
pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl |
| 294 |
|
|
| 342 | 295 |
let pp_transition_aux'' ?i m = |
| 343 | 296 |
pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl |
| 297 |
|
|
| 344 | 298 |
let pp_transition' m = |
| 345 | 299 |
pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl |
| 300 |
|
|
| 346 | 301 |
let pp_transition'' m = |
| 347 | 302 |
pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl |
| 348 | 303 |
|
| 349 | 304 |
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) = |
| 350 |
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" |
|
| 351 |
name |
|
| 352 |
pp_mem_in mem_in |
|
| 305 |
fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in |
|
| 353 | 306 |
pp_mem_out mem_out |
| 354 | 307 |
|
| 355 | 308 |
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string |
| ... | ... | |
| 357 | 310 |
let pp_functional_update mems fmt mem = |
| 358 | 311 |
let rec aux fmt mems = |
| 359 | 312 |
match mems with |
| 360 |
| [] -> pp_print_string fmt mem |
|
| 313 |
| [] -> |
|
| 314 |
pp_print_string fmt mem |
|
| 361 | 315 |
| x :: mems -> |
| 362 | 316 |
fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
|
| 363 | 317 |
in |
| 364 | 318 |
aux fmt |
| 365 |
(* if Utils.ISet.is_empty mems then |
|
| 366 |
* pp_print_string fmt mem |
|
| 367 |
* else |
|
| 368 |
* fprintf fmt "{ %s @[<hov>\\with %a@] }"
|
|
| 369 |
* mem |
|
| 370 |
* (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ") |
|
| 371 |
* (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *) |
|
| 372 |
(Utils.ISet.elements mems)
|
|
| 319 |
(* if Utils.ISet.is_empty mems then
|
|
| 320 |
* pp_print_string fmt mem
|
|
| 321 |
* else
|
|
| 322 |
* fprintf fmt "{ %s @[<hov>\\with %a@] }"
|
|
| 323 |
* mem
|
|
| 324 |
* (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
|
|
| 325 |
* (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
|
|
| 326 |
(Utils.ISet.elements mems) |
|
| 373 | 327 |
|
| 374 | 328 |
module PrintSpec = struct |
| 375 |
|
|
| 376 | 329 |
type mode = |
| 377 | 330 |
| MemoryPackMode |
| 378 | 331 |
| TransitionMode |
| ... | ... | |
| 387 | 340 |
| StateVar x -> |
| 388 | 341 |
fprintf fmt "%s.%a" mem pp_var_decl x |
| 389 | 342 |
|
| 390 |
let pp_expr: |
|
| 391 |
type a. ?output:bool -> machine_t -> ident -> formatter |
|
| 392 |
-> (value_t, a) expression_t -> unit = |
|
| 393 |
fun ?(output=false) m mem fmt -> function |
|
| 394 |
| Val v -> pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v |
|
| 395 |
| Tag t -> pp_print_string fmt t |
|
| 396 |
| Var v -> pp_var_decl fmt v |
|
| 397 |
| Memory r -> pp_reg mem fmt r |
|
| 343 |
let pp_expr : |
|
| 344 |
type a. |
|
| 345 |
?output:bool -> |
|
| 346 |
machine_t -> |
|
| 347 |
ident -> |
|
| 348 |
formatter -> |
|
| 349 |
(value_t, a) expression_t -> |
|
| 350 |
unit = |
|
| 351 |
fun ?(output = false) m mem fmt -> function |
|
| 352 |
| Val v -> |
|
| 353 |
pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v |
|
| 354 |
| Tag t -> |
|
| 355 |
pp_print_string fmt t |
|
| 356 |
| Var v -> |
|
| 357 |
pp_var_decl fmt v |
|
| 358 |
| Memory r -> |
|
| 359 |
pp_reg mem fmt r |
|
| 398 | 360 |
|
| 399 | 361 |
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p = |
| 400 |
let output, mem_update = match mode with |
|
| 401 |
| InstrMode _ -> true, false |
|
| 402 |
| TransitionFootprintMode -> false, true |
|
| 403 |
| _ -> false, false |
|
| 362 |
let output, mem_update = |
|
| 363 |
match mode with |
|
| 364 |
| InstrMode _ -> |
|
| 365 |
true, false |
|
| 366 |
| TransitionFootprintMode -> |
|
| 367 |
false, true |
|
| 368 |
| _ -> |
|
| 369 |
false, false |
|
| 404 | 370 |
in |
| 405 |
let pp_expr: |
|
| 406 |
type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit = |
|
| 407 |
fun ?output fmt e -> pp_expr ?output m mem_out fmt e
|
|
| 371 |
let pp_expr :
|
|
| 372 |
type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
|
|
| 373 |
fun ?output fmt e -> pp_expr ?output m mem_out fmt e |
|
| 408 | 374 |
in |
| 409 | 375 |
match p with |
| 410 | 376 |
| Transition (f, inst, i, inputs, locals, outputs, r, mems) -> |
| 411 |
let pp_mem_in, pp_mem_out = match inst with |
|
| 377 |
let pp_mem_in, pp_mem_out = |
|
| 378 |
match inst with |
|
| 412 | 379 |
| None -> |
| 413 |
pp_print_string, |
|
| 414 |
if mem_update then pp_functional_update mems else pp_print_string
|
|
| 380 |
( pp_print_string,
|
|
| 381 |
if mem_update then pp_functional_update mems else pp_print_string )
|
|
| 415 | 382 |
| Some inst -> |
| 416 |
(fun fmt mem_in -> |
|
| 417 |
if r then pp_print_string fmt mem_in |
|
| 418 |
else pp_access' fmt (mem_in, inst)), |
|
| 419 |
(fun fmt mem_out -> pp_access' fmt (mem_out, inst))
|
|
| 383 |
( (fun fmt mem_in ->
|
|
| 384 |
if r then pp_print_string fmt mem_in
|
|
| 385 |
else pp_access' fmt (mem_in, inst)),
|
|
| 386 |
fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
|
|
| 420 | 387 |
in |
| 421 |
pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) |
|
| 422 |
fmt |
|
| 388 |
pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt |
|
| 423 | 389 |
(f, inputs, locals, outputs, mem_in', mem_out') |
| 424 | 390 |
| Reset (_f, inst, r) -> |
| 425 | 391 |
pp_ite |
| ... | ... | |
| 429 | 395 |
fmt |
| 430 | 396 |
(r, (mem_out, 1), (mem_out, (mem_in, inst))) |
| 431 | 397 |
| MemoryPack (f, inst, i) -> |
| 432 |
let pp_mem, pp_self = match inst with |
|
| 398 |
let pp_mem, pp_self = |
|
| 399 |
match inst with |
|
| 433 | 400 |
| None -> |
| 434 | 401 |
pp_print_string, pp_print_string |
| 435 | 402 |
| Some inst -> |
| 436 |
(fun fmt mem -> pp_access' fmt (mem, inst)), |
|
| 437 |
(fun fmt self -> pp_indirect' fmt (self, inst))
|
|
| 403 |
( (fun fmt mem -> pp_access' fmt (mem, inst)),
|
|
| 404 |
fun fmt self -> pp_indirect' fmt (self, inst) )
|
|
| 438 | 405 |
in |
| 439 | 406 |
pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in) |
| 440 | 407 |
| ResetCleared f -> |
| 441 | 408 |
pp_reset_cleared' fmt (f, mem_in, mem_out) |
| 442 |
(* fprintf fmt "ResetCleared_%a" pp_print_string f *) |
|
| 443 |
| Initialization -> () |
|
| 409 |
(* fprintf fmt "ResetCleared_%a" pp_print_string f *) |
|
| 410 |
| Initialization -> |
|
| 411 |
() |
|
| 444 | 412 |
|
| 445 | 413 |
let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool |
| 446 | 414 |
|
| 447 |
let val_of_expr: type a. (value_t, a) expression_t -> value_t = function |
|
| 448 |
| Val v -> v |
|
| 449 |
| Tag t -> id_to_tag t |
|
| 450 |
| Var v -> vdecl_to_val v |
|
| 451 |
| Memory (StateVar v) -> vdecl_to_val v |
|
| 452 |
| Memory ResetFlag -> vdecl_to_val reset_flag |
|
| 415 |
let val_of_expr : type a. (value_t, a) expression_t -> value_t = function |
|
| 416 |
| Val v -> |
|
| 417 |
v |
|
| 418 |
| Tag t -> |
|
| 419 |
id_to_tag t |
|
| 420 |
| Var v -> |
|
| 421 |
vdecl_to_val v |
|
| 422 |
| Memory (StateVar v) -> |
|
| 423 |
vdecl_to_val v |
|
| 424 |
| Memory ResetFlag -> |
|
| 425 |
vdecl_to_val reset_flag |
|
| 453 | 426 |
|
| 454 | 427 |
let find_arrow m = |
| 455 |
try |
|
| 456 |
List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
|
|
| 457 |
|> fst
|
|
| 458 |
with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
|
|
| 428 |
try List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |> fst
|
|
| 429 |
with Not_found ->
|
|
| 430 |
eprintf "Internal error: arrow not found";
|
|
| 431 |
raise Not_found
|
|
| 459 | 432 |
|
| 460 | 433 |
let pp_spec mode m fmt f = |
| 461 | 434 |
let rec pp_spec mode fmt f = |
| ... | ... | |
| 479 | 452 |
| InstrMode self -> |
| 480 | 453 |
let mem = "*" ^ mem in |
| 481 | 454 |
fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label); |
| 482 |
self, flush_str_formatter (), false, |
|
| 483 |
mem, mem, false |
|
| 455 |
self, flush_str_formatter (), false, mem, mem, false |
|
| 484 | 456 |
in |
| 485 |
let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit = |
|
| 486 |
fun fmt e -> pp_expr m mem_out fmt e
|
|
| 457 |
let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
|
|
| 458 |
fun fmt e -> pp_expr m mem_out fmt e |
|
| 487 | 459 |
in |
| 488 | 460 |
let pp_spec' = pp_spec mode in |
| 489 | 461 |
match f with |
| ... | ... | |
| 492 | 464 |
| False -> |
| 493 | 465 |
pp_false fmt () |
| 494 | 466 |
| Equal (a, b) -> |
| 495 |
pp_assign_spec m |
|
| 496 |
mem_out (pp_c_var_read ~test_output:false m) indirect_l |
|
| 497 |
mem_in (pp_c_var_read ~test_output:false m) indirect_r |
|
| 498 |
fmt |
|
| 467 |
pp_assign_spec m mem_out |
|
| 468 |
(pp_c_var_read ~test_output:false m) |
|
| 469 |
indirect_l mem_in |
|
| 470 |
(pp_c_var_read ~test_output:false m) |
|
| 471 |
indirect_r fmt |
|
| 499 | 472 |
(type_of_l_value a, val_of_expr a, val_of_expr b) |
| 500 | 473 |
| And fs -> |
| 501 | 474 |
pp_and_l pp_spec' fmt fs |
| ... | ... | |
| 513 | 486 |
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p |
| 514 | 487 |
| StateVarPack ResetFlag -> |
| 515 | 488 |
let r = vdecl_to_val reset_flag in |
| 516 |
pp_assign_spec m |
|
| 517 |
mem_out (pp_c_var_read ~test_output:false m) indirect_l |
|
| 518 |
mem_in (pp_c_var_read ~test_output:false m) indirect_r |
|
| 519 |
fmt |
|
| 489 |
pp_assign_spec m mem_out |
|
| 490 |
(pp_c_var_read ~test_output:false m) |
|
| 491 |
indirect_l mem_in |
|
| 492 |
(pp_c_var_read ~test_output:false m) |
|
| 493 |
indirect_r fmt |
|
| 520 | 494 |
(Type_predef.type_bool, r, r) |
| 521 | 495 |
| StateVarPack (StateVar v) -> |
| 522 | 496 |
let v' = vdecl_to_val v in |
| 523 | 497 |
let inst = find_arrow m in |
| 524 |
pp_par (pp_implies |
|
| 525 |
(pp_not (pp_initialization pp_access')) |
|
| 526 |
(pp_assign_spec m |
|
| 527 |
mem_out (pp_c_var_read ~test_output:false m) indirect_l |
|
| 528 |
mem_in (pp_c_var_read ~test_output:false m) indirect_r)) |
|
| 498 |
pp_par |
|
| 499 |
(pp_implies |
|
| 500 |
(pp_not (pp_initialization pp_access')) |
|
| 501 |
(pp_assign_spec m mem_out |
|
| 502 |
(pp_c_var_read ~test_output:false m) |
|
| 503 |
indirect_l mem_in |
|
| 504 |
(pp_c_var_read ~test_output:false m) |
|
| 505 |
indirect_r)) |
|
| 529 | 506 |
fmt |
| 530 |
((Arrow.arrow_id, (mem_out, inst)), |
|
| 531 |
(v.var_type, v', v')) |
|
| 507 |
((Arrow.arrow_id, (mem_out, inst)), (v.var_type, v', v')) |
|
| 532 | 508 |
| ExistsMem (f, rc, tr) -> |
| 533 | 509 |
pp_exists |
| 534 | 510 |
(pp_machine_decl' ~ghost:true) |
| 535 | 511 |
(pp_and (pp_spec ResetOut) (pp_spec ResetIn)) |
| 536 | 512 |
fmt |
| 537 |
((f, mk_mem_reset m), |
|
| 538 |
(rc, tr)) |
|
| 513 |
((f, mk_mem_reset m), (rc, tr)) |
|
| 539 | 514 |
in |
| 540 | 515 |
match mode with |
| 541 | 516 |
| TransitionFootprintMode -> |
| ... | ... | |
| 543 | 518 |
let mem_out = mk_mem_out m in |
| 544 | 519 |
pp_forall |
| 545 | 520 |
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string)) |
| 546 |
(pp_spec mode) |
|
| 547 |
fmt ((m.mname.node_id, [mem_in; mem_out]), f)
|
|
| 521 |
(pp_spec mode) fmt
|
|
| 522 |
((m.mname.node_id, [ mem_in; mem_out ]), f)
|
|
| 548 | 523 |
| _ -> |
| 549 | 524 |
pp_spec mode fmt f |
| 550 |
|
|
| 551 | 525 |
end |
| 552 | 526 |
|
| 553 | 527 |
let pp_predicate pp_l pp_r fmt (l, r) = |
| 554 |
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" |
|
| 555 |
pp_l l |
|
| 556 |
pp_r r |
|
| 528 |
fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r |
|
| 557 | 529 |
|
| 558 | 530 |
let pp_lemma pp_l pp_r fmt (l, r) = |
| 559 |
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" |
|
| 560 |
pp_l l |
|
| 561 |
pp_r r |
|
| 531 |
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r |
|
| 562 | 532 |
|
| 563 | 533 |
let pp_mem_valid_def fmt m = |
| 564 | 534 |
if not (fst (get_stateless_status m)) then |
| ... | ... | |
| 570 | 540 |
(pp_and |
| 571 | 541 |
(pp_and_l (fun fmt (inst, (td, _)) -> |
| 572 | 542 |
if Arrow.td_is_arrow td then |
| 573 |
pp_valid pp_indirect' fmt [self, inst] |
|
| 574 |
else |
|
| 575 |
pp_mem_valid pp_indirect' fmt (node_name td, (self, inst)))) |
|
| 543 |
pp_valid pp_indirect' fmt [ self, inst ] |
|
| 544 |
else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst)))) |
|
| 576 | 545 |
(pp_valid pp_print_string))) |
| 577 | 546 |
fmt |
| 578 |
((name, (name, self)), |
|
| 579 |
(m.minstances, [self])) |
|
| 547 |
((name, (name, self)), (m.minstances, [ self ])) |
|
| 580 | 548 |
|
| 581 | 549 |
let pp_memory_pack_def m fmt mp = |
| 582 | 550 |
let name = mp.mpname.node_id in |
| ... | ... | |
| 587 | 555 |
(pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr)) |
| 588 | 556 |
(PrintSpec.pp_spec MemoryPackMode m)) |
| 589 | 557 |
fmt |
| 590 |
((mp, (name, mem), (name, self)), |
|
| 591 |
mp.mpformula) |
|
| 558 |
((mp, (name, mem), (name, self)), mp.mpformula) |
|
| 592 | 559 |
|
| 593 | 560 |
let print_machine_ghost_struct fmt m = |
| 594 | 561 |
pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m |
| 595 | 562 |
|
| 596 | 563 |
let pp_memory_pack_defs fmt m = |
| 597 | 564 |
if not (fst (get_stateless_status m)) then |
| 598 |
fprintf fmt "%a@,%a" |
|
| 599 |
print_machine_ghost_struct m |
|
| 600 |
(pp_print_list |
|
| 601 |
~pp_epilogue:pp_print_cut |
|
| 602 |
~pp_open_box:pp_open_vbox0 |
|
| 603 |
(pp_memory_pack_def m)) m.mspec.mmemory_packs |
|
| 565 |
fprintf fmt "%a@,%a" print_machine_ghost_struct m |
|
| 566 |
(pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0 |
|
| 567 |
(pp_memory_pack_def m)) |
|
| 568 |
m.mspec.mmemory_packs |
|
| 604 | 569 |
|
| 605 | 570 |
let pp_transition_def m fmt t = |
| 606 | 571 |
let name = t.tname.node_id in |
| ... | ... | |
| 609 | 574 |
pp_acsl |
| 610 | 575 |
(pp_predicate |
| 611 | 576 |
(pp_transition m |
| 612 |
(pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
|
|
| 613 |
(pp_local m)
|
|
| 614 |
(pp_local m)) |
|
| 577 |
(pp_machine_decl' ~ghost:true) |
|
| 578 |
(pp_machine_decl' ~ghost:true)
|
|
| 579 |
(pp_local m) (pp_local m))
|
|
| 615 | 580 |
(PrintSpec.pp_spec TransitionMode m)) |
| 616 | 581 |
fmt |
| 617 |
((t, (name, mem_in), (name, mem_out)), |
|
| 618 |
t.tformula) |
|
| 582 |
((t, (name, mem_in), (name, mem_out)), t.tformula) |
|
| 619 | 583 |
|
| 620 | 584 |
let pp_transition_defs fmt m = |
| 621 |
pp_print_list |
|
| 622 |
~pp_epilogue:pp_print_cut |
|
| 623 |
~pp_open_box:pp_open_vbox0 |
|
| 585 |
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0 |
|
| 624 | 586 |
(pp_transition_def m) fmt m.mspec.mtransitions |
| 625 | 587 |
|
| 626 | 588 |
let pp_transition_footprint fmt t = |
| 627 |
fprintf fmt "%s_transition%a_footprint" |
|
| 628 |
t.tname.node_id
|
|
| 629 |
(pp_print_option pp_print_int) t.tindex
|
|
| 589 |
fprintf fmt "%s_transition%a_footprint" t.tname.node_id
|
|
| 590 |
(pp_print_option pp_print_int)
|
|
| 591 |
t.tindex |
|
| 630 | 592 |
|
| 631 | 593 |
let pp_transition_footprint_lemma m fmt t = |
| 632 | 594 |
let open Utils.ISet in |
| 633 | 595 |
let name = t.tname.node_id in |
| 634 |
let mems = diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint in |
|
| 635 |
let memories = List.map (fun v -> |
|
| 636 |
{ v with var_type = { v.var_type with tid = -1 }})
|
|
| 596 |
let mems = |
|
| 597 |
diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint |
|
| 598 |
in |
|
| 599 |
let memories = |
|
| 600 |
List.map |
|
| 601 |
(fun v -> { v with var_type = { v.var_type with tid = -1 } })
|
|
| 637 | 602 |
(List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory) |
| 638 | 603 |
in |
| 639 | 604 |
if not (is_empty mems) then |
| 640 | 605 |
pp_acsl |
| 641 |
(pp_lemma |
|
| 642 |
pp_transition_footprint |
|
| 606 |
(pp_lemma pp_transition_footprint |
|
| 643 | 607 |
(PrintSpec.pp_spec TransitionFootprintMode m)) |
| 644 | 608 |
fmt |
| 645 |
(t, |
|
| 646 |
Forall (
|
|
| 647 |
memories @ t.tinputs @ t.tlocals @ t.toutputs, |
|
| 648 |
Imply (Spec_common.mk_transition ?i:t.tindex name
|
|
| 649 |
(vdecls_to_vals t.tinputs)
|
|
| 650 |
(vdecls_to_vals t.tlocals) |
|
| 609 |
( t,
|
|
| 610 |
Forall
|
|
| 611 |
( memories @ t.tinputs @ t.tlocals @ t.toutputs,
|
|
| 612 |
Imply
|
|
| 613 |
( Spec_common.mk_transition ?i:t.tindex name
|
|
| 614 |
(vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
|
|
| 651 | 615 |
(vdecls_to_vals t.toutputs), |
| 652 | 616 |
Spec_common.mk_transition ~mems ?i:t.tindex name |
| 653 |
(vdecls_to_vals t.tinputs) |
|
| 654 |
(vdecls_to_vals t.tlocals) |
|
| 655 |
(vdecls_to_vals t.toutputs)))) |
|
| 617 |
(vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals) |
|
| 618 |
(vdecls_to_vals t.toutputs) ) ) ) |
|
| 656 | 619 |
|
| 657 | 620 |
let pp_transition_footprint_lemmas fmt m = |
| 658 |
pp_print_list |
|
| 659 |
~pp_epilogue:pp_print_cut
|
|
| 660 |
~pp_open_box:pp_open_vbox0
|
|
| 661 |
(pp_transition_footprint_lemma m) fmt
|
|
| 662 |
(List.filter (fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
|
| 663 |
m.mspec.mtransitions)
|
|
| 621 |
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
|
|
| 622 |
(pp_transition_footprint_lemma m)
|
|
| 623 |
fmt
|
|
| 624 |
(List.filter
|
|
| 625 |
(fun t -> match t.tindex with Some i when i > 0 -> true | _ -> false)
|
|
| 626 |
m.mspec.mtransitions) |
|
| 664 | 627 |
|
| 665 | 628 |
let pp_initialization_def fmt m = |
| 666 | 629 |
if not (fst (get_stateless_status m)) then |
| ... | ... | |
| 673 | 636 |
if Arrow.td_is_arrow td then |
| 674 | 637 |
pp_initialization pp_access' fmt (node_name td, (mem_in, i)) |
| 675 | 638 |
else |
| 676 |
pp_equal (pp_reset_flag ~indirect:false pp_access') pp_print_int |
|
| 677 |
fmt |
|
| 639 |
pp_equal |
|
| 640 |
(pp_reset_flag ~indirect:false pp_access') |
|
| 641 |
pp_print_int fmt |
|
| 678 | 642 |
((mem_in, i), 1)))) |
| 679 | 643 |
fmt |
| 680 | 644 |
((name, (name, mem_in)), m.minstances) |
| ... | ... | |
| 687 | 651 |
pp_acsl |
| 688 | 652 |
(pp_predicate |
| 689 | 653 |
(pp_reset_cleared |
| 690 |
(pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)) |
|
| 654 |
(pp_machine_decl' ~ghost:true) |
|
| 655 |
(pp_machine_decl' ~ghost:true)) |
|
| 691 | 656 |
(pp_ite |
| 692 | 657 |
(pp_reset_flag' ~indirect:false) |
| 693 | 658 |
(pp_and |
| ... | ... | |
| 695 | 660 |
pp_initialization') |
| 696 | 661 |
(pp_equal pp_print_string pp_print_string))) |
| 697 | 662 |
fmt |
| 698 |
((name, (name, mem_in), (name, mem_out)), |
|
| 699 |
(mem_in, |
|
| 700 |
((mem_out, 0), (name, mem_out)), |
|
| 701 |
(mem_out, mem_in))) |
|
| 663 |
( (name, (name, mem_in), (name, mem_out)), |
|
| 664 |
(mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) ) |
|
| 702 | 665 |
|
| 703 |
let pp_at pp_p fmt (p, l) = |
|
| 704 |
fprintf fmt "\\at(%a, %s)" pp_p p l |
|
| 666 |
let pp_at pp_p fmt (p, l) = fprintf fmt "\\at(%a, %s)" pp_p p l |
|
| 705 | 667 |
|
| 706 | 668 |
let label_pre = "Pre" |
| 707 | 669 |
|
| 708 |
let pp_at_pre pp_p fmt p = |
|
| 709 |
pp_at pp_p fmt (p, label_pre) |
|
| 670 |
let pp_at_pre pp_p fmt p = pp_at pp_p fmt (p, label_pre) |
|
| 710 | 671 |
|
| 711 |
let pp_register_chain ?(indirect=true) ptr =
|
|
| 672 |
let pp_register_chain ?(indirect = true) ptr =
|
|
| 712 | 673 |
pp_print_list |
| 713 | 674 |
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr) |
| 714 |
~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
|
|
| 715 |
(if indirect then "->" else "."))
|
|
| 675 |
~pp_epilogue:(fun fmt () -> |
|
| 676 |
fprintf fmt "%s_reg._first" (if indirect then "->" else "."))
|
|
| 716 | 677 |
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else ".")) |
| 717 | 678 |
(fun fmt (i, _) -> pp_print_string fmt i) |
| 718 | 679 |
|
| 719 |
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
|
|
| 680 |
let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
|
|
| 720 | 681 |
pp_print_list |
| 721 | 682 |
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr) |
| 722 | 683 |
~pp_epilogue:(fun fmt () -> pp_reset_flag' ~indirect fmt "") |
| ... | ... | |
| 727 | 688 |
let pp_arrow_reset_ghost mem fmt inst = |
| 728 | 689 |
fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst) |
| 729 | 690 |
|
| 730 |
module GhostProto: MODIFIERS_GHOST_PROTO = struct |
|
| 731 |
let pp_ghost_parameters ?(cut=true) fmt vs =
|
|
| 691 |
module GhostProto : MODIFIERS_GHOST_PROTO = struct
|
|
| 692 |
let pp_ghost_parameters ?(cut = true) fmt vs =
|
|
| 732 | 693 |
fprintf fmt "%a%a" |
| 733 |
(if cut then pp_print_cut else pp_print_nothing) () |
|
| 694 |
(if cut then pp_print_cut else pp_print_nothing) |
|
| 695 |
() |
|
| 734 | 696 |
(pp_acsl_line' |
| 735 |
(pp_ghost |
|
| 736 |
(pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x)))) |
|
| 697 |
(pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x)))) |
|
| 737 | 698 |
vs |
| 738 | 699 |
end |
| 739 | 700 |
|
| 740 | 701 |
module HdrMod = struct |
| 741 |
|
|
| 742 | 702 |
module GhostProto = GhostProto |
| 743 | 703 |
|
| 744 |
let print_machine_decl_prefix = fun _ _ -> ()
|
|
| 704 |
let print_machine_decl_prefix _ _ = ()
|
|
| 745 | 705 |
|
| 746 | 706 |
let pp_import_arrow fmt () = |
| 747 | 707 |
fprintf fmt "#include \"%s/arrow_spec.h%s\"" |
| 748 | 708 |
(Arrow.arrow_top_decl ()).top_decl_owner |
| 749 | 709 |
(if !Options.cpp then "pp" else "") |
| 750 |
|
|
| 751 | 710 |
end |
| 752 | 711 |
|
| 753 | 712 |
module SrcMod = struct |
| 754 |
|
|
| 755 | 713 |
module GhostProto = GhostProto |
| 756 | 714 |
|
| 757 | 715 |
let pp_predicates (* dependencies *) fmt machines = |
| 758 | 716 |
let pp_preds comment pp = |
| 759 |
pp_print_list |
|
| 760 |
~pp_open_box:pp_open_vbox0 |
|
| 761 |
~pp_prologue:(pp_print_endcut comment) |
|
| 762 |
pp |
|
| 763 |
~pp_epilogue:pp_print_cutcut in |
|
| 764 |
fprintf fmt |
|
| 765 |
"%a%a%a%a%a%a" |
|
| 766 |
(pp_preds "/* ACSL `valid` predicates */" |
|
| 767 |
pp_mem_valid_def) machines |
|
| 768 |
(pp_preds "/* ACSL `memory pack` simulations */" |
|
| 769 |
pp_memory_pack_defs) machines |
|
| 770 |
(pp_preds "/* ACSL initialization annotations */" |
|
| 771 |
pp_initialization_def) machines |
|
| 772 |
(pp_preds "/* ACSL reset cleared annotations */" |
|
| 773 |
pp_reset_cleared_def) machines |
|
| 774 |
(pp_preds "/* ACSL transition annotations */" |
|
| 775 |
pp_transition_defs) machines |
|
| 717 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
| 718 |
~pp_prologue:(pp_print_endcut comment) pp ~pp_epilogue:pp_print_cutcut |
|
| 719 |
in |
|
| 720 |
fprintf fmt "%a%a%a%a%a%a" |
|
| 721 |
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def) |
|
| 722 |
machines |
|
| 723 |
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs) |
|
| 724 |
machines |
|
| 725 |
(pp_preds "/* ACSL initialization annotations */" pp_initialization_def) |
|
| 726 |
machines |
|
| 727 |
(pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def) |
|
| 728 |
machines |
|
| 729 |
(pp_preds "/* ACSL transition annotations */" pp_transition_defs) |
|
| 730 |
machines |
|
| 776 | 731 |
(pp_preds "/* ACSL transition memory footprints lemmas */" |
| 777 |
pp_transition_footprint_lemmas) machines |
|
| 732 |
pp_transition_footprint_lemmas) |
|
| 733 |
machines |
|
| 778 | 734 |
|
| 779 | 735 |
let pp_clear_reset_spec fmt self mem m = |
| 780 | 736 |
let name = m.mname.node_id in |
| 781 |
let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) |
|
| 782 |
m.minstances in |
|
| 783 |
let mk_insts = List.map (fun x -> [x]) in |
|
| 784 |
pp_acsl_cut (fun fmt () -> |
|
| 737 |
let arws, narws = |
|
| 738 |
List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances |
|
| 739 |
in |
|
| 740 |
let mk_insts = List.map (fun x -> [ x ]) in |
|
| 741 |
pp_acsl_cut |
|
| 742 |
(fun fmt () -> |
|
| 785 | 743 |
fprintf fmt |
| 786 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\ |
|
| 787 |
@[<v 2>behavior reset:@;\ |
|
| 788 |
%a@,%a@]@,\ |
|
| 789 |
@[<v 2>behavior no_reset:@;\ |
|
| 790 |
%a@,%a@]@,\ |
|
| 791 |
complete behaviors;@,\ |
|
| 792 |
disjoint behaviors;" |
|
| 793 |
(pp_requires pp_mem_valid') (name, self) |
|
| 794 |
(pp_requires (pp_separated self mem)) (mk_insts m.minstances, []) |
|
| 744 |
"%a@,\ |
|
| 745 |
%a@,\ |
|
| 746 |
%a@,\ |
|
| 747 |
%a@,\ |
|
| 748 |
%a@,\ |
|
| 749 |
%a@,\ |
|
| 750 |
%a@,\ |
|
| 751 |
%a@,\ |
|
| 752 |
%a@,\ |
|
| 753 |
%a@,\ |
|
| 754 |
@[<v 2>behavior reset:@;\ |
|
| 755 |
%a@,\ |
|
| 756 |
%a@]@,\ |
|
| 757 |
@[<v 2>behavior no_reset:@;\ |
|
| 758 |
%a@,\ |
|
| 759 |
%a@]@,\ |
|
| 760 |
complete behaviors;@,\ |
|
| 761 |
disjoint behaviors;" |
|
| 762 |
(pp_requires pp_mem_valid') |
|
| 763 |
(name, self) |
|
| 764 |
(pp_requires (pp_separated self mem)) |
|
| 765 |
(mk_insts m.minstances, []) |
|
| 795 | 766 |
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string)) |
| 796 | 767 |
(name, mem, self) |
| 797 |
(pp_ensures (pp_memory_pack_aux |
|
| 798 |
~i:(List.length m.mspec.mmemory_packs - 2) |
|
| 799 |
pp_ptr pp_print_string)) |
|
| 768 |
(pp_ensures |
|
| 769 |
(pp_memory_pack_aux |
|
| 770 |
~i:(List.length m.mspec.mmemory_packs - 2) |
|
| 771 |
pp_ptr pp_print_string)) |
|
| 800 | 772 |
(name, mem, self) |
| 801 |
(pp_assigns pp_reset_flag') [self] |
|
| 802 |
(pp_assigns (pp_register_chain self)) (mk_insts arws) |
|
| 803 |
(pp_assigns (pp_reset_flag_chain self)) (mk_insts narws) |
|
| 804 |
(pp_assigns pp_reset_flag') [mem] |
|
| 805 |
(pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws) |
|
| 806 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws) |
|
| 807 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 1) |
|
| 808 |
(pp_ensures (pp_initialization pp_ptr)) (name, mem) |
|
| 809 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) (mem, 0) |
|
| 810 |
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem) |
|
| 811 |
) |
|
| 773 |
(pp_assigns pp_reset_flag') |
|
| 774 |
[ self ] |
|
| 775 |
(pp_assigns (pp_register_chain self)) |
|
| 776 |
(mk_insts arws) |
|
| 777 |
(pp_assigns (pp_reset_flag_chain self)) |
|
| 778 |
(mk_insts narws) |
|
| 779 |
(pp_assigns pp_reset_flag') |
|
| 780 |
[ mem ] |
|
| 781 |
(pp_assigns (pp_register_chain ~indirect:false mem)) |
|
| 782 |
(mk_insts arws) |
|
| 783 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) |
|
| 784 |
(mk_insts narws) |
|
| 785 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) |
|
| 786 |
(mem, 1) |
|
| 787 |
(pp_ensures (pp_initialization pp_ptr)) |
|
| 788 |
(name, mem) |
|
| 789 |
(pp_assumes (pp_equal pp_reset_flag' pp_print_int)) |
|
| 790 |
(mem, 0) |
|
| 791 |
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) |
|
| 792 |
(mem, mem)) |
|
| 812 | 793 |
fmt () |
| 813 | 794 |
|
| 814 | 795 |
let pp_set_reset_spec fmt self mem m = |
| 815 | 796 |
let name = m.mname.node_id in |
| 816 |
pp_acsl_cut (fun fmt () -> |
|
| 817 |
fprintf fmt |
|
| 818 |
"%a@,%a@,%a" |
|
| 819 |
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self) |
|
| 820 |
(pp_ensures (pp_equal pp_reset_flag' pp_print_int)) (mem, 1) |
|
| 821 |
(pp_assigns pp_reset_flag') [self; mem]) |
|
| 797 |
pp_acsl_cut |
|
| 798 |
(fun fmt () -> |
|
| 799 |
fprintf fmt "%a@,%a@,%a" |
|
| 800 |
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) |
|
| 801 |
(name, mem, self) |
|
| 802 |
(pp_ensures (pp_equal pp_reset_flag' pp_print_int)) |
|
| 803 |
(mem, 1) |
|
| 804 |
(pp_assigns pp_reset_flag') |
|
| 805 |
[ self; mem ]) |
|
| 822 | 806 |
fmt () |
| 823 | 807 |
|
| 824 | 808 |
let pp_step_spec fmt machines self mem m = |
| 825 | 809 |
let name = m.mname.node_id in |
| 826 | 810 |
let insts = instances machines m in |
| 827 | 811 |
let insts' = powerset_instances insts in |
| 828 |
let insts'' = List.(filter (fun l -> l <> []) |
|
| 829 |
(map (filter (fun (_, (td, _)) -> |
|
| 830 |
not (Arrow.td_is_arrow td))) insts)) in |
|
| 812 |
let insts'' = |
|
| 813 |
List.( |
|
| 814 |
filter |
|
| 815 |
(fun l -> l <> []) |
|
| 816 |
(map (filter (fun (_, (td, _)) -> not (Arrow.td_is_arrow td))) insts)) |
|
| 817 |
in |
|
| 831 | 818 |
let inputs = m.mstep.step_inputs in |
| 832 | 819 |
let outputs = m.mstep.step_outputs in |
| 833 |
pp_acsl_cut (fun fmt () -> |
|
| 820 |
pp_acsl_cut |
|
| 821 |
(fun fmt () -> |
|
| 834 | 822 |
if fst (get_stateless_status m) then |
| 835 |
fprintf fmt |
|
| 836 |
"%a@,%a@,%a@,%a"
|
|
| 837 |
(pp_requires (pp_valid pp_var_decl)) outputs
|
|
| 838 |
(pp_requires pp_separated') outputs
|
|
| 839 |
(pp_assigns pp_ptr_decl) outputs |
|
| 823 |
fprintf fmt "%a@,%a@,%a@,%a"
|
|
| 824 |
(pp_requires (pp_valid pp_var_decl))
|
|
| 825 |
outputs |
|
| 826 |
(pp_requires pp_separated') |
|
| 827 |
outputs (pp_assigns pp_ptr_decl) outputs
|
|
| 840 | 828 |
(pp_ensures (pp_transition_aux'' m)) |
| 841 | 829 |
(name, inputs, [], outputs, "", "") |
| 842 | 830 |
else |
| 843 | 831 |
fprintf fmt |
| 844 | 832 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a" |
| 845 |
(pp_requires (pp_valid pp_var_decl)) outputs |
|
| 846 |
(pp_requires pp_mem_valid') (name, self) |
|
| 847 |
(pp_requires (pp_separated self mem)) (insts', outputs) |
|
| 833 |
(pp_requires (pp_valid pp_var_decl)) |
|
| 834 |
outputs |
|
| 835 |
(pp_requires pp_mem_valid') |
|
| 836 |
(name, self) |
|
| 837 |
(pp_requires (pp_separated self mem)) |
|
| 838 |
(insts', outputs) |
|
| 848 | 839 |
(pp_requires (pp_memory_pack_aux pp_ptr pp_print_string)) |
| 849 | 840 |
(name, mem, self) |
| 850 | 841 |
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) |
| 851 | 842 |
(name, mem, self) |
| 852 |
(pp_ensures (pp_transition_aux m (pp_old pp_ptr) |
|
| 853 |
pp_ptr pp_var_decl pp_ptr_decl)) |
|
| 843 |
(pp_ensures |
|
| 844 |
(pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl |
|
| 845 |
pp_ptr_decl)) |
|
| 854 | 846 |
(name, inputs, [], outputs, mem, mem) |
| 855 | 847 |
(pp_assigns pp_ptr_decl) outputs |
| 856 |
(pp_assigns (pp_reg self)) m.mmemory |
|
| 857 |
(pp_assigns pp_reset_flag') [self] |
|
| 858 |
(pp_assigns (pp_memory self)) (memories insts') |
|
| 859 |
(pp_assigns (pp_register_chain self)) insts |
|
| 860 |
(pp_assigns (pp_reset_flag_chain self)) insts'' |
|
| 861 |
(pp_assigns (pp_reg mem)) m.mmemory |
|
| 862 |
(pp_assigns pp_reset_flag') [mem] |
|
| 863 |
(pp_assigns (pp_memory ~indirect:false mem)) (memories insts') |
|
| 864 |
(pp_assigns (pp_register_chain ~indirect:false mem)) insts |
|
| 865 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts'' |
|
| 866 |
) |
|
| 848 |
(pp_assigns (pp_reg self)) |
|
| 849 |
m.mmemory |
|
| 850 |
(pp_assigns pp_reset_flag') |
|
| 851 |
[ self ] |
|
| 852 |
(pp_assigns (pp_memory self)) |
|
| 853 |
(memories insts') |
|
| 854 |
(pp_assigns (pp_register_chain self)) |
|
| 855 |
insts |
|
| 856 |
(pp_assigns (pp_reset_flag_chain self)) |
|
| 857 |
insts'' |
|
| 858 |
(pp_assigns (pp_reg mem)) |
|
| 859 |
m.mmemory |
|
| 860 |
(pp_assigns pp_reset_flag') |
|
| 861 |
[ mem ] |
|
| 862 |
(pp_assigns (pp_memory ~indirect:false mem)) |
|
| 863 |
(memories insts') |
|
| 864 |
(pp_assigns (pp_register_chain ~indirect:false mem)) |
|
| 865 |
insts |
|
| 866 |
(pp_assigns (pp_reset_flag_chain ~indirect:false mem)) |
|
| 867 |
insts'') |
|
| 867 | 868 |
fmt () |
| 868 | 869 |
|
| 869 |
let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with |
|
| 870 |
let pp_ghost_instr_code m self fmt instr = |
|
| 871 |
match instr.instr_desc with |
|
| 870 | 872 |
| MStateAssign (x, v) -> |
| 871 | 873 |
fprintf fmt "@,%a" |
| 872 |
(pp_acsl_line |
|
| 873 |
(pp_ghost |
|
| 874 |
(pp_assign m self (pp_c_var_read m)))) |
|
| 874 |
(pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m)))) |
|
| 875 | 875 |
(x, v) |
| 876 | 876 |
| MResetAssign b -> |
| 877 |
fprintf fmt "@,%a" |
|
| 878 |
(pp_acsl_line |
|
| 879 |
(pp_ghost |
|
| 880 |
(pp_reset_assign self))) |
|
| 881 |
b |
|
| 877 |
fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b |
|
| 882 | 878 |
| MSetReset inst -> |
| 883 | 879 |
let td, _ = List.assoc inst m.minstances in |
| 884 | 880 |
if Arrow.td_is_arrow td then |
| 885 |
fprintf fmt "@,%a;" |
|
| 886 |
(pp_acsl_line |
|
| 887 |
(pp_ghost |
|
| 888 |
(pp_arrow_reset_ghost self))) |
|
| 889 |
inst |
|
| 890 |
| _ -> () |
|
| 881 |
fprintf fmt "@,%a;" |
|
| 882 |
(pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self))) |
|
| 883 |
inst |
|
| 884 |
| _ -> |
|
| 885 |
() |
|
| 891 | 886 |
|
| 892 | 887 |
let pp_step_instr_spec m self mem fmt instr = |
| 893 | 888 |
fprintf fmt "%a%a" |
| 894 |
(pp_ghost_instr_code m mem) instr |
|
| 889 |
(pp_ghost_instr_code m mem) |
|
| 890 |
instr |
|
| 895 | 891 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut |
| 896 | 892 |
(pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m)))) |
| 897 | 893 |
instr.instr_spec |
| ... | ... | |
| 899 | 895 |
let pp_ghost_parameter mem fmt inst = |
| 900 | 896 |
GhostProto.pp_ghost_parameters ~cut:false fmt |
| 901 | 897 |
(match inst with |
| 902 |
| Some inst -> |
|
| 903 |
[inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)] |
|
| 904 |
| None -> |
|
| 905 |
[mem, pp_print_string]) |
|
| 906 |
|
|
| 898 |
| Some inst -> |
|
| 899 |
[ (inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)) ] |
|
| 900 |
| None -> |
|
| 901 |
[ mem, pp_print_string ]) |
|
| 907 | 902 |
end |
| 908 | 903 |
|
| 909 | 904 |
(**************************************************************************) |
| ... | ... | |
| 911 | 906 |
(**************************************************************************) |
| 912 | 907 |
|
| 913 | 908 |
module MakefileMod = struct |
| 914 |
|
|
| 915 | 909 |
let other_targets fmt basename _nodename dependencies = |
| 916 | 910 |
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@."; |
| 917 | 911 |
(* EACSL version of library file . c *) |
| 918 | 912 |
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename; |
| 919 | 913 |
fprintf fmt |
| 920 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." |
|
| 914 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on \ |
|
| 915 |
e-acsl -print -ocode %s_eacsl.c@." |
|
| 921 | 916 |
basename basename; |
| 922 | 917 |
fprintf fmt "@."; |
| 923 | 918 |
fprintf fmt "@."; |
| 924 | 919 |
|
| 925 |
(* EACSL version of library file . c + main .c *) |
|
| 926 |
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename; |
|
| 927 |
fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@." |
|
| 920 |
(* EACSL version of library file . c + main .c *) |
|
| 921 |
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename |
|
| 922 |
basename basename; |
|
| 923 |
fprintf fmt |
|
| 924 |
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c \ |
|
| 925 |
-then-on e-acsl -print -ocode %s_main_eacsl.i@." |
|
| 928 | 926 |
basename basename basename; |
| 929 | 927 |
(* Ugly hack to deal with eacsl bugs *) |
| 930 |
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename; |
|
| 928 |
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" |
|
| 929 |
basename basename; |
|
| 931 | 930 |
fprintf fmt "@."; |
| 932 | 931 |
fprintf fmt "@."; |
| 933 | 932 |
|
| 934 | 933 |
(* EACSL version of binary *) |
| 935 | 934 |
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename; |
| 936 |
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
|
|
| 935 |
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
|
|
| 936 |
basename; |
|
| 937 |
(* compiling instrumented lib + main *) |
|
| 937 | 938 |
C_backend_makefile.fprintf_dependencies fmt dependencies; |
| 938 |
fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
|
|
| 939 |
fprintf fmt |
|
| 940 |
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
|
|
| 941 |
%s_main_eacsl.o %a@." |
|
| 939 | 942 |
basename |
| 940 |
(Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name)) |
|
| 943 |
(Utils.fprintf_list ~sep:" " (fun fmt dep -> |
|
| 944 |
Format.fprintf fmt "%s.o" dep.name)) |
|
| 941 | 945 |
(C_backend_makefile.compiled_dependencies dependencies) |
| 942 | 946 |
("${FRAMACEACSL}/e_acsl.c "
|
| 943 |
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
|
| 944 |
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
|
| 947 |
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
|
| 948 |
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
|
| 945 | 949 |
basename |
| 946 | 950 |
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) |
| 947 |
(C_backend_makefile.lib_dependencies dependencies) |
|
| 948 |
; |
|
| 951 |
(C_backend_makefile.lib_dependencies dependencies); |
|
| 949 | 952 |
fprintf fmt "@." |
| 950 |
|
|
| 951 | 953 |
end |
| 952 | 954 |
|
| 953 | 955 |
(* Local Variables: *) |
Also available in: Unified diff
reformatting