Commit 3e953ef4 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

fix ci ?

parent 6bff68d5
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
open RTLpathCommon
let expanse (sb : superblock) code pm = (code, pm)
let find_last_node_reg c = ()
Require Import Coqlib Floats Values Memory.
Require Import Integers.
Require Import Op Registers.
Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
(** Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
None.
Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
None.
(* Main proof of simplification *)
Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
(H: target_op_simplify op lr hst = Some fsv)
(REF: hsilocal_refines ge sp rs0 m0 hst st)
(OK0: hsok_local ge sp rs0 m0 hst)
(OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
(OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
Proof.
unfold target_op_simplify; simpl.
intros H (LREF & SREF & SREG & SMEM) ? ? ?.
congruence.
Qed.
Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
(TARGET: target_cbranch_expanse hst c l = Some (c', l'))
(LREF : hsilocal_refines ge sp rs0 m0 hst st)
(OK: hsok_local ge sp rs0 m0 hst),
seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof.
unfold target_cbranch_expanse, seval_condition; simpl.
intros H (LREF & SREF & SREG & SMEM) ?.
congruence.
Qed.
Global Opaque target_op_simplify.
Global Opaque target_cbranch_expanse.
../aarch64/ExpansionOracle.ml
\ No newline at end of file
../aarch64/RTLpathSE_simplify.v
\ No newline at end of file
../aarch64/ExpansionOracle.ml
\ No newline at end of file
../aarch64/RTLpathSE_simplify.v
\ No newline at end of file
../aarch64/ExpansionOracle.ml
\ No newline at end of file
../aarch64/RTLpathSE_simplify.v
\ No newline at end of file
......@@ -10,7 +10,7 @@ open ExpansionOracle
let config = Machine.config
let print_superblock sb code =
let print_superblock (sb: superblock) code =
let insts = sb.instructions in
let li = sb.liveins in
let outs = sb.s_output_regs in
......
../aarch64/ExpansionOracle.ml
\ No newline at end of file
../aarch64/RTLpathSE_simplify.v
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment