Project

General

Profile

Download (2.22 KB) Statistics
| Branch: | Tag: | Revision:
1
(************ Machine code types *************)
2
open Utils
3
open Lustre_types
4
open Spec_types
5

    
6
type value_t = {
7
  value_desc : value_t_desc;
8
  value_type : Types.t;
9
  value_annot : expr_annot option;
10
}
11

    
12
and value_t_desc =
13
  | Cst of constant
14
  | Var of var_decl
15
  | Fun of ident * value_t list
16
  | Array of value_t list
17
  | Access of value_t * value_t
18
  | Power of value_t * value_t
19
  | ResetFlag
20

    
21
type mc_formula_t = value_t formula_t
22

    
23
type instr_t = {
24
  instr_desc : instr_t_desc;
25
  (* main data: the content *)
26
  (* lustre_expr: expr option; (* possible representation as a lustre expression
27
     *) *)
28
  lustre_eq : eq option;
29
  (* possible representation as a lustre flow equation *)
30
  instr_spec : mc_formula_t list;
31
}
32

    
33
and instr_t_desc =
34
  | MLocalAssign of var_decl * value_t
35
  | MStateAssign of var_decl * value_t
36
  | MResetAssign of bool
37
  | MClearReset
38
  | MSetReset of ident
39
  | MNoReset of ident
40
  | MStep of var_decl list * ident * value_t list
41
  | MBranch of value_t * (label * instr_t list) list
42
  | MComment of string
43
  | MSpec of string
44

    
45
type step_t = {
46
  step_checks : (Location.t * value_t) list;
47
  step_inputs : var_decl list;
48
  step_outputs : var_decl list;
49
  step_locals : var_decl list;
50
  step_instrs : instr_t list;
51
  step_asserts : value_t list;
52
}
53

    
54
type static_call = top_decl * Dimension.t list
55

    
56
type mc_transition_t = value_t transition_t
57

    
58
type mc_memory_pack_t = value_t memory_pack_t
59

    
60
type mc_contract_t = {
61
  mc_pre: mc_formula_t;
62
  mc_post: mc_formula_t;
63
  mc_proof: proof_annotation option
64
}
65

    
66
type machine_spec = {
67
  mnode_spec : mc_contract_t node_spec_t option;
68
  mtransitions : mc_transition_t list;
69
  mmemory_packs : mc_memory_pack_t list;
70
}
71

    
72
type machine_t = {
73
  mname : node_desc;
74
  mmemory : var_decl list;
75
  mcalls : (ident * static_call) list;
76
  (* map from stateful/stateless instance to node, no internals *)
77
  minstances : (ident * static_call) list;
78
  (* sub-map of mcalls, from stateful instance to node *)
79
  minit : instr_t list;
80
  mstatic : var_decl list;
81
  (* static inputs only *)
82
  mconst : instr_t list;
83
  (* assignments of node constant locals *)
84
  mstep : step_t;
85
  mspec : machine_spec;
86
  mannot : expr_annot list;
87
  msch : Scheduling_type.schedule_report option; (* Equations scheduling *)
88
  mis_contract: bool
89
}
(50-50/99)