From 727c890d3174ec313961dd1b7e1b8726125450e9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 15:33:13 +0100 Subject: begin adding loads --- backend/CSE2.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 14c6e042..e07e7adc 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -6,8 +6,9 @@ Require Import Memory Registers Op RTL Maps. Inductive sym_val : Type := | SMove (src : reg) -| SOp (op : operation) (args : list reg). - +| SOp (op : operation) (args : list reg) +| SLoad (chunk : memory_chunk) (addr : addressing) (args : list reg). + Definition eq_args (x y : list reg) : { x = y } + { x <> y } := list_eq_dec peq x y. @@ -17,6 +18,8 @@ Proof. generalize eq_operation. generalize eq_args. generalize peq. + generalize eq_addressing. + generalize chunk_eq. decide equality. Defined. @@ -250,6 +253,7 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) := match sv with | SMove src => if peq dst src then true else false | SOp op args => List.existsb (peq dst) args + | SLoad chunk addr args => List.existsb (peq dst) args end. Definition kill_reg (dst : reg) (rel : RELATION.t) := @@ -260,6 +264,7 @@ Definition kill_sym_val_mem (sv: sym_val) := match sv with | SMove _ => false | SOp op _ => op_depends_on_memory op + | SLoad _ _ _ => true end. Definition kill_mem (rel : RELATION.t) := -- cgit