Project

General

Profile

« Previous | Next » 

Revision 75c459f4

Added by LĂ©lio Brun 9 months ago

start with Spec AST generation

View differences:

src/backends/Ada/ada_backend_adb.ml
127 127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128 128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129 129
      | MLocalAssign (ident, value) -> 
130
          { instr_desc = MStateAssign (ident, value);
131
            lustre_eq= instr.lustre_eq }
130
        { instr with instr_desc = MStateAssign (ident, value) }
132 131
      | _ -> instr
133 132
    in
134 133
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
......
150 149
  **)
151 150
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
152 151
    let build_assign = function var ->
153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
152
      mkinstr Spec_types.True (MStateAssign (var, mk_default_value var.var_type))
154 153
    in
155 154
    let env, memory = match m_spec_opt with
156 155
      | None -> env, m.mmemory
src/backends/Ada/misc_lustre_function.ml
267 267
              in
268 268
              let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in
269 269
              { instr_desc = assign;
270
                lustre_eq  = None
270
                lustre_eq  = None;
271
                instr_spec = Spec_types.True
271 272
              }
272 273
            in
273 274
            let mkval_var id = {
src/corelang.ml
257 257
  e
258 258

  
259 259

  
260
let mkinstr ?lustre_eq i =
261
  {
262
    instr_desc = i;
263
    (* lustre_expr = lustre_expr; *)
264
    lustre_eq = lustre_eq;
265
  }
260
let mkinstr ?lustre_eq instr_spec instr_desc = {
261
  instr_desc;
262
  (* lustre_expr = lustre_expr; *)
263
  instr_spec;
264
  lustre_eq;
265
}
266 266

  
267 267
let get_instr_desc i = i.instr_desc
268 268
let update_instr_desc i id = { i with instr_desc = id }
src/corelang.mli
45 45
val mktop: top_decl_desc -> top_decl
46 46

  
47 47
(* constructor for machine types *)
48
val mkinstr: (* ?lustre_expr:expr ->  *)?lustre_eq: eq -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
48
val mkinstr: (* ?lustre_expr:expr ->  *)?lustre_eq: eq -> Machine_code_types.value_t Spec_types.formula_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
49 49
val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc
50 50
val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
51 51
  
src/dune
22 22
   delay
23 23
   machine_code_types
24 24
   spec_types
25
   spec_common
25 26
   scheduling_type
26 27
   log
27 28
   printers
src/machine_code.ml
12 12
open Lustre_types
13 13
open Machine_code_types
14 14
open Machine_code_common
15
open Spec_types
16
open Spec_common
15 17
open Corelang
16 18
open Clocks
17 19
open Causality
20
open Utils
18 21

  
19 22
exception NormalizationError
20 23

  
......
58 61

  
59 62
let translate_ident env id =
60 63
  (* Format.eprintf "trnaslating ident: %s@." id; *)
61
  try (* id is a var that shall be visible here , ie. in vars *)
64
  (* id is a var that shall be visible here , ie. in vars *)
65
  try
62 66
    let var_id = env.get_var id in
63 67
    mk_val (Var var_id) var_id.var_type
64 68
  with Not_found ->
65
  try (* id is a constant *)
69

  
70
 (* id is a constant *)
71
  try
66 72
    let vdecl = (Corelang.var_decl_of_const
67 73
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
68 74
    in
69 75
    mk_val (Var vdecl) vdecl.var_type
70 76
  with Not_found ->
71
  (* id is a tag, getting its type in the list of declared enums *)
77

  
78
   (* id is a tag, getting its type in the list of declared enums *)
72 79
  try
73 80
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
74 81
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
......
76 83
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
77 84
    assert false
78 85

  
79
let rec control_on_clock env ck inst =
80
  match (Clocks.repr ck).cdesc with
81
  | Con (ck1, cr, l) ->
82
    let id = Clocks.const_of_carrier cr in
83
    control_on_clock env ck1
84
      (mkinstr (MBranch (translate_ident env id, [l, [inst]])))
85
  | _ -> inst
86

  
87 86

  
88 87
(* specialize predefined (polymorphic) operators wrt their instances,
89 88
   so that the C semantics is preserved *)
......
158 157
      [translate_act (y, t)]
159 158
      [translate_act (y, e)]
160 159
  | Expr_merge (x, hl) ->
161
    mkinstr ~lustre_eq
162
      (MBranch (translate_ident x,
163
                List.map (fun (t,  h) -> t, [translate_act (y, h)]) hl))
164
  | _ -> mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr))
