Revision 7aaacbc9
Added by Pierre-Loïc Garoche over 5 years ago
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 15 | 15 |
| IsInit -> Format.fprintf fmt "init" |
| 16 | 16 |
| Expr e -> Printers.pp_expr fmt e |
| 17 | 17 |
|
| 18 |
let pp_guard_list fmt gl = |
|
| 19 |
(fprintf_list ~sep:"; " |
|
| 20 |
(fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl |
|
| 21 |
|
|
| 18 | 22 |
let pp_guard_expr fmt (gl,e) = |
| 19 | 23 |
Format.fprintf fmt "%a -> %a" |
| 20 |
(fprintf_list ~sep:"; " |
|
| 21 |
(fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl |
|
| 24 |
pp_guard_list gl |
|
| 22 | 25 |
pp_elem e |
| 23 | 26 |
|
| 24 | 27 |
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel |
| ... | ... | |
| 222 | 225 |
let check_sat, clean_guard = |
| 223 | 226 |
( |
| 224 | 227 |
fun l -> |
| 228 |
(* Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; *) |
|
| 225 | 229 |
let solver = Z3.Solver.mk_simple_solver !ctx in |
| 226 | 230 |
try ( |
| 227 | 231 |
let zl = |
| ... | ... | |
| 237 | 241 |
neg_ze ze |
| 238 | 242 |
) l |
| 239 | 243 |
in |
| 244 |
(* Format.eprintf "Z3 exprs: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *) |
|
| 240 | 245 |
let status_res = Z3.Solver.check solver zl in |
| 246 |
(* Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); *) |
|
| 241 | 247 |
let sat = match status_res with |
| 242 | 248 |
| Z3.Solver.UNSATISFIABLE -> false |
| 243 | 249 |
| _ -> true in |
| ... | ... | |
| 268 | 274 |
Z3.Goal.add goal zl; |
| 269 | 275 |
let goal' = Z3.Goal.simplify goal None in |
| 270 | 276 |
|
| 271 |
Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@." |
|
| 272 |
(Z3.Goal.to_string goal) |
|
| 273 |
(Z3.Goal.to_string goal') |
|
| 274 |
(Z3.Solver.string_of_status status_res) |
|
| 275 |
;
|
|
| 277 |
(* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
|
|
| 278 |
* (Z3.Goal.to_string goal)
|
|
| 279 |
* (Z3.Goal.to_string goal')
|
|
| 280 |
* (Z3.Solver.string_of_status status_res)
|
|
| 281 |
* ; *)
|
|
| 276 | 282 |
let ze = Z3.Goal.as_expr goal' in |
| 277 |
Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); |
|
| 278 |
(* let l = |
|
| 279 |
match zexpr_to_expr ze with |
|
| 283 |
(* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *) |
|
| 284 |
let l = |
|
| 285 |
(* zexpr_to_expr function returns a pair (is_init option, expr |
|
| 286 |
option). Since we are simplifying /pure/ expression, there |
|
| 287 |
should be not init sub-expressions here. *) |
|
| 288 |
match zexpr_to_expr ze with |
|
| 280 | 289 |
| None, None -> [] |
| 281 | 290 |
| None, Some e -> [e, true] |
| 282 | 291 |
| _ -> assert false |
| 283 |
(* | Some init, None -> [IsInit, init] |
|
| 284 |
| Some init, Some e -> [IsInit, init; Expr e, true] |
|
| 285 |
*) in |
|
| 286 |
*) |
|
| 292 |
in |
|
| 287 | 293 |
l |
| 294 |
|
|
| 295 |
|
|
| 288 | 296 |
) |
| 289 | 297 |
with Zustre_common.UnknownFunction(id, msg) -> ( |
| 290 | 298 |
report ~level:1 msg; |
| ... | ... | |
| 317 | 325 |
(* Filtering out trivial cases. More semantics ones would have to be |
| 318 | 326 |
addressed later *) |
| 319 | 327 |
let check (gexpr, posneg) l = |
| 328 |
(* Format.eprintf "Checking %a=%b in %a@ " |
|
| 329 |
* pp_elem gexpr |
|
| 330 |
* posneg |
|
| 331 |
* pp_guard_list l |
|
| 332 |
* ; *) |
|
| 320 | 333 |
(* Check if gepxr is part of l *) |
| 321 |
let sel_fun = select_elem gexpr in |
|
| 322 |
if List.exists sel_fun l then |
|
| 334 |
let sel_fun = select_elem gexpr in |
|
| 335 |
let ok, res = |
|
| 336 |
if List.exists sel_fun l then ( |
|
| 323 | 337 |
(* Checking the guard value posneg *) |
| 324 | 338 |
let _, status = List.find sel_fun l in |
| 339 |
(* Format.eprintf "Found %a in %a. @ Checking status (%b).@ " |
|
| 340 |
* pp_elem gexpr |
|
| 341 |
* pp_guard_list l |
|
| 342 |
* (status=posneg) |
|
| 343 |
* ; *) |
|
| 325 | 344 |
status=posneg, l |
| 326 |
else |
|
| 345 |
) |
|
| 346 |
else ( |
|
| 347 |
(* Format.eprintf "Not found.@ "; *) |
|
| 327 | 348 |
(* Valid: no overlap *) |
| 328 | 349 |
(* Individual checkat *) |
| 329 | 350 |
let ok, e = check_sat [gexpr, posneg] in |
| 351 |
(* let ok, e = true, [gexpr, posneg] in (* TODO solve the issue with check_sat *) *) |
|
| 352 |
(* Format.eprintf "Check_sat? %b@ " ok; *) |
|
| 330 | 353 |
if ok then |
| 331 | 354 |
let l = e@l in |
| 332 | 355 |
let ok, l = check_sat l in |
| 356 |
(* let ok, l = true, l in (* TODO solve the issue with check_sat *) *) |
|
| 333 | 357 |
ok, l |
| 334 | 358 |
else |
| 335 |
true, l |
|
| 359 |
false, [] |
|
| 360 |
) |
|
| 361 |
in |
|
| 362 |
(* Format.eprintf "Check sat res: %a@ " |
|
| 363 |
* pp_guard_list res; *) |
|
| 364 |
ok, res |
|
| 336 | 365 |
in |
| 337 | 366 |
let ok, gl = |
| 338 | 367 |
List.fold_left ( |
| ... | ... | |
| 351 | 380 |
check fresh_g gl |
| 352 | 381 |
) |
| 353 | 382 |
else |
| 354 |
ok, []
|
|
| 383 |
false, []
|
|
| 355 | 384 |
|
| 385 |
(* DEBUG |
|
| 386 |
let combine_guards ?(fresh=None) gl1 gl2 = |
|
| 387 |
true, |
|
| 388 |
(match fresh with None -> [] | Some (gexpr, posneg) -> [gexpr, posneg])@gl1@gl2 |
|
| 389 |
*) |
|
| 356 | 390 |
(* Encode "If gel1=posneg then gel2": |
| 357 | 391 |
- Compute the combination of guarded exprs in gel1 and gel2: |
| 358 | 392 |
- Each guarded_expr in gel1 is transformed as a guard: the |
| ... | ... | |
| 365 | 399 |
fun accu (g2,e2) -> |
| 366 | 400 |
List.fold_left ( |
| 367 | 401 |
fun accu (g1,e1) -> |
| 402 |
(* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ " |
|
| 403 |
* pp_elem e1 |
|
| 404 |
* posneg |
|
| 405 |
* pp_guard_list g1 |
|
| 406 |
* pp_guard_list g2; *) |
|
| 407 |
|
|
| 368 | 408 |
let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in |
| 409 |
(* Format.eprintf "@]@ Result is [%a]@ " |
|
| 410 |
* pp_guard_list gl; *) |
|
| 411 |
|
|
| 369 | 412 |
if ok then |
| 370 | 413 |
(gl, e2)::accu |
| 371 |
else |
|
| 414 |
else ( |
|
| 415 |
|
|
| 372 | 416 |
accu |
| 417 |
) |
|
| 373 | 418 |
) accu gel1 |
| 374 | 419 |
) [] gel2 |
| 375 | 420 |
|
| 376 | 421 |
let rec rewrite defs expr : guarded_expr list = |
| 377 | 422 |
let rewrite = rewrite defs in |
| 378 |
match expr.expr_desc with |
|
| 379 |
| Expr_appl (id, args, None) -> |
|
| 380 |
let args = rewrite args in |
|
| 381 |
List.map (fun (guards, e) -> |
|
| 423 |
let res = |
|
| 424 |
match expr.expr_desc with |
|
| 425 |
| Expr_appl (id, args, None) -> |
|
| 426 |
let args = rewrite args in |
|
| 427 |
List.map (fun (guards, e) -> |
|
| 382 | 428 |
guards, |
| 383 | 429 |
Expr {expr with expr_desc = Expr_appl(id, deelem e, None)}
|
| 384 |
) args |
|
| 385 |
| Expr_const _ -> [[], Expr expr] |
|
| 386 |
| Expr_ident id -> |
|
| 387 |
if Hashtbl.mem defs id then |
|
| 388 |
Hashtbl.find defs id |
|
| 389 |
else |
|
| 390 |
(* id should be an input *) |
|
| 391 |
[[], Expr expr] |
|
| 392 |
| Expr_ite (g, e1, e2) -> |
|
| 393 |
let g = rewrite g and |
|
| 394 |
e1 = rewrite e1 and |
|
| 395 |
e2 = rewrite e2 in |
|
| 396 |
(concatenate_ge g true e1)@ |
|
| 397 |
(concatenate_ge g false e2) |
|
| 398 |
| Expr_merge (g, branches) -> |
|
| 399 |
assert false (* TODO: deal with merges *) |
|
| 400 |
|
|
| 401 |
| Expr_when (e, _, _) -> rewrite e |
|
| 402 |
| Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *) |
|
| 403 |
| Expr_tuple el -> |
|
| 404 |
(* Each expr is associated to its flatten guarded expr list *) |
|
| 405 |
let gell = List.map rewrite el in |
|
| 406 |
(* Computing all combinations: we obtain a list of guarded tuple *) |
|
| 407 |
let rec aux gell : (guard * expr list) list = |
|
| 408 |
match gell with |
|
| 409 |
| [] -> assert false (* Not happening *) |
|
| 410 |
| [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel |
|
| 411 |
| gel::getl -> |
|
| 412 |
let getl = aux getl in |
|
| 413 |
List.fold_left ( |
|
| 414 |
fun accu (g,e) -> |
|
| 415 |
List.fold_left ( |
|
| 430 |
) args
|
|
| 431 |
| Expr_const _ -> [[], Expr expr]
|
|
| 432 |
| Expr_ident id ->
|
|
| 433 |
if Hashtbl.mem defs id then
|
|
| 434 |
Hashtbl.find defs id
|
|
| 435 |
else
|
|
| 436 |
(* id should be an input *)
|
|
| 437 |
[[], Expr expr]
|
|
| 438 |
| Expr_ite (g, e1, e2) ->
|
|
| 439 |
let g = rewrite g and
|
|
| 440 |
e1 = rewrite e1 and
|
|
| 441 |
e2 = rewrite e2 in
|
|
| 442 |
(concatenate_ge g true e1)@
|
|
| 443 |
(concatenate_ge g false e2)
|
|
| 444 |
| Expr_merge (g, branches) ->
|
|
| 445 |
assert false (* TODO: deal with merges *)
|
|
| 446 |
|
|
| 447 |
| Expr_when (e, _, _) -> rewrite e
|
|
| 448 |
| Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
|
|
| 449 |
| Expr_tuple el ->
|
|
| 450 |
(* Each expr is associated to its flatten guarded expr list *)
|
|
| 451 |
let gell = List.map rewrite el in
|
|
| 452 |
(* Computing all combinations: we obtain a list of guarded tuple *)
|
|
| 453 |
let rec aux gell : (guard * expr list) list =
|
|
| 454 |
match gell with
|
|
| 455 |
| [] -> assert false (* Not happening *)
|
|
| 456 |
| [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
|
|
| 457 |
| gel::getl ->
|
|
| 458 |
let getl = aux getl in
|
|
| 459 |
List.fold_left (
|
|
| 460 |
fun accu (g,e) ->
|
|
| 461 |
List.fold_left (
|
|
| 416 | 462 |
fun accu (gl, minituple) -> |
| 417 | 463 |
let is_compat, guard_comb = combine_guards g gl in |
| 418 | 464 |
if is_compat then |
| ... | ... | |
| 420 | 466 |
new_gt::accu |
| 421 | 467 |
else |
| 422 | 468 |
accu |
| 423 |
|
|
| 469 |
|
|
| 424 | 470 |
) accu getl |
| 425 |
) [] gel |
|
| 426 |
in |
|
| 427 |
let gtuples = aux gell in |
|
| 428 |
(* Rebuilding the valid type: guarded expr list (with tuple exprs) *) |
|
| 429 |
List.map (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
|
|
| 430 |
| Expr_fby _ |
|
| 431 |
| Expr_appl _ |
|
| 432 |
(* Should be removed by mormalization and inlining *) |
|
| 433 |
-> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false |
|
| 434 |
| Expr_array _ | Expr_access _ | Expr_power _ |
|
| 435 |
(* Arrays not handled here yet *) |
|
| 436 |
-> assert false |
|
| 437 |
| Expr_pre _ -> (* Not rewriting mem assign *) |
|
| 438 |
assert false |
|
| 471 |
) [] gel |
|
| 472 |
in |
|
| 473 |
let gtuples = aux gell in |
|
| 474 |
(* Rebuilding the valid type: guarded expr list (with tuple exprs) *) |
|
| 475 |
List.map (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
|
|
| 476 |
| Expr_fby _ |
|
| 477 |
| Expr_appl _ |
|
| 478 |
(* Should be removed by mormalization and inlining *) |
|
| 479 |
-> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false |
|
| 480 |
| Expr_array _ | Expr_access _ | Expr_power _ |
|
| 481 |
(* Arrays not handled here yet *) |
|
| 482 |
-> assert false |
|
| 483 |
| Expr_pre _ -> (* Not rewriting mem assign *) |
|
| 484 |
assert false |
|
| 485 |
in |
|
| 486 |
(* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ " |
|
| 487 |
* Printers.pp_expr expr |
|
| 488 |
* (Utils.fprintf_list ~sep:"@ " |
|
| 489 |
* pp_guard_expr) res; *) |
|
| 490 |
res |
|
| 439 | 491 |
and add_def defs vid expr = |
| 440 |
Hashtbl.add defs vid (rewrite defs expr) |
|
| 492 |
let vid_defs = rewrite defs expr in |
|
| 493 |
(* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@." |
|
| 494 |
* vid |
|
| 495 |
* Printers.pp_expr expr |
|
| 496 |
* ( |
|
| 497 |
* (Utils.fprintf_list ~sep:"@ " |
|
| 498 |
* pp_guard_expr)) vid_defs; *) |
|
| 499 |
Hashtbl.add defs vid vid_defs |
|
| 441 | 500 |
|
| 442 | 501 |
(* Takes a list of guarded exprs (ge) and a guard |
| 443 | 502 |
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore. |
| ... | ... | |
| 608 | 667 |
let _ = |
| 609 | 668 |
List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts |
| 610 | 669 |
in |
| 670 |
|
|
| 611 | 671 |
|
| 612 | 672 |
(* Registering node equations: identifying mem definitions and |
| 613 | 673 |
storing others in the "defs" hashtbl. *) |
| ... | ... | |
| 685 | 745 |
build_switch_sys update_defs [] |
| 686 | 746 |
in |
| 687 | 747 |
clean_sys sw_init, clean_sys sw_sys |
| 748 |
|
|
Also available in: Unified diff
Better extraction in lustrev-seal