Changed parsing of bytes based on the new recording (concreteStore, concreteMask, knownSymbolics) (6b499d04) · Commits · Marek Trtík / jetklee_progress_explorer

src/main/java/jetklee/CustomListCellRenderer.java

+3 −3

Original line number	Diff line number	Diff line
		@@ -5,13 +5,13 @@ import javax.swing.border.LineBorder;
		import java.awt.*;
		import java.util.List;

		import static jetklee.TreeViewer.GREEN_COLOR;
		import static jetklee.TreeViewer.RED_COLOR;

		public class CustomListCellRenderer extends DefaultListCellRenderer {
		private final List<NodeMemory.ObjectState> objects;
		private final List<NodeMemory.Deletion> deletions;

		private static final Color RED_COLOR = new Color(255, 0, 0, 125);
		private static final Color GREEN_COLOR = new Color(34, 139, 34, 125);

		public CustomListCellRenderer(List<NodeMemory.ObjectState> objects, List<NodeMemory.Deletion> deletions) {
		this.objects = objects;
		this.deletions = deletions;

src/main/java/jetklee/MemoryViewer.java

+153 −27

Original line number	Diff line number	Diff line
		package jetklee;

		import javax.swing.*;
		import javax.swing.border.EmptyBorder;
		import javax.swing.border.TitledBorder;
		import javax.swing.event.ListSelectionEvent;
		import javax.swing.event.ListSelectionListener;
		import javax.swing.text.BadLocationException;
		import javax.swing.text.StyledDocument;
		import javax.swing.text.SimpleAttributeSet;
		import javax.swing.text.StyleConstants;
		import java.awt.*;
		import java.awt.event.ActionEvent;
		import java.awt.event.ActionListener;
		@@ -15,6 +20,7 @@ import java.util.ArrayList;
		public class MemoryViewer extends JPanel implements ListSelectionListener {
		public JButton showAllButton;
		private NodeMemory.Memory currentMemory;
		private Node currentState;
		private boolean showAll = false;

		private JList<String> objectsList;
		@@ -34,21 +40,19 @@ public class MemoryViewer extends JPanel implements ListSelectionListener {
		showAllButton.addActionListener(new ActionListener() {
		@Override
		public void actionPerformed(ActionEvent e) {
		// assert currentState != null;
		//
		// showAll = !showAll;
		// if (showAll) {
		// showAllButton.setText("Hide");
		// displayCompleteMemory(currentState);
		// }
		// else {
		// showAllButton.setText("Show All");
		// displayShortMemory(currentState);
		// }
		showAll = !showAll;
		if (showAll) {
		showAllButton.setText("Hide");
		displayCompleteMemory(currentState);
		}
		else {
		showAllButton.setText("Show All");
		displayShortMemory(currentState);
		}
		}
		});

		// this.add(showAllButton, BorderLayout.NORTH);
		this.add(showAllButton, BorderLayout.NORTH);

		segmentPanel = new PlanePanel();
		segmentPanel.setBorder(new TitledBorder("Segment"));
		@@ -88,8 +92,8 @@ public class MemoryViewer extends JPanel implements ListSelectionListener {
		planesSplitPane.setResizeWeight(0.5);

		objectStateSplitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, planesSplitPane, objectInfoPanel);
		objectStateSplitPane.setDividerLocation(0.4);
		objectStateSplitPane.setResizeWeight(0.4);
		objectStateSplitPane.setDividerLocation(0.9);
		objectStateSplitPane.setResizeWeight(0.9);

		mainSplitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, objectsPanel, objectStateSplitPane);
		mainSplitPane.setDividerLocation(0.2);
		@@ -98,29 +102,21 @@ public class MemoryViewer extends JPanel implements ListSelectionListener {
		this.add(mainSplitPane, BorderLayout.CENTER);
		}


		public void displayMemory(NodeMemory.Memory memory) {
		private void displayTables(NodeMemory.Memory memory) {
		segmentPanel.updateTables(null);
		offsetPanel.updateTables(null);

		currentMemory = memory;

		// TODO vypisat, ze nebol najdeny JSON pre tento node (moze sa stat pri timeoute)dd
		if (currentMemory == null) {
		currentMemory = new NodeMemory.Memory(new ArrayList<>(), new ArrayList<>(), new ArrayList<>());
		}

		objects = new ArrayList<>();
		objects.addAll(currentMemory.additions());
		objects.addAll(currentMemory.changes());
		objects.addAll(memory.additions());
		objects.addAll(memory.changes());

		((CustomListCellRenderer) objectsList.getCellRenderer()).updateObjectList(objects, currentMemory.deletions());
		((CustomListCellRenderer) objectsList.getCellRenderer()).updateObjectList(objects, memory.deletions());
		((DefaultListModel<String>) objectsList.getModel()).clear();

		for (NodeMemory.ObjectState object : objects)
		((DefaultListModel<String>) objectsList.getModel()).addElement(String.valueOf(object.objID()));

		for (NodeMemory.Deletion deletion : currentMemory.deletions()) {
		for (NodeMemory.Deletion deletion : memory.deletions()) {
		((DefaultListModel<String>) objectsList.getModel()).addElement(String.valueOf(deletion.objID()));
		}

		@@ -132,6 +128,135 @@ public class MemoryViewer extends JPanel implements ListSelectionListener {
		updatePlanes();
		}

		private void appendKeyValue(StyledDocument doc, String key, String value) {
		SimpleAttributeSet keyStyle = new SimpleAttributeSet();
		StyleConstants.setForeground(keyStyle, Color.BLUE);
		StyleConstants.setBold(keyStyle, true);

		SimpleAttributeSet valueStyle = new SimpleAttributeSet();
		StyleConstants.setForeground(valueStyle, Color.BLACK);

		try {
		doc.insertString(doc.getLength(), key + ": ", keyStyle);
		doc.insertString(doc.getLength(), value + ", ", valueStyle);
		} catch (BadLocationException e) {
		// throw new RuntimeException(e);
		}
		}

		private void displayObjectInfo() {
		objectInfoPanel.removeAll();

		if (objectsList.getSelectedIndex() < 0) {
		return;
		}

		JTextPane textPane = new JTextPane();
		textPane.setEditable(false);
		textPane.setBorder(new EmptyBorder(10, 10, 10, 10));

		JScrollPane scrollPane = new JScrollPane(textPane);
		scrollPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED);
		scrollPane.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);

		objectInfoPanel.add(scrollPane, BorderLayout.CENTER);

		StyledDocument doc = textPane.getStyledDocument();

		int selected = Integer.parseInt(objectsList.getSelectedValue());

		boolean isDeletion = currentMemory.deletions().stream()
		.anyMatch(deletion -> deletion.objID() == selected);

		if (isDeletion) {
		handleDeletionClick(selected);
		return;
		}

		NodeMemory.ObjectState currentObjectState = objects.stream()
		.filter(obj -> obj.objID() == selected)
		.findFirst()
		.orElse(null);

		if (currentObjectState == null) {
		return;
		}

		appendKeyValue(doc, "ID", String.valueOf(currentObjectState.objID()));
		appendKeyValue(doc, "Segment", String.valueOf(currentObjectState.segment()));
		appendKeyValue(doc, "Name", currentObjectState.name());
		appendKeyValue(doc, "Size", currentObjectState.size());
		appendKeyValue(doc, "Local", String.valueOf(currentObjectState.isLocal()));
		appendKeyValue(doc, "Global", String.valueOf(currentObjectState.isGlobal()));
		appendKeyValue(doc, "Fixed", String.valueOf(currentObjectState.isFixed()));
		appendKeyValue(doc, "User Spec", String.valueOf(currentObjectState.isUserSpec()));
		appendKeyValue(doc, "Lazy", String.valueOf(currentObjectState.isLazy()));
		appendKeyValue(doc, "Symbolic Address", currentObjectState.symAddress());
		appendKeyValue(doc, "Copy-On-Write Owner", String.valueOf(currentObjectState.copyOnWriteOwner()));
		appendKeyValue(doc, "Read-Only", String.valueOf(currentObjectState.readOnly()));

		if (currentObjectState.segmentPlane() != null) {
		appendPlaneInfo(doc, "Segment Plane", currentObjectState.segmentPlane());
		}
		if (currentObjectState.offsetPlane() != null) {
		appendPlaneInfo(doc, "Offset Plane", currentObjectState.offsetPlane());
		}
		}

		private void appendPlaneInfo(StyledDocument doc, String planeType, NodeMemory.Plane plane) {
		assert plane != null;

		SimpleAttributeSet headerStyle = new SimpleAttributeSet();
		StyleConstants.setForeground(headerStyle, Color.BLUE);
		StyleConstants.setBold(headerStyle, true);
		try {
		doc.insertString(doc.getLength(), "\n\n" + planeType + ":\n", headerStyle);
		} catch (BadLocationException e) {
		// e.printStackTrace();
		}

		appendKeyValue(doc, "Root Object", plane.rootObject());
		appendKeyValue(doc, "Size Bound", String.valueOf(plane.sizeBound()));
		appendKeyValue(doc, "Initialized", String.valueOf(plane.initialized()));
		appendKeyValue(doc, "Symbolic", String.valueOf(plane.symbolic()));
		appendKeyValue(doc, "Initial Value", String.valueOf(plane.initialValue()));
		}

		private void getCompleteMemory(Node node, NodeMemory.Memory memory) {
		if (node == null) {
		return;
		}

		getCompleteMemory(node.getParent(), memory);
		}

		private void displayCompleteMemory(Node node) {
		NodeMemory.Memory m = new NodeMemory.Memory(new ArrayList<>(), new ArrayList<>(), new ArrayList<>());
		getCompleteMemory(node, m);
		displayTables(m);
		displayObjectInfo();
		}

		private void displayShortMemory(Node node) {
		displayTables(currentMemory);
		displayObjectInfo();
		}

		public void displayMemory(Node node) {
		currentState = node;
		currentMemory = node.getMemory().getMemory();

		if (currentMemory == null) {
		currentMemory = new NodeMemory.Memory(new ArrayList<>(), new ArrayList<>(), new ArrayList<>());
		}

		if (showAll) {
		displayCompleteMemory(node);
		} else {
		displayShortMemory(node);
		}
		}

		private void updatePlanes() {
		if (objectsList.getModel().getSize() == 0) {
		segmentPanel.updateTables(null);
		@@ -185,6 +310,7 @@ public class MemoryViewer extends JPanel implements ListSelectionListener {
		if (isDeletion) {
		handleDeletionClick(selectedID);
		} else {
		displayObjectInfo();
		updatePlanes();
		}
		}

src/main/java/jetklee/Node.java

+8 −10

Original line number	Diff line number	Diff line
		@@ -19,8 +19,8 @@ public class Node {
		private Node left;
		private Node right;
		private int id;
		private int memoryId;
		private NodeInfo info;
		private NodeMemory memory;
		/**
		* @param id_ unique node id
		*/
		@@ -66,10 +66,6 @@ public class Node {
		return id;
		}

		public int getMemoryId() {
		return memoryId;
		}

		public NodeInfo getInfo() {
		return info;
		}
		@@ -101,12 +97,14 @@ public class Node {
		public void setId(int id) {
		this.id = id;
		}

		public void setMemoryId(int memoryId) {
		this.memoryId = memoryId;
		}

		public void setInfo(NodeInfo info) {
		this.info = info;
		}

		public void setMemory(NodeMemory memory) {
		this.memory = memory;
		}
		public NodeMemory getMemory() {
		return memory;
		}
		}

src/main/java/jetklee/NodeMemory.java

+43 −46

Original line number	Diff line number	Diff line
		@@ -4,7 +4,8 @@ import org.json.JSONArray;
		import org.json.JSONObject;

		import java.util.ArrayList;
		import java.util.LinkedHashMap;
		import java.util.HashMap;
		import java.util.HashSet;

		/**
		* Parses and holds information about execution state of the process tree
		@@ -13,7 +14,7 @@ public class NodeMemory {
		// TODO presunut nondet values do context


		public record Diff<T>(ArrayList<T> additions, ArrayList<T> deletions) {
		public record Diff(ByteMap additions, ByteMap deletions) {
		}

		public enum OperationType {
		@@ -26,21 +27,16 @@ public class NodeMemory {
		int copyOnWriteOwner, boolean readOnly, Plane segmentPlane, Plane offsetPlane) {
		}

		public record ByteGroup(boolean concrete, boolean knownSym, boolean unflushed, String value,
		ArrayList<Integer> indices, boolean isAddition) {

		public static class ByteMap extends HashMap<String, ArrayList<Integer>> {
		}

		public record Plane(PlaneType type, int memoryObjectID, String rootObject, int sizeBound,
		boolean initialized, boolean symbolic, int initialValue,
		Diff<ByteGroup> bytes, Updates updates) {
		Diff concreteStore, Diff concreteMask, Diff knownSymbolics,
		Updates updates) {
		public enum PlaneType {
		SEGMENT, OFFSET;

		public boolean isSegment(PlaneType type) {
		return type == SEGMENT;
		}

		public static String toString(PlaneType type) {
		return switch (type) {
		case SEGMENT -> "segmentPlane";
		@@ -54,7 +50,7 @@ public class NodeMemory {
		ArrayList<Deletion> deletions) {
		}

		public class Updates extends LinkedHashMap<String, String> {
		public class Updates extends HashMap<String, String> {
		}

		public record Deletion(int objID, OperationType type) {
		@@ -127,41 +123,28 @@ public class NodeMemory {
		return objectStates;
		}

		private ArrayList<ByteGroup> parseByte(JSONArray bytesJSON, boolean isAddition) {
		ArrayList<ByteGroup> bytes = new ArrayList<>();
		private ByteMap parseByte(JSONArray bytesJSON, boolean isAddition) {
		ByteMap byteMap = new ByteMap();

		for (int i = 0; i < bytesJSON.length(); ++i) {
		JSONArray byteJSON = bytesJSON.getJSONArray(i);

		// skip first 3 elements (concrete, knownSym, unflushed) in byte array: [concrete, knownSym, unflushed, [value, index, index, ..., index]]
		for (int j = 3; j < byteJSON.length(); ++j) {
		JSONObject byteObject = bytesJSON.getJSONObject(i);
		String value = byteObject.keys().next(); // values of byte
		JSONArray indicesJSON = byteObject.getJSONArray(value); // indices for this value
		ArrayList<Integer> indices = new ArrayList<>();
		JSONArray indicesJSON = byteJSON.getJSONArray(j);

		// skip first element (value) in index array: [value, index, index, ..., index]
		for (int k = 1; k < indicesJSON.length(); ++k) {
		indices.add(indicesJSON.getInt(k));
		for (int j = 0; j < indicesJSON.length(); ++j) {
		indices.add(indicesJSON.getInt(j));
		}

		ByteGroup b = new ByteGroup(
		byteJSON.getInt(0) == 1, // concrete
		byteJSON.getInt(1) == 1, // knownSym
		byteJSON.getInt(2) == 1, // unflushed
		indicesJSON.getString(0), //value
		indices,
		isAddition
		);
		bytes.add(b);
		byteMap.put(value, indices);
		}
		}
		return bytes;
		return byteMap;
		}

		private Diff<ByteGroup> parseBytes(JSONObject bytes) {
		ArrayList<ByteGroup> additions = new ArrayList<>();
		ArrayList<ByteGroup> deletions = new ArrayList<>();
		private Diff parseBytes(JSONObject bytes) {
		ByteMap additions = new ByteMap();
		ByteMap deletions = new ByteMap();

		// TODO refactor to "additions, deletions" instead of "add, del"
		if (bytes.has("add")) {
		JSONArray additionsJSON = bytes.getJSONArray("add");
		additions = parseByte(additionsJSON, true);
		@@ -170,7 +153,7 @@ public class NodeMemory {
		JSONArray additionsJSON = bytes.getJSONArray("del");
		deletions = parseByte(additionsJSON, false);
		}
		return new Diff<>(additions, deletions);
		return new Diff(additions, deletions);
		}

		private Plane parsePlane(JSONObject data, Plane.PlaneType type) {
		@@ -178,11 +161,23 @@ public class NodeMemory {
		if (planeJSON.isEmpty()) return null;


		Diff<ByteGroup> bytes = new Diff<>(new ArrayList<>(), new ArrayList<>());
		Diff concreteStore = new Diff(new ByteMap(), new ByteMap());
		Diff concreteMask = new Diff(new ByteMap(), new ByteMap());
		Diff knownSymbolics = new Diff(new ByteMap(), new ByteMap());

		if (planeJSON.has("concreteStore")) {
		JSONObject bytesJSON = planeJSON.getJSONObject("concreteStore");
		concreteStore = parseBytes(bytesJSON);
		}

		if (planeJSON.has("concreteMask")) {
		JSONObject bytesJSON = planeJSON.getJSONObject("concreteMask");
		concreteMask = parseBytes(bytesJSON);
		}

		if (planeJSON.has("bytes")) {
		JSONObject bytesJSON = planeJSON.getJSONObject("bytes");
		bytes = parseBytes(bytesJSON);
		if (planeJSON.has("knownSymbolics")) {
		JSONObject bytesJSON = planeJSON.getJSONObject("knownSymbolics");
		knownSymbolics = parseBytes(bytesJSON);
		}

		Updates updates = new Updates();
		@@ -198,13 +193,15 @@ public class NodeMemory {

		return new Plane(
		type,
		planeJSON.getInt("memoryObjectID"),
		planeJSON.getInt("objID"),
		planeJSON.getString("rootObject"),
		planeJSON.getInt("sizeBound"),
		planeJSON.getInt("initialized") == 1,
		planeJSON.getInt("symbolic") == 1,
		planeJSON.getInt("initialValue"),
		bytes,
		concreteStore,
		concreteMask,
		knownSymbolics,
		updates
		);
		}

src/main/java/jetklee/PlanePanel.java

+57 −33

Original line number	Diff line number	Diff line
		@@ -3,6 +3,7 @@ package jetklee;
		import javax.swing.*;
		import javax.swing.table.TableCellRenderer;
		import java.awt.*;
		import java.lang.reflect.Array;
		import java.util.ArrayList;
		import java.util.Comparator;

		@@ -11,30 +12,37 @@ import static jetklee.TreeViewer.*;
		public class PlanePanel extends JPanel {
		private NodeMemory.Plane currentPlane;
		private JCheckBox sortByOffsetCheckBox;
		private JPanel bytePanel;
		private JPanel concretePanel;
		private JPanel symbolicPanel;
		private JPanel updatePanel;

		private final String[] byteColumns = {"offset", "value", "concrete", "knownSym", "unflushed"};
		private static final Color RED_COLOR = new Color(255, 0, 0, 100);
		private static final Color GREEN_COLOR = new Color(34, 139, 34, 100);
		private final String[] concreteColumns = {"index", "value", "isConcrete"};
		private final String[] symbolicColumns = {"index", "value", "isSymbolic"};

		public PlanePanel() {
		super(new BorderLayout());
		JTabbedPane offsetTabbedPane = new JTabbedPane(JTabbedPane.TOP);

		sortByOffsetCheckBox = new JCheckBox("Sort by Offset");
		sortByOffsetCheckBox.setSelected(false);
		sortByOffsetCheckBox.setSelected(true);
		sortByOffsetCheckBox.addActionListener(e -> updateTables(currentPlane));

		JPanel controlPanel = new JPanel(new BorderLayout());
		controlPanel.add(sortByOffsetCheckBox, BorderLayout.NORTH);

		bytePanel = new JPanel(new BorderLayout());
		concretePanel = new JPanel(new BorderLayout());
		symbolicPanel = new JPanel(new BorderLayout());

		updatePanel = new JPanel(new BorderLayout());

		offsetTabbedPane.addTab("Bytes", bytePanel);
		offsetTabbedPane.addTab("Updates", updatePanel);
		// Create a JSplitPane to display the concrete and symbolic panels side by side
		JSplitPane concreteSymbolicSplitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, concretePanel, symbolicPanel);
		concreteSymbolicSplitPane.setResizeWeight(0.5); // Divide space equally between panels

		// Create a vertical JSplitPane to display the control panel and the combined concrete/symbolic panel
		JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, controlPanel, concreteSymbolicSplitPane);

		JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, controlPanel, offsetTabbedPane);
		this.add(splitPane, BorderLayout.CENTER);
		}

		@@ -51,34 +59,17 @@ public class PlanePanel extends JPanel {
		panel.repaint();
		}

		private void updateBytesTable(NodeMemory.Plane plane) {
		assert plane != null;

		if (plane.bytes().additions().isEmpty() && plane.bytes().deletions().isEmpty()) {
		private void updateBytesTable(NodeMemory.ByteMap additions, NodeMemory.ByteMap deletions, JPanel bytePanel, String[] byteColumns, boolean isConcrete) {
		if (additions.isEmpty() && deletions.isEmpty()) {
		clearTable(bytePanel);
		return;
		}

		ArrayList<NodeMemory.ByteGroup> byteGroups = new ArrayList<>();
		byteGroups.addAll(plane.bytes().additions());
		byteGroups.addAll(plane.bytes().deletions());

		ArrayList<Object[]> byteEntries = new ArrayList<>();
		ArrayList<Color> rowColors = new ArrayList<>();

		for (NodeMemory.ByteGroup bg : byteGroups) {
		for (int index : bg.indices()) {
		Object[] byteData = new Object[byteColumns.length];
		byteData[0] = index;
		byteData[1] = bg.value();
		byteData[2] = bg.concrete();
		byteData[3] = bg.knownSym();
		byteData[4] = bg.unflushed();

		byteEntries.add(byteData);
		rowColors.add(bg.isAddition() ? GREEN_COLOR : RED_COLOR);
		}
		}
		createByteRows(byteEntries, rowColors, additions, GREEN_COLOR, byteColumns, currentPlane.concreteMask().additions(), isConcrete);
		createByteRows(byteEntries, rowColors, deletions, RED_COLOR, byteColumns, currentPlane.concreteMask().additions(), isConcrete);

		if (sortByOffsetCheckBox.isSelected()) {
		ArrayList<Integer> indices = new ArrayList<>();
		@@ -126,6 +117,27 @@ public class PlanePanel extends JPanel {
		bytePanel.repaint();
		}

		private void createByteRows(ArrayList<Object[]> byteEntries, ArrayList<Color> rowColors, NodeMemory.ByteMap deletions, Color redColor, String[] byteColumns, NodeMemory.ByteMap concreteMask, boolean isConcrete) {
		for (String key : deletions.keySet()) {
		ArrayList<Integer> indices = deletions.get(key);
		for (int index : indices) {
		Object[] byteData = new Object[byteColumns.length];
		byteData[0] = index;
		byteData[1] = key;
		String mask = findKeyForByteIndex(index, concreteMask);
		if (mask != null) {
		if (isConcrete) {
		byteData[2] = mask.equals("0") ? "false" : "true";
		} else {
		byteData[2] = mask.equals("0") ? "true" : "false";
		}
		}
		byteEntries.add(byteData);
		rowColors.add(redColor);
		}
		}
		}

		private boolean isNumeric(String str) {
		try {
		Integer.parseInt(str);
		@@ -162,8 +174,7 @@ public class PlanePanel extends JPanel {
		}

		if (sortByOffsetCheckBox.isSelected()) {
		numericUpdates.sort(Comparator.comparingInt(entry -> Integer.parseInt((String) entry[0]))
		);
		numericUpdates.sort(Comparator.comparingInt(entry -> Integer.parseInt((String) entry[0])));
		}

		updateEntries.addAll(numericUpdates);
		@@ -185,12 +196,25 @@ public class PlanePanel extends JPanel {
		public void updateTables(NodeMemory.Plane plane) {
		if (plane == null) {
		clearTable(updatePanel);
		clearTable(bytePanel);
		clearTable(concretePanel);
		clearTable(symbolicPanel);
		return;
		}

		this.currentPlane = plane;
		updateBytesTable(currentPlane);
		updateBytesTable(currentPlane.concreteStore().additions(), currentPlane.concreteStore().deletions(), concretePanel, concreteColumns, true);
		updateBytesTable(currentPlane.knownSymbolics().additions(), currentPlane.knownSymbolics().deletions(), symbolicPanel, symbolicColumns, false);
		updateUpdatesTable(currentPlane);
		}

		private String findKeyForByteIndex(int byteIndex, NodeMemory.ByteMap additions) {
		for (String key : additions.keySet()) {
		ArrayList<Integer> values = additions.get(key);

		if (values.contains(byteIndex)) {
		return key;
		}
		}
		return null;
		}
		}