Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by Lélio Brun 7 months ago

work on spec generation almost done

View differences:

src/machine_code_common.ml
1 1
open Lustre_types
2 2
open Machine_code_types
3 3
open Spec_types
4
open Spec_common
5 4
open Corelang
6 5
open Utils.Format
7 6

  
......
10 9
let is_memory m id =
11 10
  (List.exists (fun o -> o.var_id = id.var_id) m.mmemory) 
12 11

  
12
let is_reset_flag id =
13
  id.var_id = "_reset"
14

  
15
let pp_vdecl fmt v =
16
  pp_print_string fmt v.var_id
17

  
13 18
let rec pp_val m fmt v =
14 19
  let pp_val = pp_val m in
15 20
  match v.value_desc with
16 21
  | Cst c         -> Printers.pp_const fmt c 
17 22
  | Var v    ->
18
     if is_memory m v then
19
       if print_statelocaltag then
20
	 fprintf fmt "{%s}" v.var_id
21
       else
22
	 pp_print_string fmt v.var_id
23
     else     
24
       if print_statelocaltag then
25
	 fprintf fmt "%s" v.var_id
26
       else
27
	 pp_print_string fmt v.var_id
28
  | Array vl      -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
23
    if is_memory m v then
24
      if print_statelocaltag then
25
        fprintf fmt "{%s}" v.var_id
26
      else
27
        pp_print_string fmt v.var_id
28
    else
29
    if print_statelocaltag then
30
      fprintf fmt "%s" v.var_id
31
    else
32
      pp_vdecl fmt v
33
  | Array vl      -> pp_print_bracketed pp_val fmt vl
29 34
  | Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
30 35
  | Power (v, n)  -> fprintf fmt "(%a^%a)" pp_val v pp_val n
31
  | Fun (n, vl)   -> fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
32

  
33
module PrintSpec = PrintSpec(struct
34
    type t = value_t
35
    type ctx = machine_t
36
    let pp_val = pp_val
37
  end)
38

  
39
let rec  pp_instr m fmt i =
40
 let     pp_val = pp_val m and
41
      pp_branch = pp_branch m in
42
  let _ =
43
    match i.instr_desc with
36
  | Fun (n, vl)   -> fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
37

  
38
module PrintSpec = struct
39

  
40
  let pp_reg fmt = function
41
    | ResetFlag -> pp_print_string fmt "{RESET}"
42
    | StateVar v -> fprintf fmt "{OUT:%a}" pp_vdecl v
43

  
44
  let pp_expr: type a. machine_t -> formatter -> (value_t, a) expression_t -> unit =
45
    fun m fmt -> function
46
      | Val v -> pp_val m fmt v
47
      | Tag t -> pp_print_string fmt t
48
      | Var v -> pp_vdecl fmt v
49
      | Memory r -> pp_reg fmt r
50

  
51
  let pp_predicate m fmt p =
52
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
53
      fun fmt e -> pp_expr m fmt e
54
    in
55
    match p with
56
    | Transition (f, inst, i, inputs, locals, outputs) ->
57
      fprintf fmt "Transition_%a<%a>%a%a"
58
        pp_print_string f
59
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
60
           pp_print_string) inst
61
        (pp_print_option pp_print_int) i
62
        (pp_print_parenthesized pp_expr) (inputs @ locals @ outputs)
63
    | MemoryPack (f, inst, i) ->
64
      fprintf fmt "MemoryPack_%a<%a>%a"
65
        pp_print_string f
66
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
67
           pp_print_string) inst
68
        (pp_print_option pp_print_int) i
69
    | ResetCleared f ->
70
      fprintf fmt "ResetCleared_%a" pp_print_string f
71
    | Initialization -> ()
72

  
73
  let pp_spec m =
74
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
75
      fun fmt e -> pp_expr m fmt e
76
    in
77
    let rec pp_spec fmt f =
78
      match f with
79
      | True -> pp_print_string fmt "true"
80
      | False -> pp_print_string fmt "false"
81
      | Equal (a, b) ->
82
        fprintf fmt "%a == %a" pp_expr a pp_expr b
83
      | And fs ->
84
        pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
85
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
86
      | Or fs ->
87
        pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
88
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
89
      | Imply (a, b) ->
90
        fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
91
      | Exists (xs, a) ->
92
        fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
93
          (pp_comma_list Printers.pp_var) xs pp_spec a
94
      | Forall (xs, a) ->
95
        fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
96
          (pp_comma_list Printers.pp_var) xs pp_spec a
97
      | Ternary (e, a, b) ->
98
        fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])"
99
          pp_expr e pp_spec a pp_spec b
100
      | Predicate p ->
101
        pp_predicate m fmt p
102
      | StateVarPack r ->
103
        fprintf fmt "StateVarPack<%a>" pp_reg r
104
      | ExistsMem (rc, tr) ->
105
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [rc; tr])
106
    in
107
    pp_spec
