Skip to content

Commit 61c3d76

Browse files
IngridJiangIngridJiang
committed
Add Z3-related fixes, scripts, logs, and experimental artifacts
1 parent 19cb9ce commit 61c3d76

40 files changed

Lines changed: 4435 additions & 126 deletions

‎.claude/settings.local.json‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
{
2+
"permissions": {
3+
"allow": [
4+
"Bash(bash:*)",
5+
"Bash(powershell -Command \"Test-Path ''C:\\\\Users\\\\10239\\\\Amathea-acset''\")",
6+
"Bash(where:*)",
7+
"Bash(cmd /c \"set \"\"PYTHON_CMD=\"\" && where python.exe >nul 2>&1 && set \"\"PYTHON_CMD=python.exe\"\" && echo !PYTHON_CMD!\")",
8+
"Bash(mvn clean install:*)",
9+
"Bash(mvn clean package:*)",
10+
"Bash(mvn package:*)",
11+
"Bash(mvn clean compile:*)",
12+
"Bash(dir:*)",
13+
"Bash(findstr:*)",
14+
"Bash(ls:*)",
15+
"Bash(./run-symbolic-execution.bat)",
16+
"Bash(./run-symbolic-execution.ps1)",
17+
"Bash(powershell -File run-symbolic-execution.ps1)",
18+
"Bash(java:*)",
19+
"Bash(cat:*)",
20+
"Bash(tee:*)",
21+
"Bash(mvn exec:java:*)",
22+
"Bash(run-with-instrumentation.bat:*)",
23+
"Bash(cmd /c run-with-instrumentation.bat)",
24+
"Bash(mvn process-test-resources:*)",
25+
"Bash(mvn dependency:build-classpath:*)",
26+
"Bash(./test-auto-mode.bat)",
27+
"Bash(./test-auto-with-regular-java.bat)",
28+
"Bash(xargs cat:*)",
29+
"Bash(./test-auto-fixed.bat)",
30+
"Bash(mvn test-compile:*)",
31+
"Bash(./compile-and-run-simple-test.bat)",
32+
"Bash(mvn compile:*)"
33+
]
34+
}
35+
}

‎knarr-runtime/apply-pure-auto-mode.bat‎