165

  
166
let reset_instance env i r c =
167
  match r with
168
  | Some r ->
169
    [control_on_clock env c
170
       (mk_conditional
171
          (translate_guard env r)
172
          [mkinstr (MReset i)]
173
          [mkinstr (MNoReset i)])]
174
  | None -> []
175

  
160
    mk_branch ~lustre_eq
161
      (translate_ident x)
162
      (List.map (fun (t, h) -> t, [translate_act (y, h)]) hl)
163
  | _ ->
164
    mk_assign ~lustre_eq y (translate_expr expr)
176 165

  
177 166
(* Datastructure updated while visiting equations *)
178 167
type machine_ctx = {
179
  m: VSet.t; (* Memories *)
168
  (* Memories *)
169
  m: VSet.t;
170
  (* Reset instructions *)
180 171
  si: instr_t list;
181
  j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
172
  (* Instances *)
173
  j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
174
  (* Step instructions *)
182 175
  s: instr_t list;
176
  (* Memory pack spec *)
177
  mp: mc_formula_t list;
178
  (* Clocked spec *)
179
  c: mc_formula_t IMap.t;
180
  (* Transition spec *)
181
  t: mc_formula_t list;
183 182
}
184 183

  
185
let ctx_init = { m = VSet.empty; (* memories *)
186
                 si = []; (* init instr *)
187
                 j = Utils.IMap.empty;
188
                 s = [] }
184
let ctx_init = {
185
  m = VSet.empty;
186
  si = [];
187
  j = IMap.empty;
188
  s = [];
189
  mp = [];
190
  c = IMap.empty;
191
  t = []
192
}
189 193

  
190 194
(****************************************************************)
191 195
(* Main function to translate equations into this machine context we
192 196
   are building *) 
193 197
(****************************************************************)
194 198

  
199
let mk_control id vs v l inst =
200
  mkinstr
201
    (Imply (mk_clocked_on id vs, inst.instr_spec))
202
    (MBranch (v, [l, [inst]]))
203

  
204
let control_on_clock env ctx ck inst =
205
  let rec aux (ck_ids, vs, ctx, inst as acc) ck =
206
    match (Clocks.repr ck).cdesc with
207
    | Con (ck, cr, l) ->
208
      let id = Clocks.const_of_carrier cr in
209
      let v = translate_ident env id in
210
      let ck_ids' = String.concat "_" ck_ids in
211
      let id' = id ^ "_" ^ ck_ids' in
212
      let ck_spec = mk_condition v l in
