Require Import Coqlib Maps List Integers Errors.
Import ListNotations.
Require Import Compopts.
Require Import AST.
Require Import Op Registers RTL RTLpast.
Require Import CounterMeasures.

Expanding observe builtings into opaque copies.

Compile instructions

Section transf_instr.

  Fixpoint opaque_copies pc rs : seqinstr OneExit :=
    match rs with
    | [] => Seinstr Inop
    | r::rs =>
        let seq := opaque_copies pc rs in
        (Ssinstr (Iop (Ocopyimm (Int.repr (Zpos pc))) [r] r);;seq)
    end.

  Definition is_observe ef (des: builtin_res reg) :=
    match ef, des with
    | EF_observe _, BR_none => true
    | _, _ => false
    end.

  Definition transf_builtin (_ : node) ef args des (pc' : node) :=
    if is_observe ef des then
      if Compopts.opaque_copies tt then
        opaque_copies pc' (map_filter (fun a => match a with BA r => Some r | _ => None end) args)
      else Seinstr Inop
    else Seinstr (Ibuiltin ef args des).

End transf_instr.

Definition transf_function (f : function) :=
  let (code, entry) :=
    transf_function
      (Seinstr Inop)
      transf_nop_default transf_op_default
      transf_load_default transf_store_default
      transf_call_default transf_tailcall_default
      transf_builtin
      transf_cond_default
      transf_jumptable_default transf_return_default
      f in
  mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) code entry (fn_attr f).

Definition transf_fundef (fd: fundef) :=
  AST.transf_fundef transf_function fd.

Definition transf_program (p: program) :=
  AST.transform_program transf_fundef p.