108

  
109
end
110

  
111
let pp_spec m =
112
  pp_print_list
113
    ~pp_open_box:pp_open_vbox0
114
    ~pp_prologue:pp_print_cut
115
    (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
116

  
117
let rec pp_instr m fmt i =
118
  let pp_val = pp_val m in
119
  let pp_branch = pp_branch m in
120
  begin match i.instr_desc with
44 121
    | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
45 122
    | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
46
    | MReset i           -> fprintf fmt "reset %s" i
123
    | MSetReset i        -> fprintf fmt "set_reset %s" i
124
    | MClearReset        -> fprintf fmt "clear_reset %s" m.mname.node_id
47 125
    | MNoReset i         -> fprintf fmt "noreset %s" i
48 126
    | MStep (il, i, vl)  ->
49
       fprintf fmt "%a = %s (%a)"
50
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) il
51
	 i
52
	 (Utils.fprintf_list ~sep:", " pp_val) vl
127
      fprintf fmt "%a := %s%a"
128
        (pp_comma_list pp_vdecl) il
129
        i
130
        (pp_print_parenthesized pp_val) vl
53 131
    | MBranch (g,hl)     ->
54
       fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
55
	 pp_val g
56
	 (Utils.fprintf_list ~sep:"@," pp_branch) hl
132
      fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}"
133
        pp_val g
134
        (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch) hl
57 135
    | MComment s -> pp_print_string fmt s
58 136
    | MSpec s -> pp_print_string fmt ("@" ^ s)
59
       
60
  in
137

  
138
  end;
61 139
  (* Annotation *)
62 140
  (* let _ = *)
63 141
  (*   match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
64 142
  (* in *)
65 143
  begin match i.lustre_eq with
66 144
  | None -> ()
67
  | Some eq -> fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
145
  | Some eq -> fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq
68 146
  end;
69
  fprintf fmt "@ --%@ %a" (PrintSpec.pp_spec m) i.instr_spec
147
  pp_spec m fmt i.instr_spec
70 148

  
71 149

  
72 150
and pp_branch m fmt (t, h) =
......
95 173
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
96 174

  
97 175
let pp_step m fmt s =
98
  let pp_list = pp_print_list ~pp_sep:pp_print_comma in
99
  fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
100
    (pp_list Printers.pp_var) s.step_inputs
101
    (pp_list Printers.pp_var) s.step_outputs
102
    (pp_list Printers.pp_var) s.step_locals
103
    (pp_list (fun fmt (_, c) -> pp_val m fmt c))
176
  fprintf fmt
177
    "@[<v>\
178
     inputs : %a@ \
179
     outputs: %a@ \
180
     locals : %a@ \
181
     checks : %a@ \
182
     instrs : @[%a@]@ \
183
     asserts : @[%a@]@]@ "
184
    (pp_comma_list Printers.pp_var) s.step_inputs
185
    (pp_comma_list Printers.pp_var) s.step_outputs
186
    (pp_comma_list Printers.pp_var) s.step_locals
