From f83a2cf869e5baee07fae908567b124b64b99d85 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 2 Oct 2023 14:29:49 -0700 Subject: [PATCH] [PCover] Update symmetry depedency tracking --- .../java/psym/runtime/machine/Machine.java | 2 + .../explicit/ExplicitSymmetryTracker.java | 9 ++-- .../java/psym/valuesummary/NamedTupleVS.java | 54 +++++++++++-------- 3 files changed, 38 insertions(+), 27 deletions(-) diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java index 00d1eaecd..a95f649b4 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java @@ -25,6 +25,7 @@ public abstract class Machine implements Serializable, Comparable { @Getter private static final int mainMachineId = 2; protected static int globalMachineId = mainMachineId; + @Getter private static final Map nameToMachine = new HashMap<>(); public final Map< String, SerializableFunction< @@ -54,6 +55,7 @@ public Machine(String name, int id, State startState, State... states) { this.name = name; // this.instanceId = id; this.instanceId = globalMachineId++; + nameToMachine.put(toString(), this); this.startState = startState; this.sendBuffer = new EventQueue(this); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java index 9283018cc..0cf943c66 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java @@ -70,7 +70,8 @@ public void reset() { machineToParent = new HashMap<>(); } - public void addMachineSymData(Machine machine, String dataName, Object data) { + public void addMachineSymData(Machine machine, Object data) { + String dataName = data.getClass().toString(); Map machineSymmetricData = machineToSymData.get(machine); if (machineSymmetricData == null) { machineSymmetricData = new HashMap<>(); @@ -89,11 +90,11 @@ public void addMachineSymData(Machine machine, String dataName, Object data) { } } - public Object getMachineSymData(Machine machine, String dataName, Object curr) { - Object result = curr; + public Object getMachineSymData(Machine machine, Object curr) { + String dataName = curr.getClass().toString(); Map machineSymmetricData = machineToSymData.get(machine); if (machineSymmetricData != null) { - result = machineSymmetricData.get(dataName); + Object result = machineSymmetricData.get(dataName); if (result != null) { return result; } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/NamedTupleVS.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/NamedTupleVS.java index 403cdb5b4..56b50045c 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/NamedTupleVS.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/NamedTupleVS.java @@ -23,17 +23,21 @@ public class NamedTupleVS implements ValueSummary { private void storeSymmetricTuple() { if (PSymGlobal.getConfiguration().getSymmetryMode() == SymmetryMode.Full) { if (this.names.size() == 2 && !isEmptyVS()) { - if (this.names.get(0).equals("symMachine")) { + if (this.names.get(0).equals("symtag")) { if (PSymGlobal.getSymmetryTracker() instanceof ExplicitSymmetryTracker) { ExplicitSymmetryTracker symTracker = (ExplicitSymmetryTracker) PSymGlobal.getSymmetryTracker(); - List> machineGVs = ValueSummary.getGuardedValues(this.tuple.getField(0)); + + List> symtagGVs = ValueSummary.getGuardedValues(this.tuple.getField(0)); + assert (symtagGVs.size() == 1); List> dataGVs = ValueSummary.getGuardedValues(this.tuple.getField(1)); - assert (machineGVs.size() == 1); assert (dataGVs.size() == 1); - if (machineGVs.get(0).getValue() != null) { - assert (machineGVs.get(0).getValue() instanceof Machine); - symTracker.addMachineSymData( - (Machine) machineGVs.get(0).getValue(), this.names.get(1), dataGVs.get(0).getValue()); + + if (symtagGVs.get(0).getValue() != null) { + String symTag = symtagGVs.get(0).getValue().toString(); + Machine machineTag = Machine.getNameToMachine().get(symTag); + if (machineTag != null) { + symTracker.addMachineSymData(machineTag, dataGVs.get(0).getValue()); + } } } } @@ -89,27 +93,31 @@ public NamedTupleVS getCopy() { public NamedTupleVS swap(Map mapping) { if (this.names.size() == 2 && !isEmptyVS()) { - if (this.names.get(0).equals("symMachine")) { + if (this.names.get(0).equals("symtag")) { if (PSymGlobal.getSymmetryTracker() instanceof ExplicitSymmetryTracker) { ExplicitSymmetryTracker symTracker = (ExplicitSymmetryTracker) PSymGlobal.getSymmetryTracker(); - List> machineGVs = ValueSummary.getGuardedValues(this.tuple.getField(0)); + List> symtagGVs = ValueSummary.getGuardedValues(this.tuple.getField(0)); + assert (symtagGVs.size() == 1); List> dataGVs = ValueSummary.getGuardedValues(this.tuple.getField(1)); - assert (machineGVs.size() == 1); assert (dataGVs.size() == 1); - if (machineGVs.get(0).getValue() != null) { - assert (machineGVs.get(0).getValue() instanceof Machine); - - Machine origMachine = (Machine) machineGVs.get(0).getValue(); - Machine newMachine = mapping.get(origMachine); - if (newMachine != null) { - Object origValue = dataGVs.get(0).getValue(); - Object newValue = symTracker.getMachineSymData(newMachine, this.names.get(1), origValue); - Guard guard = machineGVs.get(0).getGuard(); - - return new NamedTupleVS( - new ArrayList<>(this.names), - new TupleVS(new PrimitiveVS<>(newMachine, guard), new PrimitiveVS<>(newValue, guard))); + + if (symtagGVs.get(0).getValue() != null) { + String symTag = symtagGVs.get(0).getValue().toString(); + Machine machineTag = Machine.getNameToMachine().get(symTag); + if (machineTag != null) { + Machine machineTagSwapped = mapping.get(machineTag); + if (machineTagSwapped != null) { + Object origValue = dataGVs.get(0).getValue(); + Object newValue = + symTracker.getMachineSymData(machineTagSwapped, origValue); + Guard guard = symtagGVs.get(0).getGuard(); + + return new NamedTupleVS( + new ArrayList<>(this.names), + new TupleVS( + new PrimitiveVS<>(machineTagSwapped.toString(), guard), new PrimitiveVS<>(newValue, guard))); + } } } return this;