From 53b8128578dc9a14dd2def64196c578b79f1922b Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 5 Jul 2022 19:49:30 +0200
Subject: [PATCH] correct_sb: define cycle_on_more_advanced

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 src/correct_store_buffer.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index f49d3f6..993249c 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -65,6 +65,16 @@ Definition is_constrained (elt : instr_kind) trace sbState :=
   | _, _ => false
   end.
 
+Definition cycle_on_more_advanced (t : trace_kind) (instr : instr_kind) sbState :=
+  let (_, state) := instr in
+  let isSuUsed := List.existsb is_in_su t in
+  List.map (fun (elt : instr_kind) =>
+              let (_, state') := elt in
+              if state_leb state state' && negb (state_leb state' state) then
+                cycle_elt isSuUsed sbState t elt
+              else
+                elt) t.
+
 Section can_advance.
   Variable isSuUsed : bool.
   Variable sbState : sbStateT.
-- 
GitLab