213
      aux (id :: ck_ids,
214
           v :: vs,
215
           { ctx
216
             with c = IMap.add id ck_spec
217
                      (IMap.add id'
218
                         (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
219
           },
220
           mk_control id' (v :: vs) v l inst) ck
221
    | _ -> acc
222
  in
223
  let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
224
  ctx, inst
225

  
226
let reset_instance env i r c =
227
  match r with
228
  | Some r ->
229
    [snd (control_on_clock env ctx_init c
230
            (mk_conditional
231
               (translate_guard env r)
232
               [mkinstr True (MReset i)]
233
               [mkinstr True (MNoReset i)]))]
234
  | None -> []
195 235

  
196 236

  
197 237
let translate_eq env ctx eq =
198 238
  let translate_expr = translate_expr env in
199 239
  let translate_act = translate_act env in
200
  let control_on_clock = control_on_clock env in
240
  let control_on_clock ck inst =
241
    let ctx, ins = control_on_clock env ctx ck inst in
242
    { ctx with s = ins :: ctx.s }
243
  in
201 244
  let reset_instance = reset_instance env in
202
  let mkinstr' = mkinstr ~lustre_eq:eq in
245
  let mkinstr' = mkinstr ~lustre_eq:eq True in
203 246
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
204 247
    control_on_clock ck (mkinstr' instr) in
205 248

  
......
211 254
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
212 255
    let c1 = translate_expr e1 in
213 256
    let c2 = translate_expr e2 in
257
    let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
214 258
    { ctx with
215
      si = mkinstr (MReset o) :: ctx.si;
216
      j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
217
      s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s
259
      si = mkinstr True (MReset o) :: ctx.si;
260
      j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
218 261
    }
219 262
  | [x], Expr_pre e1 when env.is_local x    ->
220 263
    let var_x = env.get_var x in
264
    let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
221 265
    { ctx with
222 266
      m = VSet.add var_x ctx.m;
223
      s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s
224 267
    }
225 268
  | [x], Expr_fby (e1, e2) when env.is_local x ->
226 269
    let var_x = env.get_var x in
270
    let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
227 271
    { ctx with
228 272
      m = VSet.add var_x ctx.m;
229 273
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
230
      s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s
231 274
    }
232 275
  | p, Expr_appl (f, arg, r)
233 276
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
......
241 284
        el [eq.eq_rhs.expr_clock] in
242 285
    let call_ck = Clock_calculus.compute_root_clock
243 286
        (Clock_predef.ck_tuple env_cks) in
287
    let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
244 288
    (*Clocks.new_var true in
245 289
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
246 290
      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
247 291
    { ctx with
248 292
      si = if Stateless.check_node node_f
249
        then ctx.si else mkinstr (MReset o) :: ctx.si;
250
      j = Utils.IMap.add o call_f ctx.j;
293
        then ctx.si else mkinstr True (MReset o) :: ctx.si;
294
      j = IMap.add o call_f ctx.j;
251 295
      s = (if Stateless.check_node node_f
252
           then [] else reset_instance o r call_ck)
253
          @ ctl ~ck:call_ck (MStep (var_p, o, vl))
254
          :: ctx.s
296
           then []
297
           else reset_instance o r call_ck)
298
          @ ctx.s
255 299
    }
256 300
  | [x], _ ->
257 301
    let var_x = env.get_var x in
258
    { ctx with
259
      s = control_on_clock eq.eq_rhs.expr_clock
260
          (translate_act (var_x, eq.eq_rhs))
261
          :: ctx.s
262
      }
302
    control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
263 303
  | _ ->
264 304
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
265 305
      Printers.pp_node_eq eq;
......
270 310
      if vdecl.var_dec_const
271 311
      then
272 312
        { eq_lhs = [vdecl.var_id];
273
          eq_rhs = Utils.desome vdecl.var_dec_value;
313
          eq_rhs = desome vdecl.var_dec_value;
274 314
          eq_loc = vdecl.var_loc
275 315
        } :: eqs
276 316
      else eqs)
......
326 366
  let ctx0 = translate_eqs env ctx_init constant_eqs in
327 367
  assert (VSet.is_empty ctx0.m);
328 368
  assert (ctx0.si = []);
329
  assert (Utils.IMap.is_empty ctx0.j);
369
  assert (IMap.is_empty ctx0.j);
330 370

  
331 371
  (* Compute ctx for all eqs *)
332 372
  let ctx = translate_eqs env ctx_init sorted_eqs in
......
371 411
    let l = VSet.elements (VSet.diff locals ctx.m) in
372 412
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
373 413
  in
374
  let mmap = Utils.IMap.bindings ctx.j in
414
  let mmap = IMap.bindings ctx.j in
375 415
  {
376 416
    mname = nd;
377 417
    mmemory = VSet.elements ctx.m;
......
417 457
    List.map
418 458
      (fun decl ->
419 459
         let node = node_of_top decl in
420
         let sch = Utils.IMap.find node.node_id node_schs in
460
         let sch = IMap.find node.node_id node_schs in
421 461
         translate_decl node sch
422 462
      ) nodes
423 463
  in
src/machine_code_common.ml
1 1
open Lustre_types
2 2
open Machine_code_types
3
open Spec_types
4
open Spec_common
3 5
open Corelang
4 6
  
5 7
let print_statelocaltag = true
......
153 155
let is_output m id =
154 156
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
155 157

  
158
let get_instr_spec i = i.instr_spec
156 159

  
157 160
let mk_conditional ?lustre_eq c t e =
158
  mkinstr ?lustre_eq:lustre_eq  (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
159

  
160

  
161
  mkinstr ?lustre_eq
162
    (Ternary (Val c,
163
              And (List.map get_instr_spec t),
164
              And (List.map get_instr_spec e)))
165
    (MBranch(c, [
166
         (tag_true, t);
167
         (tag_false, e) ]))
168

  
169
let mk_branch ?lustre_eq c br =
170
  mkinstr ?lustre_eq
171
    (And (List.map (fun (l, instrs) ->
172
         Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
173
         br))
174
    (MBranch (c, br))
175

  
176
let mk_assign ?lustre_eq x v =
177
  mkinstr ?lustre_eq
178
    (Equal (Var x, Val v))
179
    (MLocalAssign (x, v))
161 180

  
162 181
let mk_val v t =
163 182
  { value_desc = v; 
......
178 197
    mmemory = [var_state];
179 198
    mcalls = [];
180 199
    minstances = [];
181
    minit = [mkinstr (MStateAssign(var_state, cst true))];
200
    minit = [mkinstr True (MStateAssign(var_state, cst true))];
182 201
    mstatic = [];
183 202
    mconst = [];
184 203
    mstep = {
......
187 206
      step_locals = [];
188 207
      step_checks = [];
189 208
      step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
190
			(List.map mkinstr
209
			(List.map (mkinstr True)
191 210
			[MStateAssign(var_state, cst false);
192 211
			 MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
193
                        (List.map mkinstr
212
                        (List.map (mkinstr True)
194 213
			[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
195 214
      step_asserts = [];
196 215
    };
......
354 373
 | _                   , []                               ->
355 374
   [inst1]
356 375
 | MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 ->
357
    mkinstr
376
    mkinstr True
358 377
      (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
359 378
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
360 379
   :: (List.tl insts2)
src/machine_code_common.mli
8 8
val is_stateless: Machine_code_types.machine_t -> bool
9 9
val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
10 10
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
11
val mk_branch: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> (Lustre_types.label * Machine_code_types.instr_t list) list -> Machine_code_types.instr_t
12
val mk_assign: ?lustre_eq:Lustre_types.eq -> Lustre_types.var_decl -> Machine_code_types.value_t -> Machine_code_types.instr_t
11 13
val empty_machine: Machine_code_types.machine_t
12 14
val arrow_machine: Machine_code_types.machine_t
13 15
val new_instance: Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
src/machine_code_types.ml
1 1
(************ Machine code types *************)
2 2
open Lustre_types
3 3
open Spec_types
4
  
4

  
5 5
type value_t =
6 6
  {
7 7
    value_desc: value_t_desc;
......
16 16
  | Access of value_t * value_t
17 17
  | Power of value_t * value_t
18 18

  
19
type mc_formula_t = value_t formula_t
20

  
19 21
type instr_t =
20 22
  {
21 23
    instr_desc: instr_t_desc; (* main data: the content *)
22 24
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
23 25
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
26
    instr_spec: mc_formula_t
24 27
  }
25 28
and instr_t_desc =
26 29
  | MLocalAssign of var_decl * value_t
......
45 48

  
46 49
type machine_spec = {
47 50
  mnode_spec: node_spec_t option;
48
  mtransitions: transition_t list
51
  mtransitions: value_t transition_t list
49 52
}
50 53
  
51 54
type machine_t = {
src/optimize_machine.ml
283 283
  let vdecl = { vdecl with var_type = const.const_type } in
284 284
  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
285 285
  mkinstr
286
    ~lustre_eq:lustre_eq 
286
    ~lustre_eq
287
    True
287 288
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
288 289

  
289 290
(* We do not perform this optimization on contract nodes since there
src/plugins/scopes/scopes.ml
220 220
                        
221 221
let update_machine main_node machine scopes =
222 222
  let stateassign (vdecl_mem, vdecl_orig) =
223
    mkinstr 
223
    mkinstr True
224 224
    (MStateAssign (vdecl_mem, mk_val (Var vdecl_orig) vdecl_orig.var_type))
225 225
  in
226 226
  let selection =
......
248 248
    mstep = { 
249 249
      machine.mstep with 
250 250
        step_instrs = machine.mstep.step_instrs
251
        @ (mkinstr (MComment "Registering all flows"))::(List.map stateassign new_mems)
251
        @ (mkinstr True (MComment "Registering all flows"))::(List.map stateassign new_mems)
252 252
          
253 253
    }
254 254
  }
src/spec_types.ml
4 4
  | In
5 5
  | Out
6 6

  
7
type expression_t =
8
  | Cst of constant
7
type 'a expression_t =
8
  | Val of 'a
9
  | Tag of ident
9 10
  | Var of var_decl
10 11
  | Instance of state_t * ident
11 12
  | Memory of state_t * ident
12 13

  
13 14
type predicate_t =
14
  | Atom of expression_t
15
  | Equal of predicate_t * predicate_t
16
  | Imply of predicate_t * predicate_t
17
  | Exists of var_decl list * predicate_t list
18
  | Forall of var_decl list * predicate_t list
15
  (* | Memory_pack *)
16
  | Clocked_on of ident
17
  | Transition
18
  | Initialization
19 19

  
20
type transition_t = {
20
type 'a formula_t =
21
  | True
22
  | False
23
  | Equal of 'a expression_t * 'a expression_t
24
  | And of 'a formula_t list
25
  | Or of 'a formula_t list
26
  | Imply of 'a formula_t * 'a formula_t
27
  | Exists of var_decl list * 'a formula_t
28
  | Forall of var_decl list * 'a formula_t
29
  | Ternary of 'a expression_t * 'a formula_t * 'a formula_t
30
  | Predicate of predicate_t * 'a expression_t list
31

  
32
(* type 'a simulation_t = {
33
 *   sname: node_desc;
34
 *   sindex: option int;
35
 *   sformula: 'a formula_t;
36
 * } *)
37

  
38
type 'a transition_t = {
21 39
  tname: node_desc;
22
  tindex: int;
40
  tindex: int option;
23 41
  tlocals: var_decl list;
24 42
  toutputs: var_decl list;
25
  tpredicate: predicate_t list;
43
  tformula: 'a formula_t;
26 44
}
45

  
src/utils/utils.ml
32 32
  let equal n1 n2 = n1 = n2
33 33
end
34 34

  
35
module IMap = Map.Make(IdentModule)
35
module IMap = struct
36
  include Map.Make(IdentModule)
37
  let union_l m1 m2 =
38
    merge (fun _ o1 o2 -> match o1, o2 with
39
        | None, None -> None
40
        | Some _, _ -> o1
41
        | _, Some _ -> o2) m1 m2
42
end
43

  
36 44
module ISet = Set.Make(IdentModule)
37 45
module IdentDepGraph = Imperative.Digraph.ConcreteBidirectional (IdentModule)
38 46
module TopologicalDepGraph = Topological.Make(IdentDepGraph)

Also available in: Unified diff