Skip to content

Latest commit

 

History

History
130 lines (93 loc) · 5.33 KB

UTILIZATION.md

File metadata and controls

130 lines (93 loc) · 5.33 KB

Utilize the API

1. Start and initialize the service

curl http://0.0.0.0:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification

Notice that 0.0.0.0 is used as the service is running in a Docker container.

2. Register a new verification request:

The JBMC request JSON format:
{
	"tool": "JBMC",
	"isJarFile" : true | false,
	"jarName" : "file.jar", # Name of the jar file that is uploaded
	"className": "package.ClassName", # Path of the class that contains the main
	"isMethod": true | false
	"methodName": "fully.qualified.name:(arg types)return type"
}
The ESBMC request JSON format:
{
	"tool": "ESBMC",
	"fileName": "relative/path/to/c-or-cpp-file"
	"isFunction": true | false
	"functionName:" "name"
}
Using the curl:
curl -X POST -H "Content-Type: multipart/form-data" -F "file=@/path/to/code/file" -F "request=@/path/to/request/json/file" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry
Examples:

The example code files are under examples/codes/. The example request files are under examples/requests/.

3. Verification request that uses JBMC:

3.1. Upload a class file (my/petty/examples/Simple.class) and verify the whole class with JBMC :

curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/java/my/petty/examples/Simple.class" -F "request=@examples/requests/jbmc/request-class.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

3.2. Upload a class file (my/petty/examples/Simple.class) and verify the void foo() method with JBMC:

curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/java/my/petty/examples/Simple.class" -F "request=@examples/requests/jbmc/request-method-1.json"  http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

3.3. Upload a class file (my/petty/examples/Simple.class) and verify the boolean foo(String) method with JBMC:

curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/java/my/petty/examples/Simple.class" -F "request=@examples/requests/jbmc/request-method-2.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

3.4. Upload a jar file (my/petty/examples/simple.jar) and verify the boolean foo(String) method from a class that is in a jar file with JBMC:

cd examples/codes/java
javac my/petty/examples/Simple.java
jar -cvf simple.jar my/petty/examples
cd ../../../
curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/java/simple.jar" -F "request=@examples/requests/jbmc/request-method-3.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

3.5. Upload a jar file (radioProfilerCluster.jar) and verify the whole class described in the request-class-radio-profiler.json with JBMC:

cd examples/codes/java/
export SERVICE_HOME=~/Elegant/Elegant-Code-Verification-Service
javac -classpath $SERVICE_HOME/nebulastream/nebulastream-java-client-0.0.83.jar stream/nebula/examples/radioProfilerCluster.java 
jar -cvf radioProfilerCluster.jar stream/nebula/examples
curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/java/radioProfilerCluster.jar" -F "request=@examples/requests/jbmc/request-class-radio-profiler-cluster.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

4. Verification request that uses ESBMC:

4.1. Verify the examples/codes/c/ex1.c with ESBMC:

curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/c/ex1.c" -F "request=@examples/requests/esbmc/request-1.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

4.2. Verify the examples/codes/c/ex2.c with ESBMC:

curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/c/ex2.c" -F "request=@examples/requests/esbmc/request-2.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

4.3. Verify the examples/codes/c/ex3.c with ESBMC:

curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/c/ex3.c" -F "request=@examples/requests/esbmc/request-3.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry

5. Get the verification outcome of an entry:

curl http://0.0.0.0:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/getEntry?entryId=<ID>

6. Remove an entry:

curl --request DELETE http://0.0.0.0:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/removeEntry?entryId=<ID>

7. List all known verification entries:

curl http://0.0.0.0:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/getEntries
Tested Use Cases:
  1. NES Example (examples/codes/cpp/NES-example.cpp):
curl -X POST -H "Content-Type: multipart/form-data" -F "file=@examples/codes/cpp/NES-example.cpp" -F "request=@examples/requests/esbmc/NES-request.json" http://localhost:8080/Elegant-Code-Verification-Service-1.0-SNAPSHOT/api/verification/newEntry