Skip to content

Commit 46e409d

Browse files
IngridJiangclaude
IngridJiang
and
claude
committed
Add Windows scripts and fixes for run-symbolic-execution-adapted
- Add CLAUDE.md with project architecture and build instructions - Add run-symbolic-execution-adapted.bat and .ps1 (Windows versions of adapted script) - Fix run-symbolic-execution-adapted.sh: set EXTERNAL_PATH to local Amathea-acset path - Fix run-symbolic-execution-adapted.sh: use OS-aware classpath separator (; on Windows, : on Linux) - Fix run-symbolic-execution-adapted.sh: add EXIT trap to show errors before terminal closes - Update execution_paths_automatic.json and execution_paths_multivar.json from local runs Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 838bca4 commit 46e409d

12 files changed

Lines changed: 935 additions & 70 deletions

‎CLAUDE.md‎

Lines changed: 150 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,150 @@
1+
# CLAUDE.md
2+
3+
This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
4+
5+
## Project Overview
6+
7+
**CoCoPath** is a concolic execution framework for systematically exploring execution paths in Vitruvius model transformations. It combines:
8+
- **Galette** – JVM dynamic taint tracking via ASM bytecode instrumentation
9+
- **Modified Knarr Runtime** – Symbolic execution and path constraint management
10+
- **Z3 / GREEN solver** – SMT constraint solving
11+
- **Vitruvius** – Eclipse-based model transformation framework (EMF/XMI)
12+
13+
## Prerequisites
14+
15+
- Java 17 (OpenJDK recommended; supports 8–21 at runtime)
16+
- Maven 3.6+
17+
- Python 3.x (for `switch-dependency.py`)
18+
- External dependency: clone and build [Amalthea-acset](https://github.com/IngridJiang/Amalthea-acset)
19+
20+
## Build Commands
21+
22+
```bash
23+
# 1. Build external dependency (one-time)
24+
git clone https://github.com/IngridJiang/Amalthea-acset.git
25+
cd Amalthea-acset && mvn clean install -DskipTests -Dcheckstyle.skip=true
26+
27+
# 2. Build CoCoPath
28+
mvn clean install -DskipTests -Dcheckstyle.skip=true
29+
30+
# 3. Generate instrumented Java VM (required for taint tracking; run from knarr-runtime/)
31+
cd knarr-runtime && mvn process-test-resources
32+
```
33+
34+
If the instrumented VM is missing or stale:
35+
```bash
36+
cd knarr-runtime && rm -rf target/galette/ && mvn clean process-test-resources
37+
```
38+
39+
If Maven cache is corrupted:
40+
```bash
41+
rm -rf ~/.m2/repository/edu/neu/ccs/prl/galette/
42+
rm -rf ~/.m2/repository/tools/vitruv/methodologisttemplate/
43+
mvn clean install -U -DskipTests
44+
```
45+
46+
## Running Path Exploration
47+
48+
All scripts run from `knarr-runtime/`:
49+
50+
```bash
51+
# Linux/macOS
52+
./run-symbolic-execution.sh # interactive
53+
./run-symbolic-execution.sh --internal # simplified stub (no Vitruvius)
54+
./run-symbolic-execution.sh --external # full Vitruvius transformations
55+
./run-symbolic-execution.sh --multivar # 25 paths (5×5 multi-variable)
56+
57+
# Windows CMD
58+
run-symbolic-execution.bat [internal|external|multivar]
59+
60+
# PowerShell
61+
.\run-symbolic-execution.ps1 [-Internal | -External | -MultiVar]
62+
```
63+
64+
## Running Tests
65+
66+
```bash
67+
mvn test # all modules
68+
mvn test -pl galette-agent # ASM instrumentation unit tests (13)
69+
mvn test -pl galette-integration-tests # integration tests (70+)
70+
mvn test -pl knarr-runtime # constraint solver tests
71+
```
72+
73+
## Architecture
74+
75+
### Four-Layer Stack
76+
77+
```
78+
Application Layer → amalthea-acset-integration/.../Test.java
79+
(Vitruvius model transformation, user decisions)
80+
Path Exploration → knarr-runtime/.../vitruvius/AutomaticVitruvPathExploration.java
81+
(single-variable) / AutomaticVitruvMultiVarPathExploration.java
82+
(multi-variable, Cartesian product of N symbolic vars)
83+
Constraint Management → knarr-runtime/.../runtime/PathExplorer.java
84+
PathUtils.java (manual constraint API)
85+
ConstraintSolver.java (GREEN/Z3 wrapper)
86+
Tag Propagation → galette-agent/ (ASM bytecode instrumentation)
87+
GaletteSymbolicator.java (symbolic value creation & tag reuse)
88+
```
89+
90+
### Key Source Files
91+
92+
| File | Role |
93+
|------|------|
94+
| `knarr-runtime/src/main/java/.../runtime/PathExplorer.java` | Core exploration loop: execute → collect constraints → negate → solve → repeat |
95+
| `knarr-runtime/src/main/java/.../runtime/PathUtils.java` | Manual API for domain constraints (`addIntDomainConstraint`) and path constraints (`addSwitchConstraint`) |
96+
| `knarr-runtime/src/main/java/.../runtime/GaletteSymbolicator.java` | Creates tagged symbolic integers; reuses tags via qualified names across iterations |
97+
| `knarr-runtime/src/main/java/.../runtime/Z3ConstraintSolver.java` | Direct Z3 JNI integration |
98+
| `knarr-runtime/src/main/java/.../runtime/ConstraintSolver.java` | GREEN solver wrapper |
99+
| `knarr-runtime/src/main/java/.../vitruvius/AutomaticVitruvMultiVarPathExploration.java` | Multi-variable exploration entry point |
100+
| `amalthea-acset-integration/vsum/src/main/java/.../Test.java` | Vitruvius transformation entry point; calls PathUtils to register constraints |
101+
| `galette-agent/src/main/java/.../GaletteAgent.java` | JVM instrumentation agent |
102+
103+
### Constraint Collection Pattern
104+
105+
Constraints are registered **manually** in Vitruvius reactions (automatic bytecode instrumentation is disabled due to JVM verification errors):
106+
107+
```java
108+
// Domain constraint (defines variable range)
109+
PathUtils.addIntDomainConstraint("user_choice", 0, 5);
110+
// → (0 <= user_choice) AND (user_choice < 5)
111+
112+
// Path constraint (records executed branch)
113+
PathUtils.addSwitchConstraint("user_choice", 0);
114+
// → user_choice == 0
115+
```
116+
117+
Tag reuse across exploration iterations is achieved via qualified names:
118+
```java
119+
GaletteSymbolicator.getOrMakeSymbolicInt("CreateAscetTaskRoutine:execute:userChoice")
120+
```
121+
122+
### Output Structure
123+
124+
```
125+
knarr-runtime/
126+
├── execution_paths_automatic.json # 5 paths: {pathId, inputs, constraints, executionTime}
127+
├── execution_paths_multivar.json # 25 paths
128+
├── galette-output-automatic-{0..4}/ # EMF model files per path
129+
│ ├── example.model # AMALTHEA source
130+
│ ├── example.model2 # ASCET target
131+
│ └── galette-test-output/vsum-output.xmi
132+
└── galette-output-multivar-{i}_{j}/
133+
```
134+
135+
### Modifying Consistency Preservation Rules
136+
137+
Reactions live in the external Amalthea-acset repository. After editing:
138+
```bash
139+
cd Amalthea-acset && mvn clean generate-sources
140+
cd /path/to/galette-vitruv/knarr-runtime
141+
./copy-generated-reactions.sh --external-path /path/to/Amalthea-acset
142+
cd ../amalthea-acset-integration && mvn clean compile -Dcheckstyle.skip=true
143+
```
144+
Generated Java is copied from `Amalthea-acset/consistency/target/generated-sources/reactions/mir/` to `amalthea-acset-integration/consistency/src/main/java/mir/`.
145+
146+
## Known Limitations
147+
148+
- Only integer symbolic variables are supported (no strings, booleans, arrays)
149+
- Automatic switch instrumentation from bytecode is disabled; constraints must be registered via `PathUtils` manually
150+
- No automatic inter-procedural constraint propagation

‎knarr-runtime/execution_paths_automatic.json‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==0"
1010
],
1111
"numConstraints": 2,
12-
"executionTimeMs": 21595
12+
"executionTimeMs": 58871
1313
},
1414
{
1515
"pathId": 2,
@@ -20,7 +20,7 @@
2020
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==1"
2121
],
2222
"numConstraints": 1,
23-
"executionTimeMs": 172
23+
"executionTimeMs": 412
2424
},
2525
{
2626
"pathId": 3,
@@ -31,7 +31,7 @@
3131
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==2"
3232
],
3333
"numConstraints": 1,
34-
"executionTimeMs": 133
34+
"executionTimeMs": 420
3535
},
3636
{
3737
"pathId": 4,
@@ -42,7 +42,7 @@
4242
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==3"
4343
],
4444
"numConstraints": 1,
45-
"executionTimeMs": 159
45+
"executionTimeMs": 454
4646
},
4747
{
4848
"pathId": 5,
@@ -53,6 +53,6 @@
5353
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==4"
5454
],
5555
"numConstraints": 1,
56-
"executionTimeMs": 63
56+
"executionTimeMs": 227
5757
}
5858
]