Lines changed: 283 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,283 @@
1+
@echo off
2+
setlocal enabledelayedexpansion
3+
4+
REM ================================================================================
5+
REM Apply Pure Auto Mode - Code Modification Script
6+
REM ================================================================================
7+
REM This script automatically modifies GaletteSymbolicator.java to enable
8+
REM pure auto-instrumentation mode (without manual PathUtils calls)
9+
REM
10+
REM ⚠️ ONLY run this AFTER verify-auto-instrumentation.bat shows VERIFICATION PASSED!
11+
REM ================================================================================
12+
13+
echo ================================================================================
14+
echo Apply Pure Auto-Instrumentation Mode
15+
echo ================================================================================
16+
echo.
17+
18+
REM Check if verification passed
19+
if not exist verification-status.txt (
20+
echo ERROR: verification-status.txt not found
21+
echo.
22+
echo You must run verify-auto-instrumentation.bat first!
23+
echo Only proceed if verification PASSED.
24+
echo.
25+
exit /b 1
26+
)
27+
28+
findstr /C:"VERIFICATION PASSED" verification-status.txt >nul 2>&1
29+
if errorlevel 1 (
30+
echo ❌ ERROR: Verification did NOT pass!
31+
echo.
32+
type verification-status.txt
33+
echo.
34+
echo You cannot proceed with code modification until verification passes.
35+
echo Please fix the issues and run verify-auto-instrumentation.bat again.
36+
echo.
37+
exit /b 1
38+
)
39+
40+
echo ✅ Verification passed. Safe to proceed with code modification.
41+
echo.
42+
43+
REM Confirm with user
44+
echo This script will modify GaletteSymbolicator.java to:
45+
echo - Add shouldUseManualConstraints() method
46+
echo - Wrap PathUtils calls with conditional checks
47+
echo - Enable pure auto-instrumentation mode
48+
echo.
49+
echo A backup will be created: GaletteSymbolicator.java.before-pure-auto
50+
echo.
51+
set /p "CONFIRM=Continue? (yes/no): "
52+
53+
if not "%CONFIRM%"=="yes" (
54+
echo Cancelled by user.
55+
exit /b 0
56+
)
57+
58+
echo.
59+
echo ================================================================================
60+
echo Starting code modification...
61+
echo ================================================================================
62+
echo.
63+
64+
set "JAVA_FILE=src\main\java\edu\neu\ccs\prl\galette\concolic\knarr\runtime\GaletteSymbolicator.java"
65+
66+
if not exist "%JAVA_FILE%" (
67+
echo ERROR: %JAVA_FILE% not found
68+
exit /b 1
69+
)
70+
71+
REM Step 1: Create backup
72+
echo [1/4] Creating backup...
73+
copy /y "%JAVA_FILE%" "%JAVA_FILE%.before-pure-auto" >nul 2>&1
74+
echo Backup created: %JAVA_FILE%.before-pure-auto
75+
echo.
76+
77+
REM Step 2: Create modified version using Python (if available) or manual instructions
78+
echo [2/4] Applying modifications...
79+
80+
REM Try to find Python
81+
set "PYTHON_CMD="
82+
where python.exe >nul 2>&1 && set "PYTHON_CMD=python.exe"
83+
if "%PYTHON_CMD%"=="" where python3 >nul 2>&1 && set "PYTHON_CMD=python3"
84+
if "%PYTHON_CMD%"=="" where python >nul 2>&1 && set "PYTHON_CMD=python"
85+
86+
if "%PYTHON_CMD%"=="" (
87+
echo Python not found. Will provide manual modification instructions.
88+
goto MANUAL_INSTRUCTIONS
89+
)
90+
91+
REM Create Python script to apply modifications
92+
echo import sys > apply_modifications.py
93+
echo import re >> apply_modifications.py
94+
echo. >> apply_modifications.py
95+
echo with open(sys.argv[1], 'r', encoding='utf-8') as f: >> apply_modifications.py
96+
echo content = f.read() >> apply_modifications.py
97+
echo. >> apply_modifications.py
98+
echo # Add the shouldUseManualConstraints method before makeSymbolicInt >> apply_modifications.py
99+
echo if 'shouldUseManualConstraints' not in content: >> apply_modifications.py
100+
echo method_code = ''' /** >> apply_modifications.py
101+
echo * Check if manual constraint collection should be used. >> apply_modifications.py
102+
echo * >> apply_modifications.py
103+
echo * Returns true in manual mode (when instrumentation is skipped). >> apply_modifications.py
104+
echo * Returns false in auto mode (when using javaagent instrumentation). >> apply_modifications.py
105+
echo * >> apply_modifications.py
106+
echo * @return true if manual PathUtils calls should be made >> apply_modifications.py
107+
echo */ >> apply_modifications.py
108+
echo private static boolean shouldUseManualConstraints() { >> apply_modifications.py
109+
echo boolean skipInstrumentation = Boolean.getBoolean("skip.instrumentation.check"); >> apply_modifications.py
110+
echo boolean manualMode = Boolean.getBoolean("manual.constraint.collection"); >> apply_modifications.py
111+
echo boolean useManual = skipInstrumentation ^|^| manualMode; >> apply_modifications.py
112+
echo if (DEBUG ^&^& useManual) { >> apply_modifications.py
113+
echo System.out.println("[GaletteSymbolicator] Using MANUAL constraint collection mode"); >> apply_modifications.py
114+
echo } else if (DEBUG) { >> apply_modifications.py
115+
echo System.out.println("[GaletteSymbolicator] Using AUTO constraint collection mode (bytecode instrumentation)"); >> apply_modifications.py
116+
echo } >> apply_modifications.py
117+
echo return useManual; >> apply_modifications.py
118+
echo } >> apply_modifications.py
119+
echo ''' >> apply_modifications.py
120+
echo # Insert before makeSymbolicInt method >> apply_modifications.py
121+
echo content = re.sub(r'( public static Tag makeSymbolicInt)', method_code + '\n\\1', content) >> apply_modifications.py
122+
echo. >> apply_modifications.py
123+
echo # Wrap first PathUtils calls (around line 174-175) >> apply_modifications.py
124+
echo content = re.sub( >> apply_modifications.py
125+
echo r'(\s+)PathUtils\.addIntDomainConstraint\(qualifiedName, min, max \+ 1\);\s*\n\s*PathUtils\.addSwitchConstraint\(qualifiedName, concreteValue\);', >> apply_modifications.py
126+
echo r'\1if (shouldUseManualConstraints()) {\n\1 PathUtils.addIntDomainConstraint(qualifiedName, min, max + 1);\n\1 PathUtils.addSwitchConstraint(qualifiedName, concreteValue);\n\1}', >> apply_modifications.py
127+
echo content, >> apply_modifications.py
128+
echo count=1 >> apply_modifications.py
129+
echo ) >> apply_modifications.py
130+
echo. >> apply_modifications.py
131+
echo # Wrap second PathUtils calls (around line 201-202) - in the else branch >> apply_modifications.py
132+
echo content = re.sub( >> apply_modifications.py
133+
echo r'( // Note: PathUtils\.addIntDomainConstraint uses exclusive upper bound\s*\n\s*)PathUtils\.addIntDomainConstraint\(qualifiedName, min, max \+ 1\);\s*\n\s*// Record switch constraint for the concrete value\s*\n\s*PathUtils\.addSwitchConstraint\(qualifiedName, concreteValue\);', >> apply_modifications.py
134+
echo r'\1if (shouldUseManualConstraints()) {\n\1 // Note: PathUtils.addIntDomainConstraint uses exclusive upper bound\n\1 PathUtils.addIntDomainConstraint(qualifiedName, min, max + 1);\n\n\1 // Record switch constraint for the concrete value\n\1 PathUtils.addSwitchConstraint(qualifiedName, concreteValue);\n\1}', >> apply_modifications.py
135+
echo content >> apply_modifications.py
136+
echo ) >> apply_modifications.py
137+
echo. >> apply_modifications.py
138+
echo with open(sys.argv[1], 'w', encoding='utf-8') as f: >> apply_modifications.py
139+
echo f.write(content) >> apply_modifications.py
140+
echo. >> apply_modifications.py
141+
echo print("Modifications applied successfully") >> apply_modifications.py
142+
143+
REM Apply modifications
144+
%PYTHON_CMD% apply_modifications.py "%JAVA_FILE%"
145+
146+
if errorlevel 1 (
147+
echo ERROR: Failed to apply modifications
148+
echo Restoring backup...
149+
copy /y "%JAVA_FILE%.before-pure-auto" "%JAVA_FILE%" >nul 2>&1
150+
del apply_modifications.py 2>nul
151+
exit /b 1
152+
)
153+
154+
del apply_modifications.py 2>nul
155+
echo Modifications applied successfully
156+
echo.
157+
158+
goto COMPILE_AND_TEST
159+
160+
:MANUAL_INSTRUCTIONS
161+
echo.
162+
echo ================================================================================
163+
echo Manual Modification Instructions
164+
echo ================================================================================
165+
echo.
166+
echo Python not found. Please apply modifications manually:
167+
echo.
168+
echo 1. Open: %JAVA_FILE%
169+
echo.
170+
echo 2. Add this method before 'makeSymbolicInt' method (around line 240):
171+
echo.
172+
type <<EOF
173+
/**
174+
* Check if manual constraint collection should be used.
175+
*/
176+
private static boolean shouldUseManualConstraints() {
177+
boolean skipInstrumentation = Boolean.getBoolean("skip.instrumentation.check");
178+
boolean manualMode = Boolean.getBoolean("manual.constraint.collection");
179+
boolean useManual = skipInstrumentation || manualMode;
180+
if (DEBUG && useManual) {
181+
System.out.println("[GaletteSymbolicator] Using MANUAL constraint collection mode");
182+
} else if (DEBUG) {
183+
System.out.println("[GaletteSymbolicator] Using AUTO constraint collection mode");
184+
}
185+
return useManual;
186+
}
187+
EOF
188+
echo.
189+
echo 3. Find line 174-175 and wrap PathUtils calls:
190+
echo Change:
191+
echo PathUtils.addIntDomainConstraint(qualifiedName, min, max + 1);
192+
echo PathUtils.addSwitchConstraint(qualifiedName, concreteValue);
193+
echo.
194+
echo To:
195+
echo if (shouldUseManualConstraints()) {
196+
echo PathUtils.addIntDomainConstraint(qualifiedName, min, max + 1);
197+
echo PathUtils.addSwitchConstraint(qualifiedName, concreteValue);
198+
echo }
199+
echo.
200+
echo 4. Find line 201-205 and wrap PathUtils calls:
201+
echo Change:
202+
echo PathUtils.addIntDomainConstraint(qualifiedName, min, max + 1);
203+
echo PathUtils.addSwitchConstraint(qualifiedName, concreteValue);
204+
echo.
205+
echo To:
206+
echo if (shouldUseManualConstraints()) {
207+
echo PathUtils.addIntDomainConstraint(qualifiedName, min, max + 1);
208+
echo PathUtils.addSwitchConstraint(qualifiedName, concreteValue);
209+
echo }
210+
echo.
211+
echo 5. Save the file and run this script again
212+
echo.
213+
pause
214+
exit /b 0
215+
216+
:COMPILE_AND_TEST
217+
218+
REM Step 3: Recompile
219+
echo [3/4] Recompiling...
220+
call mvn clean compile -pl knarr-runtime -DskipTests -Dcheckstyle.skip=true -q
221+
222+
if errorlevel 1 (
223+
echo ERROR: Compilation failed
224+
echo Restoring backup...
225+
copy /y "%JAVA_FILE%.before-pure-auto" "%JAVA_FILE%" >nul 2>&1
226+
exit /b 1
227+
)
228+
229+
echo Compilation successful
230+
echo.
231+
232+
REM Step 4: Verify modifications
233+
echo [4/4] Verifying modifications...
234+
235+
REM Check if method was added
236+
findstr /C:"shouldUseManualConstraints" "%JAVA_FILE%" >nul 2>&1
237+
if errorlevel 1 (
238+
echo WARNING: shouldUseManualConstraints method not found in file
239+
echo Please verify modifications manually
240+
) else (
241+
echo ✓ shouldUseManualConstraints method added
242+
)
243+
244+
REM Count conditional wrapping
245+
set "WRAP_COUNT=0"
246+
for /f %%a in ('findstr /C:"if (shouldUseManualConstraints())" "%JAVA_FILE%" ^| find /c "if"') do set "WRAP_COUNT=%%a"
247+
248+
if "%WRAP_COUNT%"=="2" (
249+
echo ✓ PathUtils calls wrapped correctly (2 locations)
250+
) else (
251+
echo WARNING: Expected 2 conditional wraps, found %WRAP_COUNT%
252+
echo Please verify modifications manually
253+
)
254+
255+
echo.
256+
echo ================================================================================
257+
echo Modification Complete!
258+
echo ================================================================================
259+
echo.
260+
echo Changes applied:
261+
echo ✓ Added shouldUseManualConstraints() method
262+
echo ✓ Wrapped PathUtils calls with conditional checks
263+
echo ✓ Code recompiled successfully
264+
echo.
265+
echo Backup saved: %JAVA_FILE%.before-pure-auto
266+
echo.
267+
echo Next steps:
268+
echo 1. Test MANUAL mode:
269+
echo run-symbolic-execution.bat
270+
echo Should see: "Using MANUAL constraint collection mode"
271+
echo.
272+
echo 2. Test AUTO mode:
273+
echo run-with-instrumentation.bat
274+
echo Should see: "Using AUTO constraint collection mode"
275+
echo.
276+
echo 3. Compare results (should be identical)
277+
echo.
278+
echo If there are any issues, restore backup:
279+
echo copy /y "%JAVA_FILE%.before-pure-auto" "%JAVA_FILE%"
280+
echo.
281+
echo ================================================================================
282+
283+
exit /b 0

