Project

General

Profile

« Previous | Next » 

Revision 0406ab94

Added by LĂ©lio Brun 7 months ago

implement optimization on spec: IT WORKS

View differences:

src/backends/C/c_backend_spec.ml
258 258

  
259 259
let pp_memory_pack' fmt = pp_memory_pack pp_print_string pp_print_string fmt
260 260

  
261
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
262
    (name, inputs, locals, outputs, mem_in, mem_out) =
261
let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
262
    (name, vars, mem_in, mem_out) =
263 263
  let stateless = fst (get_stateless_status m) in
264
  fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])" name
264
  fprintf fmt "%s_transition%a(@[<hov>%t%a%t@])" name
265 265
    (pp_print_option pp_print_int)
266 266
    i
267 267
    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)
268 268
    (pp_comma_list
269 269
       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())
270
       pp_input)
271
    inputs
272
    (pp_print_option (fun fmt _ ->
273
         pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
274
    i
270
       pp_var)
271
    vars
275 272
    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
276
    (pp_comma_list ~pp_prologue:pp_print_comma pp_output)
277
    outputs
278 273

  
279
let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
280
    (t, mem_in, mem_out) =
281
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
282
    (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
274
let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
275
  pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_var fmt
276
    (t.tname.node_id, t.tvars, mem_in, mem_out)
283 277

  
284 278
let pp_transition_aux' ?i m =
285
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
279
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl
286 280

  
287 281
let pp_transition_aux'' ?i m =
288
  pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
282
  pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
283
      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
289 284

  
290 285
let pp_transition' m =
291
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
292

  
293
let pp_transition'' m =
294
  pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
286
  pp_transition m pp_print_string pp_print_string pp_var_decl
295 287

  
296 288
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
297 289
  fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])" name pp_mem_in mem_in
......
329 321

  
330 322
  let pp_expr :
331 323
      type a.
332
      ?output:bool ->
324
      ?test_output:bool ->
333 325
      machine_t ->
334 326
      ident ->
335 327
      formatter ->
336 328
      (value_t, a) expression_t ->
337 329
      unit =
338
   fun ?(output = false) m mem fmt -> function
330
   fun ?(test_output = false) m mem fmt -> function
339 331
    | Val v ->
340
      pp_c_val m mem (pp_c_var_read ~test_output:output m) fmt v
332
      pp_c_val m mem (pp_c_var_read ~test_output m) fmt v
341 333
    | Tag t ->
342 334
      pp_print_string fmt t
343 335
    | Var v ->
......
346 338
      pp_reg mem fmt r
347 339

  
348 340
  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
349
    let output, mem_update =
341
    let test_output, mem_update =
350 342
      match mode with
351 343
      | InstrMode _ ->
352 344
        true, false
......
355 347
      | _ ->
356 348
        false, false
357 349
    in
358
    let pp_expr :
359
        type a. ?output:bool -> formatter -> (value_t, a) expression_t -> unit =
360
     fun ?output fmt e -> pp_expr ?output m mem_out fmt e
350
    let pp_expr : type a. bool -> formatter -> (value_t, a) expression_t -> unit
351
        =
352
     fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
361 353
    in
362 354
    match p with
363
    | Transition (f, inst, i, inputs, locals, outputs, r, mems, insts) ->
355
    | Transition (f, inst, i, vars, r, mems, insts) ->
364 356
      let pp_mem_in, pp_mem_out =
365 357
        match inst with
366 358
        | None ->
......
373 365
              else pp_access' fmt (mem_in, inst)),
374 366
            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )
375 367
      in
376
      pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr (pp_expr ~output) fmt
377
        (f, inputs, locals, outputs, mem_in', mem_out')
368
      pp_transition_aux ?i m pp_mem_in pp_mem_out (pp_expr test_output) fmt
369
        (f, vars, mem_in', mem_out')
378 370
    | Reset (_f, inst, r) ->
379 371
      pp_ite
380 372
        (pp_c_val m mem_in (pp_c_var_read m))
......
555 547
       (pp_transition m
556 548
          (pp_machine_decl' ~ghost:true)
557 549
          (pp_machine_decl' ~ghost:true)
558
          (pp_local m) (pp_local m))
550
          (pp_local m))
559 551
       (PrintSpec.pp_spec TransitionMode m))
560 552
    fmt
561 553
    ((t, (name, mem_in), (name, mem_out)), t.tformula)
......
593 585
  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
594 586
  let tr ?mems ?insts () =
595 587
    Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
596
      (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
597
      (vdecls_to_vals t.toutputs)
588
      (vdecls_to_vals t.tvars)
598 589
  in
599 590
  if not (mems_empty && insts_empty) then
600 591
    pp_acsl
......
610 601
      ( t,
611 602
        ( (m.mname.node_id, [ mem_in; mem_out ]),
612 603
          ( instances,
613
            ( memories,
614
              Forall
615
                ( t.tinputs @ t.tlocals @ t.toutputs,
616
                  Imply (tr (), tr ~mems ~insts ()) ) ) ) ) )
604
            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )
605
      )
617 606

  
618 607
let pp_transition_footprint_lemmas fmt m =
619 608
  pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
......
824 813
            (pp_requires pp_separated')
825 814
            outputs (pp_assigns pp_ptr_decl) outputs
826 815
            (pp_ensures (pp_transition_aux'' m))
827
            (name, inputs, [], outputs, "", "")
816
            (name, inputs @ outputs, "", "")
828 817
        else
829 818
          fprintf fmt
830 819
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
......
839 828
            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
840 829
            (name, mem, self)
841 830
            (pp_ensures
842
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr pp_var_decl
843
                  pp_ptr_decl))
844
            (name, inputs, [], outputs, mem, mem)
831
               (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
832
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
833
            (name, inputs @ outputs, mem, mem)
845 834
            (pp_assigns pp_ptr_decl) outputs
846 835
            (pp_assigns (pp_reg self))
847 836
            m.mmemory

Also available in: Unified diff