Added table for bytes and updates in memory tab (7cabd3d6) · Commits · Marek Trtík / jetklee_progress_explorer

src/main/java/jetklee/CustomListCellRenderer.java

0 → 100644

+64 −0

Original line number	Diff line number	Diff line
		package jetklee;

		import javax.swing.*;
		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<ExecutionState.ObjectState> objects;

		public CustomListCellRenderer(List<ExecutionState.ObjectState> objects) {
		this.objects = objects;
		}

		@Override
		public Component getListCellRendererComponent(JList<?> list, Object value, int index, boolean isSelected, boolean cellHasFocus) {
		JLabel label = (JLabel) super.getListCellRendererComponent(list, value, index, isSelected, cellHasFocus);

		int objID = Integer.parseInt(value.toString());
		ExecutionState.ObjectState objectState = getObjectStateById(objID);

		if (objectState != null) {
		switch (objectState.type()) {
		case ADDITION:
		label.setBackground(GREEN_COLOR);
		break;
		case DELETION:
		label.setBackground(RED_COLOR);
		break;
		case CHANGE:
		label.setBackground(Color.ORANGE);
		break;
		default:
		label.setBackground(Color.WHITE);
		}
		}

		if (isSelected) {
		label.setBorder(new LineBorder(Color.BLACK, 2));
		} else {
		label.setBorder(null);
		}

		label.setOpaque(true);
		return label;
		}

		private ExecutionState.ObjectState getObjectStateById(int objID) {
		for (ExecutionState.ObjectState object : objects) {
		if (object.objID() == objID) {
		return object;
		}
		}
		return null;
		}

		public void updateObjectList(List<ExecutionState.ObjectState> newObjects) {
		this.objects.clear();
		this.objects.addAll(newObjects);
		}
		}
		No newline at end of file

src/main/java/jetklee/ExecutionState.java

+144 −218