‎knarr-runtime/compile-and-run-simple-test.bat‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
@echo off
2+
setlocal enabledelayedexpansion
3+
4+
set "INSTRUMENTED_JAVA=C:\Users\10239\galette-vitruv\knarr-runtime\target\galette\java\bin\java.exe"
5+
set "GALETTE_AGENT=C:\Users\10239\galette-vitruv\galette-agent\target\galette-agent-1.0.0-SNAPSHOT.jar"
6+
set "EMF_ECORE=C:\Users\10239\.m2\repository\org\eclipse\emf\org.eclipse.emf.ecore\2.38.0\org.eclipse.emf.ecore-2.38.0.jar"
7+
set "EMF_COMMON=C:\Users\10239\.m2\repository\org\eclipse\emf\org.eclipse.emf.common\2.40.0\org.eclipse.emf.common-2.40.0.jar"
8+
set "EMF_XMI=C:\Users\10239\.m2\repository\org\eclipse\emf\org.eclipse.emf.ecore.xmi\2.16.0\org.eclipse.emf.ecore.xmi-2.16.0.jar"
9+
10+
REM Read classpath
11+
set /p "MAVEN_CP="<cp-test.txt
12+
set "CP=target\classes;target\test-classes;%MAVEN_CP%"
13+
14+
echo ================================================================================
15+
echo Step 1: Compiling SimpleAutomaticTest...
16+
echo ================================================================================
17+
18+
javac -cp "%CP%" ^
19+
src\test\java\edu\neu\ccs\prl\galette\concolic\knarr\runtime\SimpleAutomaticTest.java ^
20+
-d target\test-classes
21+
22+
if errorlevel 1 (
23+
echo ERROR: Compilation failed
24+
exit /b 1
25+
)
26+
27+
echo Compilation successful!
28+
echo.
29+
30+
echo ================================================================================
31+
echo Step 2: Running with AUTOMATIC instrumentation...
32+
echo ================================================================================
33+
echo.
34+
35+
"%INSTRUMENTED_JAVA%" ^
36+
-cp "%CP%" ^
37+
-Xbootclasspath/a:"%GALETTE_AGENT%;%EMF_ECORE%;%EMF_COMMON%;%EMF_XMI%" ^
38+
-javaagent:"%GALETTE_AGENT%" ^
39+
-Dgalette.debug=false ^
40+
edu.neu.ccs.prl.galette.concolic.knarr.runtime.SimpleAutomaticTest
41+
42+
set "EXIT_CODE=%ERRORLEVEL%"
43+
44+
echo.
45+
echo ================================================================================
46+
echo Test completed with exit code: %EXIT_CODE%
47+
echo ================================================================================
48+
49+
if %EXIT_CODE%==0 (
50+
echo ✓ SUCCESS: Automatic constraint collection is working!
51+
) else (
52+
echo ✗ FAILURE: Automatic constraint collection not working.
53+
)
54+
55+
exit /b %EXIT_CODE%

‎knarr-runtime/copy-generated-reactions.sh‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,10 @@
1414

1515
set -e
1616

17-
# Default paths
18-
EXTERNAL_PATH="/home/anne/CocoPath/Amalthea-acset"
19-
INTERNAL_PATH="/home/anne/CocoPath/CocoPath/amalthea-acset-integration"
17+
# Default paths - Auto-detect relative to script
18+
SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
19+
EXTERNAL_PATH="$(cd "$SCRIPT_DIR/../.." && pwd)/Amathea-acset"
20+
INTERNAL_PATH="$(cd "$SCRIPT_DIR/.." && pwd)/amalthea-acset-integration"
2021

2122
# Parse arguments
2223
while [[ $# -gt 0 ]]; do

0 commit comments

Comments
 (0)