From bcfd6e010ad96b9552277be1ca29f9ceb170e194 Mon Sep 17 00:00:00 2001
From: xavier thirioux <xavier.thirioux@isae-supaero.fr>
Date: Wed, 22 Mar 2023 18:11:12 +0100
Subject: [PATCH] corrected again a regression bug in causality/scheduling: bad
handling of tuples
---
src/causality.ml | 1 +
src/causality.mli | 1 +
src/scheduling.ml | 5 ++++-
3 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/causality.ml b/src/causality.ml
index 30116cee..602019bf 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -118,6 +118,7 @@ module ExprDep = struct
let is_read_var v = v.[0] = '#'
let is_instance_var v = v.[0] = '!' || v.[0] = '?'
+ let is_call_instance_var v = v.[0] = '?'
let is_ghost_var v = is_instance_var v || is_read_var v
let undo_read_var id =
diff --git a/src/causality.mli b/src/causality.mli
index 08dab51e..22f04eed 100644
--- a/src/causality.mli
+++ b/src/causality.mli
@@ -40,6 +40,7 @@ module ExprDep : sig
val mk_return_instance_var : ident -> ident
val mk_read_var : ident -> ident
val is_instance_var : ident -> bool
+ val is_call_instance_var : ident -> bool
val is_ghost_var : ident -> bool
val is_read_var : ident -> bool
val undo_instance_var : ident -> ident
diff --git a/src/scheduling.ml b/src/scheduling.ml
index 509524f5..0850f947 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -30,7 +30,7 @@ open Scheduling_type
(* Checks whether the currently scheduled variable [choice] is an output of a
call, possibly among others *)
let is_call_output choice g =
- List.exists ExprDep.is_instance_var (IdentDepGraph.succ g choice)
+ List.exists ExprDep.is_call_instance_var (IdentDepGraph.succ g choice)
(* Adds successors of [v] in graph [g] in [pending] or [frontier] sets, wrt
[eq_equiv], then removes [v] from [g] *)
@@ -55,6 +55,7 @@ let next_element eq_equiv g sort call pending frontier =
pending := p;
frontier := f;
call := is_call_output choice g;
+ (*if !call then Format.eprintf "call var@."*)
add_successors eq_equiv g choice pending frontier;
if not (ExprDep.is_ghost_var choice) then sort := [ choice ] :: !sort)
else
@@ -62,6 +63,7 @@ let next_element eq_equiv g sort call pending frontier =
(*Format.eprintf "-2-> %s@." choice;*)
pending := ISet.remove choice !pending;
add_successors eq_equiv g choice pending frontier;
+ (*if !call then Format.eprintf "call var@."*)
if not (ExprDep.is_ghost_var choice) then
sort :=
if !call then (choice :: List.hd !sort) :: List.tl !sort
@@ -82,6 +84,7 @@ let topological_sort eq_equiv g =
next_element eq_equiv g sorted call pending frontier
done;
IdentDepGraph.clear g;
+ (*List.iter (fun l -> Format.eprintf "(%a) " (fun fmt -> List.iter (fun v -> Format.pp_print_string fmt v)) l) !sorted;*)
!sorted
(* XXX: UNUSED *)
--
GitLab