diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-03 17:34:02 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-03 17:34:02 +0200 |
commit | 863b65cc49fb49ad203694cac36e3cbd4f45dab7 (patch) | |
tree | 30a0eaafba7086be2e5eb3cab1038c7b705e11fc /backend/Duplicate.v | |
parent | 2bf7b92601fd6f33f93609c85a79192f821e6637 (diff) | |
download | compcert-kvx-863b65cc49fb49ad203694cac36e3cbd4f45dab7.tar.gz compcert-kvx-863b65cc49fb49ad203694cac36e3cbd4f45dab7.zip |
Stubs for Duplicate pass
Diffstat (limited to 'backend/Duplicate.v')
-rw-r--r-- | backend/Duplicate.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v new file mode 100644 index 00000000..cb52ec04 --- /dev/null +++ b/backend/Duplicate.v @@ -0,0 +1,31 @@ +(** RTL node duplication using external oracle. Used to form superblock + structures *) + +Require Import AST RTL Maps. +Require Import Coqlib Errors. + +Local Open Scope error_monad_scope. + +(** External oracle returning the new RTL function, along with a mapping + of new nodes to old nodes *) +Axiom duplicate_aux: RTL.function -> RTL.function * (PTree.t nat). + +Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". + +(** * Verification of node duplications *) + +(** Verifies that the mapping [mp] is giving correct information *) +Definition verify_mapping (f tf: function) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) + +(** * Entry points *) + +Definition transf_function (f: function) : res function := + let (tf, mp) := duplicate_aux f in + do u <- verify_mapping f tf mp; + OK tf. + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p.
\ No newline at end of file |