‎knarr-runtime/execution_paths_multivar.json‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -8,175 +8,175 @@
88
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
99
"constraints": ["(0<=CreateAscetTaskRoutine:execute:userChoice_forTask_task1)&&(CreateAscetTaskRoutine:execute:userChoice_forTask_task1<5)", "CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "(0<=CreateAscetTaskRoutine:execute:userChoice_forTask_task2)&&(CreateAscetTaskRoutine:execute:userChoice_forTask_task2<5)", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
1010
"num_constraints": 4,
11-
"execution_time_ms": 22352
11+
"execution_time_ms": 46105
1212
},
1313
{
1414
"path_id": 1,
1515
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
1616
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
1717
"num_constraints": 2,
18-
"execution_time_ms": 193
18+
"execution_time_ms": 388
1919
},
2020
{
2121
"path_id": 2,
2222
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
2323
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
2424
"num_constraints": 2,
25-
"execution_time_ms": 238
25+
"execution_time_ms": 394
2626
},
2727
{
2828
"path_id": 3,
2929
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
3030
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
3131
"num_constraints": 2,
32-
"execution_time_ms": 181
32+
"execution_time_ms": 369
3333
},
3434
{
3535
"path_id": 4,
3636
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
3737
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
3838
"num_constraints": 2,
39-
"execution_time_ms": 106
39+
"execution_time_ms": 220
4040
},
4141
{
4242
"path_id": 5,
4343
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
4444
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
4545
"num_constraints": 2,
46-
"execution_time_ms": 127
46+
"execution_time_ms": 358
4747
},
4848
{
4949
"path_id": 6,
5050
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
5151
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
5252
"num_constraints": 2,
53-
"execution_time_ms": 138
53+
"execution_time_ms": 248
5454
},
5555
{
5656
"path_id": 7,
5757
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
5858
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
5959
"num_constraints": 2,
60-
"execution_time_ms": 155
60+
"execution_time_ms": 465
6161
},
6262
{
6363
"path_id": 8,
6464
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
6565
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
6666
"num_constraints": 2,
67-
"execution_time_ms": 111
67+
"execution_time_ms": 302
6868
},
6969
{
7070
"path_id": 9,
7171
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
7272
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
7373
"num_constraints": 2,
74-
"execution_time_ms": 112
74+
"execution_time_ms": 362
7575
},
7676
{
7777
"path_id": 10,
7878
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
7979
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
8080
"num_constraints": 2,
81-
"execution_time_ms": 156
81+
"execution_time_ms": 332
8282
},
8383
{
8484
"path_id": 11,
8585
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
8686
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
8787
"num_constraints": 2,
88-
"execution_time_ms": 122
88+
"execution_time_ms": 293
8989
},
9090
{
9191
"path_id": 12,
9292
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
9393
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
9494
"num_constraints": 2,
95-
"execution_time_ms": 179
95+
"execution_time_ms": 230
9696
},
9797
{
9898
"path_id": 13,
9999
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
100100
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
101101
"num_constraints": 2,
102-
"execution_time_ms": 114
102+
"execution_time_ms": 249
103103
},
104104
{
105105
"path_id": 14,
106106
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
107107
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
108108
"num_constraints": 2,
109-
"execution_time_ms": 125
109+
"execution_time_ms": 237
110110
},
111111
{
112112
"path_id": 15,
113113
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
114114
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
115115
"num_constraints": 2,
116-
"execution_time_ms": 134
116+
"execution_time_ms": 441
117117
},
118118
{
119119
"path_id": 16,
120120
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
121121
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
122122
"num_constraints": 2,
123-
"execution_time_ms": 103
123+
"execution_time_ms": 421
124124
},
125125
{
126126
"path_id": 17,
127127
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
128128
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
129129
"num_constraints": 2,
130-
"execution_time_ms": 126
130+
"execution_time_ms": 461
131131
},
132132
{
133133
"path_id": 18,
134134
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
135135
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
136136
"num_constraints": 2,
137-
"execution_time_ms": 159
137+
"execution_time_ms": 451
138138
},
139139
{
140140
"path_id": 19,
141141
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
142142
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
143143
"num_constraints": 2,
144-
"execution_time_ms": 95
144+
"execution_time_ms": 269
145145
},
146146
{
147147
"path_id": 20,
148148
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
149149
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
150150
"num_constraints": 2,
151-
"execution_time_ms": 87
151+
"execution_time_ms": 180
152152
},
153153
{
154154
"path_id": 21,
155155
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
156156
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
157157
"num_constraints": 2,
158-
"execution_time_ms": 120
158+
"execution_time_ms": 199
159159
},
160160
{
161161
"path_id": 22,
162162
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
163163
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
164164
"num_constraints": 2,
165-
"execution_time_ms": 97
165+
"execution_time_ms": 281
166166
},
167167
{
168168
"path_id": 23,
169169
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
170170
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
171171
"num_constraints": 2,
172-
"execution_time_ms": 107
172+
"execution_time_ms": 265
173173
},
174174
{
175175
"path_id": 24,
176176
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
177177
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
178178
"num_constraints": 2,
179-
"execution_time_ms": 86
179+
"execution_time_ms": 485
180180
}
181181
]
182182
}

0 commit comments

Comments
 (0)