-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathrun-dljc-infer.sh
executable file
·68 lines (52 loc) · 1.99 KB
/
run-dljc-infer.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
#!/bin/bash
set -e
WORKING_DIR=$(pwd)
JSR308=$(cd $(dirname "$0")/.. && pwd)
CFI=$JSR308/checker-framework-inference
VI=$JSR308/value-inference
VIPATH=$VI/build/classes/java/main:$VI/build/resources/main:$VI/build/libs/value-inference.jar
export AFU=$JSR308/annotation-tools/annotation-file-utilities
export PATH=$AFU/scripts:$PATH
export CLASSPATH=$VIPATH
export external_checker_classpath=$VIPATH
CFI_LIB=$CFI/lib
export DYLD_LIBRARY_PATH=$CFI_LIB
export LD_LIBRARY_PATH=$CFI_LIB
CHECKER=value.ValueChecker
SOLVER=value.solver.ValueSolverEngine
# DEBUG_SOLVER=checkers.inference.solver.DebugSolver
OPTIMIZINGMODE=$1
shift
SOLVERARGS="solver=Z3smt,optimizingMode=$OPTIMIZINGMODE,collectStatistics=true,writeSolutions=true,noAppend=false"
DLJC=$JSR308/do-like-javac
# Parsing build command of the target program
build_cmd=$1
shift
while [ "$#" -gt 0 ]
do
build_cmd="$build_cmd $1"
shift
done
# DLJC Inference
cd "$WORKING_DIR"
infer_cmd="python $DLJC/dljc -t inference --guess --crashExit \
--checker $CHECKER --solver $SOLVER --solverArgs=$SOLVERARGS \
-o logs -m ROUNDTRIP -afud $WORKING_DIR/annotated -- $build_cmd "
# debug_onlyCompile="--onlyCompileBytecodeBase true"
# TODO:see how ontology uses testminimizer
# debug_cmd="python $DLJC/dljc -t testminimizer --annotationClassPath $UIPATH \
# $debug_onlyCompile --expectOutputRegex 'Unsatisfiable' --checker $CHECKER \
# --solver $DEBUG_SOLVER --solverArgs=$SOLVERARGS \
# -o logs -m INFER -afud $WORKING_DIR/annotated -- $build_cmd "
debug_cmd="python $DLJC/dljc -t inference --guess --crashExit \
--checker $CHECKER --solver $DEBUG_SOLVER --solverArgs=$SOLVERARGS \
-o logs -m ROUNDTRIP -afud $WORKING_DIR/annotated -- $build_cmd "
running_cmd=$infer_cmd
echo "============ Important variables ============="
echo "JSR308: $JSR308"
echo "CLASSPATH: $CLASSPATH"
echo "build cmd: $build_cmd"
echo "infer cmd: $running_cmd"
echo "============================================="
eval "$running_cmd"
echo "---- Reminder: do not forget to clean up the project! ----"