Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
| src/normalization.ml | ||
|---|---|---|
| 90 | 90 |
var_dec_clock = dummy_clock_dec; |
| 91 | 91 |
var_dec_const = false; |
| 92 | 92 |
var_dec_value = None; |
| 93 |
var_parent_nodeid = Some node.node_id; |
|
| 93 | 94 |
var_type = ty; |
| 94 | 95 |
var_clock = ck; |
| 95 | 96 |
var_loc = loc |
| ... | ... | |
| 167 | 168 |
(Clocks.clock_list_of_clock expr.expr_clock) in |
| 168 | 169 |
let new_def = |
| 169 | 170 |
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
| 170 |
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
|
| 171 |
in |
|
| 172 |
(* Typing and Registering machine type *) |
|
| 173 |
let _ = Machine_types.type_def node new_aliases expr in |
|
| 174 |
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
|
| 171 | 175 |
else |
| 172 | 176 |
(defs, vars), expr |
| 173 | 177 |
|
| ... | ... | |
| 420 | 424 |
) (vars, [], []) node.node_asserts in |
| 421 | 425 |
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout |
| 422 | 426 |
vars and initial locals ones *) |
| 423 |
let new_locals = node.node_locals @ new_locals in (* we add again, at the |
|
| 427 |
|
|
| 428 |
let all_locals = node.node_locals @ new_locals in (* we add again, at the |
|
| 424 | 429 |
beginning of the list the |
| 425 | 430 |
local declared ones *) |
| 426 | 431 |
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) |
| 427 | 432 |
|
| 433 |
|
|
| 434 |
(* Updating annotations: traceability and machine types for fresh variables *) |
|
| 435 |
|
|
| 436 |
(* Compute traceability info: |
|
| 437 |
- gather newly bound variables |
|
| 438 |
- compute the associated expression without aliases |
|
| 439 |
*) |
|
| 428 | 440 |
let new_annots = |
| 429 | 441 |
if !Options.traces then |
| 430 | 442 |
begin |
| 431 |
(* Compute traceability info: |
|
| 432 |
- gather newly bound variables |
|
| 433 |
- compute the associated expression without aliases |
|
| 434 |
*) |
|
| 435 |
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in |
|
| 443 |
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in |
|
| 436 | 444 |
let norm_traceability = {
|
| 437 | 445 |
annots = List.map (fun v -> |
| 438 | 446 |
let eq = |
| ... | ... | |
| 446 | 454 |
in |
| 447 | 455 |
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in |
| 448 | 456 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
| 457 |
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; |
|
| 449 | 458 |
(["traceability"], pair) |
| 450 | 459 |
) diff_vars; |
| 451 | 460 |
annot_loc = Location.dummy_loc |
| ... | ... | |
| 457 | 466 |
node.node_annot |
| 458 | 467 |
in |
| 459 | 468 |
|
| 469 |
let new_annots = |
|
| 470 |
List.fold_left (fun annots v -> |
|
| 471 |
if Machine_types.is_exportable v then |
|
| 472 |
let typ = Machine_types.get_specified_type v in |
|
| 473 |
let typ_name = Machine_types.type_name typ in |
|
| 474 |
|
|
| 475 |
let loc = v.var_loc in |
|
| 476 |
let typ_as_string = |
|
| 477 |
mkexpr |
|
| 478 |
loc |
|
| 479 |
(Expr_const |
|
| 480 |
(Const_string typ_name)) |
|
| 481 |
in |
|
| 482 |
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in |
|
| 483 |
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword; |
|
| 484 |
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
|
|
| 485 |
else |
|
| 486 |
annots |
|
| 487 |
) new_annots new_locals |
|
| 488 |
in |
|
| 460 | 489 |
let node = |
| 461 | 490 |
{ node with
|
| 462 |
node_locals = new_locals;
|
|
| 491 |
node_locals = all_locals;
|
|
| 463 | 492 |
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs); |
| 464 | 493 |
node_asserts = asserts; |
| 465 | 494 |
node_annot = new_annots; |
Also available in: Unified diff
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program