Original line number	Diff line number	Diff line
		@@ -5,16 +5,11 @@ import org.json.JSONObject;

		import java.util.ArrayList;
		import java.util.LinkedHashMap;
		import java.util.Map;

		/**
		* Parses and holds information about execution state of the process tree
		*/
		public class ExecutionState {
		public static final int BYTES_INDENT = 12;
		public static final int OBJS_INDENT = 4;
		public int nodeID;

		public record Location(String file, int line, int column, int assemblyLine) {
		@Override
		public String toString() {
		@@ -62,191 +57,203 @@ public class ExecutionState {
		}
		}

		public record Diff<T>(ArrayList<T> additions, ArrayList<T> deletions, int indent) {
		@Override
		public String toString() {
		if (additions.isEmpty() && deletions.isEmpty()) return "";

		StringBuilder addStr = new StringBuilder();
		for (T addition : additions) {
		addStr.append(" ".repeat(indent + 4));
		addStr.append(addition.toString()).append("\n");
		}
		StringBuilder delStr = new StringBuilder();
		for (T deletion : deletions) {
		delStr.append(" ".repeat(indent + 4));
		delStr.append(deletion.toString()).append("\n");
		public record Diff<T>(ArrayList<T> additions, ArrayList<T> deletions) {
		}

		return String.format(
		" ".repeat(indent) + "add: \n%s" +
		" ".repeat(indent) + "del: \n%s ",
		addStr, delStr
		);
		}
		public enum OperationType {
		ADDITION, DELETION, CHANGE;
		}

		public record Object(int objID, int segment, String name, String size, boolean isLocal, boolean isGlobal,
		boolean isFixed, boolean isUserSpec, boolean isLazy, String symAddress) {
		@Override
		public String toString() {
		return String.format(
		"objID: %d, " +
		"segment: %d, " +
		"name: %s, " +
		"size: %s, " +
		"isLocal: %s, " +
		"isGlobal: %s, " +
		"isFixed: %s, " +
		"isUserSpec: %s, " +
		"isLazy: %s, " +
		"symAddress: %s",
		objID, segment, name, size, isLocal, isGlobal, isFixed, isUserSpec, isLazy, symAddress
		);
		}
		public record ObjectState(int objID, OperationType type, int segment, String name, String size, boolean isLocal,
		boolean isGlobal,
		boolean isFixed, boolean isUserSpec, boolean isLazy, String symAddress,
		int copyOnWriteOwner, boolean readOnly, Plane segmentPlane, Plane offsetPlane) {
		}

		public record ByteGroup (boolean concrete, boolean knownSym, boolean unflushed, String value, ArrayList<Integer> indices) {
		@Override
		public String toString() {
		return String.format(
		"concrete: %s, " +
		"knownSym: %s, " +
		"unflushed: %s, " +
		"value: %s, " +
		"indices: %s",
		concrete, knownSym, unflushed, value, indices.toString()
		);
		}
		public record ByteGroup(boolean concrete, boolean knownSym, boolean unflushed, String value,
		ArrayList<Integer> indices, boolean isAddition) {

		}

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

		public static String toString(Type type) {
		public boolean isSegment(PlaneType type) {
		return type == SEGMENT;
		}

		public static String toString(PlaneType type) {
		return switch (type) {
		case SEGMENT -> "segmentPlane";
		case OFFSET -> "offsetPlane";
		};
		}
		}

		@Override
		public String toString() {
		StringBuilder updatesStr = new StringBuilder();
		for (Map.Entry<Integer, String> update : updates.entrySet()) {
		updatesStr.append(update.getKey().toString());
		updatesStr.append(" : ");
		updatesStr.append(update.getValue());
		updatesStr.append("\n");
		}

		return String.format(
		"memoryObjectID: %d, " +
		"rootObject: %s, " +
		"sizeBound: %d, " +
		"initialized: %s, " +
		"symbolic: %s, " +
		"initialValue: %d, " +
		"\n bytes:\n%s" +
		"\n updates:\n%s",
		memoryObjectID, rootObject, sizeBound, initialized, symbolic, initialValue, bytes.toString(), updatesStr
		);
		}
		public record Memory(ArrayList<ObjectState> additions, ArrayList<ObjectState> changes,
		ArrayList<Deletion> deletions) {
		}

		public record ObjectState(int objID, int copyOnWriteOwner, boolean readOnly, Plane segmentPlane,
		Plane offsetPlane) {
		@Override
		public String toString() {
		return String.format(
		" objID: %d, " +
		"copyOnWriteOwner: %d, " +
		"readOnly: %s\n" +
		" segmentPlane: %s\n" +
		" offsetPlane: %s",
		objID, copyOnWriteOwner, readOnly, segmentPlane == null ? "" : segmentPlane.toString(),
		offsetPlane == null ? "" : offsetPlane.toString()
		);
		public class Updates extends LinkedHashMap<String, String> {
		}

		public record Deletion(int objID, OperationType type) {
		}

		public Context context;
		public ArrayList<String> constraints;
		public Diff<Object> objectsDiff;
		public ArrayList<ObjectState> objectStates;

		public Memory memory;
		public Node node;

		/**
		* @param data information about one execution state
		*/
		public ExecutionState(JSONObject data) {
		public ExecutionState(JSONObject data, Node node_) {
		context = parseContext(data);
		constraints = parseConstraints(data);
		objectsDiff = parseObjects(data);
		objectStates = parseObjectStates(data);
		memory = parseMemory(data);
		node = node_;
		}

		private Memory parseMemory(JSONObject data) {
		ArrayList<ObjectState> additions = new ArrayList<>();
		ArrayList<ObjectState> changes = new ArrayList<>();
		ArrayList<Deletion> deletions = new ArrayList<>();

		if (!data.has("objects")) return new Memory(additions, changes, deletions);

		JSONObject objectsJSON = data.getJSONObject("objects");
		if (objectsJSON.has("added")) {
		JSONArray additionsJSON = objectsJSON.getJSONArray("added");
		additions = parseObjectStates(additionsJSON, OperationType.ADDITION);
		}
		if (objectsJSON.has("changed")) {
		JSONArray changesJSON = objectsJSON.getJSONArray("changed");
		changes = parseObjectStates(changesJSON, OperationType.CHANGE);
		}
		if (objectsJSON.has("deleted")) {
		JSONArray deletionsJSON = objectsJSON.getJSONArray("deleted");
		for (int i = 0; i < deletionsJSON.length(); ++i) {
		deletions.add(new Deletion(deletionsJSON.getInt(i), OperationType.DELETION));
		}
		}

		return new Memory(additions, changes, deletions);
		}

		private ArrayList<ObjectState> parseObjectStates(JSONObject data) {
		objectStates = new ArrayList<>();
		if (!data.has("objectStates")) return objectStates;
		private ArrayList<ObjectState> parseObjectStates(JSONArray objectStatesJSON, OperationType type) {
		ArrayList<ObjectState> objectStates = new ArrayList<>();

		JSONArray objectStatesJSON = data.getJSONArray("objectStates");
		for (int i = 0; i < objectStatesJSON.length(); i++) {
		JSONObject objectStateJSON = objectStatesJSON.getJSONObject(i);

		ObjectState objectState = new ObjectState(
		objectStateJSON.getInt("objID"),
		type,
		objectStateJSON.getInt("segment"),
		objectStateJSON.getString("name"),
		objectStateJSON.getString("size"),
		objectStateJSON.getInt("isLocal") == 1,
		objectStateJSON.getInt("isGlobal") == 1,
		objectStateJSON.getInt("isFixed") == 1,
		objectStateJSON.getInt("isUserSpec") == 1,
		objectStateJSON.getInt("isLazy") == 1,
		objectStateJSON.getString("symAddress"),
		objectStateJSON.getInt("copyOnWriteOwner"),
		objectStateJSON.getInt("readOnly") == 1,
		parsePlane(objectStateJSON, Plane.Type.SEGMENT),
		parsePlane(objectStateJSON, Plane.Type.OFFSET)
		parsePlane(objectStateJSON, Plane.PlaneType.SEGMENT),
		parsePlane(objectStateJSON, Plane.PlaneType.OFFSET)
		);
		objectStates.add(objectState);
		}
		return objectStates;
		}

		private ArrayList<Object> parseObject(JSONArray objectsJSON) {
		ArrayList<Object> objects = new ArrayList<>();
		for (int i = 0; i < objectsJSON.length(); i++) {
		JSONObject objectJSON = objectsJSON.getJSONObject(i);
		Object object = new Object(
		objectJSON.getInt("objID"),
		objectJSON.getInt("segment"),
		objectJSON.getString("name"),
		objectJSON.getString("size"),
		objectJSON.getInt("isLocal") == 1,
		objectJSON.getInt("isGlobal") == 1,
		objectJSON.getInt("isFixed") == 1,
		objectJSON.getInt("isUserSpec") == 1,
		objectJSON.getInt("isLazy") == 1,
		objectJSON.getString("symAddress")
		private ArrayList<ByteGroup> parseByte(JSONArray bytesJSON, boolean isAddition) {
		ArrayList<ByteGroup> bytes = new ArrayList<>();

		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) {
		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));
		}

		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
		);
		objects.add(object);
		bytes.add(b);
		}
		return objects;
		}
		return bytes;
		}

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

		if (data.has("objects")) {
		JSONObject objectsJSON = data.getJSONObject("objects");
		if (objectsJSON.has("add")) {
		JSONArray additionsJSON = objectsJSON.getJSONArray("add");
		additions = parseObject(additionsJSON);
		// TODO refactor to "additions, deletions" instead of "add, del"
		if (bytes.has("add")) {
		JSONArray additionsJSON = bytes.getJSONArray("add");
		additions = parseByte(additionsJSON, true);
		}
		if (objectsJSON.has("del")) {
		JSONArray additionsJSON = objectsJSON.getJSONArray("del");
		deletions = parseObject(additionsJSON);
		if (bytes.has("del")) {
		JSONArray additionsJSON = bytes.getJSONArray("del");
		deletions = parseByte(additionsJSON, false);
		}
		return new Diff<>(additions, deletions);
		}

		return new Diff<>(additions, deletions, OBJS_INDENT);
		private Plane parsePlane(JSONObject data, Plane.PlaneType type) {
		JSONObject planeJSON = data.getJSONObject(Plane.PlaneType.toString(type));
		if (planeJSON.isEmpty()) return null;


		Diff<ByteGroup> bytes = new Diff<>(new ArrayList<>(), new ArrayList<>());

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

		Updates updates = new Updates();
		if (planeJSON.has("updates")) {
		JSONArray updatesJSON = planeJSON.getJSONArray("updates");
		for (int i = 0; i < updatesJSON.length(); ++i) {
		JSONObject updateJSON = updatesJSON.getJSONObject(i);
		String key = updateJSON.keys().next();
		String value = updateJSON.getString(key);
		updates.put(key, value);
		}
		}

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

		private Location getLocation(JSONObject data, String location) {
		@@ -260,7 +267,6 @@ public class ExecutionState {
		}

		private Context parseContext(JSONObject data) {
		nodeID = data.getInt("nodeID");
		Location location = getLocation(data, "location");
		Location nextLocation = getLocation(data, "nextLocation");

		@@ -305,84 +311,4 @@ public class ExecutionState {
		}
		return constraints;
		}

		private ArrayList<ByteGroup> parseByte(JSONArray bytesJSON) {
		ArrayList<ByteGroup> bytes = new ArrayList<>();
		for (int i = 0; i < bytesJSON.length(); i++) {
		JSONArray byteJSON = bytesJSON.getJSONArray(i);

		ArrayList<Integer> indices = new ArrayList<>();
		JSONArray indicesJSON = byteJSON.getJSONArray(3);

		// skip first element (value)
		for (int j = 1; 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
		byteJSON.getJSONArray(3).getString(0), //value
		indices
		);
		bytes.add(b);
		}
		return bytes;
		}

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

		if (bytes.has("add")) {
		JSONArray additionsJSON = bytes.getJSONArray("add");
		additions = parseByte(additionsJSON);
		}
		if (bytes.has("del")) {
		JSONArray additionsJSON = bytes.getJSONArray("del");
		deletions = parseByte(additionsJSON);
		}
		return new Diff<>(additions, deletions, BYTES_INDENT);
		}

		private Plane parsePlane(JSONObject data, Plane.Type type) {
		JSONObject planeJSON = data.getJSONObject(Plane.Type.toString(type));
		if (planeJSON.isEmpty()) return null;


		Diff<ByteGroup> bytes = new Diff<>(new ArrayList<>(), new ArrayList<>(), BYTES_INDENT);

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

		LinkedHashMap<Integer, String> updates = new LinkedHashMap<>();
		if (planeJSON.has("updates")) {
		JSONArray updatesJSON = planeJSON.getJSONArray("updates");
		for (int i = 0; i < updatesJSON.length(); ++i) {
		JSONObject updateJSON = updatesJSON.getJSONObject(i);
		String key = updateJSON.keys().next();
		String value = updateJSON.getString(key);
		updates.put(Integer.parseInt(key), value);
		}
		}

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

		public void getCompleteMemory() {

		}
		}

src/main/java/jetklee/MemoryViewer.java

+131 −24

File changed.

Preview size limit exceeded, changes collapsed.

src/main/java/jetklee/PlanePanel.java

0 → 100644

+124 −0

Original line number	Diff line number	Diff line
		package jetklee;

		import javax.swing.*;
		import javax.swing.table.TableCellRenderer;
		import java.awt.*;
		import java.util.ArrayList;
		import java.util.Map;

		import static jetklee.TreeViewer.*;

		public class PlanePanel extends JPanel {
		private JPanel bytePanel;
		private JPanel updatePanel;

		private final String[] byteColumns = {"offset", "value", "concrete", "knownSym", "unflushed"};

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

		bytePanel = new JPanel(new BorderLayout());
		// Object[][] byteData = {};
		// JTable byteTable = new JTable(byteData, byteColumns);
		// JScrollPane scrollPane = new JScrollPane(byteTable);
		// bytePanel.add(scrollPane);

		updatePanel = new JPanel(new BorderLayout());

		offsetTabbedPane.addTab("Bytes", bytePanel);
		offsetTabbedPane.addTab("Updates", updatePanel);
		this.add(offsetTabbedPane, BorderLayout.CENTER);
		}

		private void updateBytesTable(ExecutionState.Plane plane) {
		// TODO bytes in consecutive order and save if byte is added or deleted

		if (plane == null) {
		bytePanel.removeAll();
		bytePanel.revalidate();
		bytePanel.repaint();
		return;
		}

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

		int totalSize = 0;
		for (ExecutionState.ByteGroup bg : bytes) {
		totalSize += bg.indices().size();
		}

		Object[][] byteData = new Object[totalSize][byteColumns.length];
		Color[] rowColors = new Color[totalSize];

		int row = 0;
		for (ExecutionState.ByteGroup bg : bytes) {
		for (int index : bg.indices()) {
		byteData[row][0] = index;
		byteData[row][1] = bg.value();
		byteData[row][2] = bg.concrete();
		byteData[row][3] = bg.knownSym();
		byteData[row][4] = bg.unflushed();

		rowColors[row] = bg.isAddition() ? GREEN_COLOR : RED_COLOR;
		++row;
		}
		}

		JTable byteTable = new JTable(byteData, byteColumns) {

		@Override
		public Component prepareRenderer(TableCellRenderer renderer, int row, int column) {
		Component c = super.prepareRenderer(renderer, row, column);
		c.setBackground(rowColors[row]);
		return c;
		}
		};
		bytePanel.removeAll();
		bytePanel.add(new JScrollPane(byteTable));
		bytePanel.revalidate();
		bytePanel.repaint();
		}

		private void updateUpdatesTable(ExecutionState.Plane plane) {
		if (plane == null) {
		updatePanel.removeAll();
		updatePanel.revalidate();
		updatePanel.repaint();
		return;
		}

		Object[][] updateData = new Object[plane.updates().size()][2];
		Color[] rowColors = new Color[plane.updates().size()];

		int row = 0;
		for (Map.Entry<String, String> update : plane.updates().entrySet()) {
		updateData[row][0] = update.getKey();
		updateData[row][1] = update.getValue();

		rowColors[row] = GREEN_COLOR;
		++row;
		}

		JTable updateTable = new JTable(updateData, new String[]{"offset", "value"}) {

		@Override
		public Component prepareRenderer(TableCellRenderer renderer, int row, int column) {
		Component c = super.prepareRenderer(renderer, row, column);
		c.setBackground(rowColors[row]);
		return c;
		}
		};
		updatePanel.removeAll();
		updatePanel.add(new JScrollPane(updateTable));
		updatePanel.revalidate();
		updatePanel.repaint();
		}

		public void updateTables(ExecutionState.Plane plane) {
		updateBytesTable(plane);
		updateUpdatesTable(plane);
		}
		}

src/main/java/jetklee/ProgressExplorer.java

+10 −6

File changed.

Preview size limit exceeded, changes collapsed.