vericert.Compiler


Compiler Proof

This is the top-level module of the correctness proof and proves the final backwards simulation correct.

Imports

We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end.





Declarations

We then need to declare the external OCaml functions used to print out intermediate steps in the compilation, such as print_RTL, print_HTL and print_RTLBlock.

Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_HTL: Z -> HTL.program -> unit.
Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
Parameter print_RTLPar: Z -> RTLPar.program -> unit.
Parameter print_RTLParFU: Z -> RTLParFU.program -> unit.

Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
  let unused := printer prog in prog.

Lemma print_identity:
  forall (A: Type) (printer: A -> unit) (prog: A),
  print printer prog = prog.

We also declare some new notation, which is also used in CompCert to combine the monadic results of each pass.

Notation "a @@@ b" :=
   (Compiler.apply_partial _ _ a b) (at level 50, left associativity).
Notation "a @@ b" :=
  (Compiler.apply_total _ _ a b) (at level 50, left associativity).

As printing is used in the translation but does not change the output, we need to prove that it has no effect so that it can be removed during the proof.

Lemma compose_print_identity:
  forall (A: Type) (x: res A) (f: A -> unit),
  x @@ print f = x.

Finally, some optimisation passes are only activated by a flag, which is handled by the following functions for partial and total passes.

Definition total_if {A: Type}
          (flag: unit -> bool) (f: A -> A) (prog: A) : A :=
  if flag tt then f prog else prog.

Definition partial_if {A: Type}
          (flag: unit -> bool) (f: A -> res A) (prog: A) : res A :=
  if flag tt then f prog else OK prog.

Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.

Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop): A -> A -> Prop :=
  if flag tt then R else eq.

Lemma total_if_match:
  forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A),
  (forall p, rel p (f p)) ->
  match_if flag rel prog (total_if flag f prog).

Lemma partial_if_match:
  forall (A: Type) (flag: unit -> bool) (f: A -> res A) (rel: A -> A -> Prop) (prog tprog: A),
  (forall p tp, f p = OK tp -> rel p tp) ->
  partial_if flag f prog = OK tprog ->
  match_if flag rel prog tprog.

Remark forward_simulation_identity:
  forall sem, forward_simulation sem sem.

Lemma match_if_simulation:
  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (transf: A -> A -> Prop) (prog tprog: A),
  match_if flag transf prog tprog ->
  (forall p tp, transf p tp -> forward_simulation (sem p) (sem tp)) ->
  forward_simulation (sem prog) (sem tprog).

Top-level Translation

An optimised transformation function from RTL to Verilog can then be defined, which applies the front end compiler optimisations of CompCert to the RTL that is generated and then performs the two Vericert passes from RTL to HTL and then from HTL to Verilog.

Definition transf_backend (r : RTL.program) : res Verilog.program :=
  OK r
  @@@ Inlining.transf_program
   @@ print (print_RTL 1)
   @@ Renumber.transf_program
   @@ print (print_RTL 2)
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print (print_RTL 3)
   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
   @@ print (print_RTL 4)
  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
   @@ print (print_RTL 5)
  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
   @@ print (print_RTL 6)
  @@@ time "Unused globals" Unusedglob.transform_program
   @@ print (print_RTL 7)
  @@@ HTLgen.transl_program
   @@ print (print_HTL 0)

   @@ Veriloggen.transl_program.

The transformation functions from RTL to Verilog are then added to the backend of the CompCert transformations from Clight to RTL.

Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
  OK p
  @@@ SimplExpr.transl_program
  @@@ SimplLocals.transf_program
  @@@ Cshmgen.transl_program
  @@@ Cminorgen.transl_program
  @@@ Selection.sel_program
  @@@ RTLgen.transl_program
   @@ print (print_RTL 0)
  @@@ transf_backend.

Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
  OK p
  @@@ SimplExpr.transl_program
  @@@ SimplLocals.transf_program
  @@@ Cshmgen.transl_program
  @@@ Cminorgen.transl_program
  @@@ Selection.sel_program
  @@@ RTLgen.transl_program
  @@@ Inlining.transf_program
   @@ print (print_RTL 1)
   @@ Renumber.transf_program
   @@ print (print_RTL 2)
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print (print_RTL 3)
   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
   @@ print (print_RTL 4)
  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
   @@ print (print_RTL 5)
  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
   @@ print (print_RTL 6)
  @@@ time "Unused globals" Unusedglob.transform_program
   @@ print (print_RTL 7)
  @@@ RTLBlockgen.transl_program
   @@ print (print_RTLBlock 0)
   @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
   @@ print (print_RTLBlock 1)
  @@@ RTLPargen.transl_program
   @@ print (print_RTLPar 0)
  @@@ RTLParFUgen.transl_program
   @@ print (print_RTLParFU 0)
  @@@ HTLPargen.transl_program
   @@ print (print_HTL 0)
   @@ Veriloggen.transl_program.

Correctness Proof

Finally, the top-level definition for all the passes is defined, which combines the match_prog predicates of each translation pass from C until Verilog.


Definition CompCert's_passes :=
      mkpass SimplExprproof.match_prog
  ::: mkpass SimplLocalsproof.match_prog
  ::: mkpass Cshmgenproof.match_prog
  ::: mkpass Cminorgenproof.match_prog
  ::: mkpass Selectionproof.match_prog
  ::: mkpass RTLgenproof.match_prog
  ::: mkpass Inliningproof.match_prog
  ::: mkpass Renumberproof.match_prog
  ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
  ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
  ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
  ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
  ::: mkpass Unusedglobproof.match_prog
  ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program))
  
  ::: mkpass Veriloggenproof.match_prog
  ::: pass_nil _.

These passes are then composed into a larger, top-level match_prog predicate which matches a C program directly with a Verilog program.

Definition match_prog: Csyntax.program -> Verilog.program -> Prop :=
  pass_match (compose_passes CompCert's_passes).

We then need to prove that this predicate holds, assuming that the translation is performed using the transf_hls function declared above.

Theorem transf_hls_match:
  forall p tp,
    transf_hls p = OK tp ->
    match_prog p tp.

Theorem cstrategy_semantic_preservation:
  forall p tp,
  match_prog p tp ->
  forward_simulation (Cstrategy.semantics p) (Verilog.semantics tp)
  /\ backward_simulation (atomic (Cstrategy.semantics p)) (Verilog.semantics tp).

Backward Simulation

The following theorem is a *backward simulation* between the C and Verilog, which proves the semantics preservation of the translation. We can assume that the C and Verilog programs match, as we have proven previously in transf_hls_match that our translation implies that the match_prog predicate will hold.

Theorem c_semantic_preservation:
  forall p tp,
  match_prog p tp ->
  backward_simulation (Csem.semantics p) (Verilog.semantics tp).

We can then use transf_hls_match to prove the backward simulation where the assumption is that the translation is performed using the transf_hls function and that it succeeds.

Theorem transf_c_program_correct:
  forall p tp,
  transf_hls p = OK tp ->
  backward_simulation (Csem.semantics p) (Verilog.semantics tp).

The final theorem of the semantic preservation of the translation of separate translation units can also be proven correct, however, this is only because the translation fails if more than one translation unit is passed to Vericert at the moment.

Theorem separate_transf_c_program_correct:
  forall c_units verilog_units c_program,
  nlist_forall2 (fun cu tcu => transf_hls cu = OK tcu) c_units verilog_units ->
  link_list c_units = Some c_program ->
  exists verilog_program,
      link_list verilog_units = Some verilog_program
   /\ backward_simulation (Csem.semantics c_program) (Verilog.semantics verilog_program).