187
    (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
104 188
    s.step_checks
105 189
    (pp_instrs m) s.step_instrs
106
    (pp_list (pp_val m)) s.step_asserts
107

  
190
    (pp_comma_list (pp_val m)) s.step_asserts
108 191

  
109 192
let pp_static_call fmt (node, args) =
110
 fprintf fmt "%s<%a>"
111
   (node_name node)
112
   (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
193
  fprintf fmt "%s<%a>"
194
    (node_name node)
195
    (pp_comma_list Dimension.pp_dimension) args
196

  
197
let pp_instance fmt (o1, o2) =
198
  fprintf fmt "(%s, %a)"
199
    o1
200
    pp_static_call o2
201

  
202
let pp_memory_pack m fmt mp =
203
  fprintf fmt
204
    "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]"
205
    pp_print_string mp.mpname.node_id
206
    (pp_print_option pp_print_int) mp.mpindex
207
    (PrintSpec.pp_spec m) mp.mpformula
208

  
209
let pp_memory_packs m fmt =
210
  fprintf fmt
211
    "@[<v 2>memory_packs:@ %a@]"
212
    (pp_print_list (pp_memory_pack m))
213

  
214
let pp_transition m fmt t =
215
  fprintf fmt
216
    "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]"
217
    pp_print_string t.tname.node_id
218
    (pp_print_option pp_print_int) t.tindex
219
    (pp_print_parenthesized pp_vdecl) (t.tinputs @ t.tlocals @ t.toutputs)
220
    (PrintSpec.pp_spec m) t.tformula
221

  
222
let pp_transitions m fmt =
223
  fprintf fmt
224
    "@[<v 2>transitions:@ %a@]"
225
    (pp_print_list (pp_transition m))
113 226

  
114 227
let pp_machine fmt m =
115 228
  fprintf fmt
......
120 233
     const    : %a@ \
121 234
     step     :@   \
122 235
     @[<v 2>%a@]@ \
123
     spec     : @[%t@]@ \
236
     spec     : @[<v>%t@ %a@ @ %a@]@ \
124 237
     annot    : @[%a@]@]@ "
125 238
    m.mname.node_id
126
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
127
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
128
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
129
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
239
    (pp_comma_list Printers.pp_var) m.mmemory
240
    (pp_comma_list pp_instance) m.minstances
241
    (pp_instrs m) m.minit
242
    (pp_instrs m) m.mconst
130 243
    (pp_step m) m.mstep
131 244
    (fun fmt -> match m.mspec.mnode_spec with
132 245
       | None -> ()
133 246
       | Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
134 247
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
135
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
248
    (pp_memory_packs m) m.mspec.mmemory_packs
249
    (pp_transitions m) m.mspec.mtransitions
250
    (pp_print_list Printers.pp_expr_annot) m.mannot
136 251

  
137
let pp_machines fmt ml =
138
  fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
252
let pp_machines =
253
  pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
139 254

  
140
  
141 255
let rec is_const_value v =
142 256
  match v.value_desc with
143 257
  | Cst _          -> true
......
169 283

  
170 284
let get_instr_spec i = i.instr_spec
171 285

  
286
let mk_val v t =
287
  { value_desc = v;
288
    value_type = t;
289
    value_annot = None }
290

  
291
let vdecl_to_val vd =
292
  mk_val (Var vd) vd.var_type
293

  
294
let vdecls_to_vals =
295
  List.map vdecl_to_val
296

  
297
let id_to_tag id =
298
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
299
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
300

  
172 301
let mk_conditional ?lustre_eq c t e =
173 302
  mkinstr ?lustre_eq
174 303
    (* (Ternary (Val c,
175 304
     *           And (List.map get_instr_spec t),
176 305
     *           And (List.map get_instr_spec e))) *)
177
    True
178 306
    (MBranch(c, [
179 307
         (tag_true, t);
180 308
         (tag_false, e) ]))
......
184 312
    (* (And (List.map (fun (l, instrs) ->
185 313
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
186 314
     *      br)) *)
187
    True
188
    (MBranch (c, br))
315
    (MBranch (vdecl_to_val c, br))
189 316

  
190 317
let mk_assign ?lustre_eq x v =
191 318
  mkinstr ?lustre_eq
192 319
    (* (Equal (Var x, Val v)) *)
193
    True
194 320
    (MLocalAssign (x, v))
195 321

  
196
let mk_val v t =
197
  { value_desc = v; 
198
    value_type = t; 
199
    value_annot = None }
200
    
201 322
let arrow_machine =
202 323
  let state = "_first" in
203 324
  let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
......
212 333
    mmemory = [var_state];
213 334
    mcalls = [];
214 335
    minstances = [];
215
    minit = [mkinstr True (MStateAssign(var_state, cst true))];
336
    minit = [mkinstr (MStateAssign(var_state, cst true))];
216 337
    mstatic = [];
217 338
    mconst = [];
218 339
    mstep = {
......
221 342
      step_locals = [];
222 343
      step_checks = [];
223 344
      step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
224
			(List.map (mkinstr True)
225
			[MStateAssign(var_state, cst false);
226
			 MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
227
                        (List.map (mkinstr True)
228
			[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
345
                       (List.map mkinstr
346
                          [MStateAssign(var_state, cst false);
347
                           MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
348
                       (List.map mkinstr
349
                          [MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
229 350
      step_asserts = [];
230 351
    };
231
    mspec = { mnode_spec = None; mtransitions = [] };
352
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
232 353
    mannot = [];
233 354
    msch = None
234 355
  }
......
269 390
      step_instrs = [];
270 391
      step_asserts = [];
271 392
    };
272
    mspec = { mnode_spec = None; mtransitions = [] };
393
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
273 394
    mannot = [];
274 395
    msch = None
275 396
  }
......
374 495
  | _                                             -> assert false
375 496

  
376 497

  
377
     let rec join_branches hl1 hl2 =
498
let rec join_branches hl1 hl2 =
378 499
 match hl1, hl2 with
379 500
 | []          , _            -> hl2
380 501
 | _           , []           -> hl1
......
384 505
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
385 506

  
386 507
and join_guards inst1 insts2 =
387
 match get_instr_desc inst1, List.map get_instr_desc insts2 with
388
 | _                   , []                               ->
389
   [inst1]
390
 | MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 ->
391
    mkinstr True
392
      (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
393
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
394
   :: (List.tl insts2)
395
 | _ -> inst1 :: insts2
508
 match get_instr_desc inst1, insts2 with
509
   | MBranch (x1, hl1),
510
     ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2
511
     when x1 = x2 ->
512
     mkinstr
513
       ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
514
       (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
515
       (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
516
     :: insts2
517
   | _ -> inst1 :: insts2
396 518

  
397 519
let join_guards_list insts =
398 520
 List.fold_right join_guards insts []

Also available in: Unified diff