Closed maxvonhippel closed 3 years ago
Might be an LLVM installation issue. Other parts are compiling properly but the C to SMT conversion is not happening as shown in the 2nd point of the example given in readme. Make sure by running opt command that you have clang-LLVM 7.0.0 properly installed in your system. You should also run our another subproject that we use to generate such LLVM passes like libTestPass.so
and convert C codes to SMTLIB2 expressions.
Thank you @SunandanAdhikary for your help! I updated my Dockerfile to use clang-LLVM 7:
# Set up the system
FROM ubuntu:20.04
ENV TZ=America/Cancun
RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
RUN apt-get update -y
RUN apt-get install -y --fix-missing git
RUN apt-get install -y --fix-missing clang-7 # use version 7.0.0
RUN apt-get install -y --fix-missing llvm-7 # use version 7.0.0
RUN rm -rf /var/lib/apt/lists/*
RUN apt-get update -y --fix-missing
RUN apt-get install -y --fix-missing libboost-all-dev
RUN apt-get install -y --fix-missing python-dev
RUN apt-get install -y --fix-missing python3-dev
RUN apt-get install -y --fix-missing pkg-config
RUN apt-get install -y --fix-missing build-essential
RUN apt-get install -y --fix-missing libglib2.0-dev
RUN apt-get install -y --fix-missing libjson-glib-dev
RUN apt-get install -y --fix-missing cmake
RUN apt-get install -y --fix-missing tree
RUN pkg-config --cflags json-glib-1.0
# Recompile libTestPass.so
RUN mkdir home/amit
RUN mkdir home/amit/MyData
WORKDIR home/amit/MyData
RUN git clone https://github.com/saverecs/CProgramToSMT.git 1ProjectFMSafe
WORKDIR 1ProjectFMSafe/llvm-pass-moduleTest
RUN mkdir build
WORKDIR build
RUN cmake -DCMAKE_C_FLAGS=-DLLVM_ENABLE_DUMP -DCMAKE_CXX_FLAGS=-DLLVM_ENABLE_DUMP ..
WORKDIR ..
RUN make clean build
RUN make
# Get SaverECS
WORKDIR /home
RUN git clone https://github.com/saverecs/SaverECS.git
WORKDIR SaverECS/src
RUN cp /home/amit/MyData/1ProjectFMSafe/llvm-pass-moduleTest/src/libTestPass.so lib/.
# Compile it
RUN chmod +x compile-cpp
RUN ./compile-cpp
RUN chmod +x ./bin/dReal
RUN chmod +x ../.././SaverECS/ODE_visualization/*.sh
It now appears to work! After building the image as saver
:
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo make run
sudo docker run --rm saver \
./SaVerECS -m 100 \
-t 0.2 \
-d 0.001 \
-u 10 \
-l 5 \
--time-horizon 3 \
--goal "x>=5 & y>=3" \
--plant-file "benchmarks/thermostat/thermostat.ha" \
--controller-file "benchmarks/thermostat/thermostat.c" \
-o test.smt2
**** Running tool SaVerECS (Safety Verification of Embedded Control Software) ... ****
[FV]: fileName = benchmarks/thermostat/thermostat.ha
Model File Selected for reading!!
HASLAC input model: parsing ...
--------------------AUTOMATON H1: Before Splitting ----------------------
--------------------AUTOMATON H1: Printed Successfully ------------------
--------------------Displaying user's input parameters ----------------------
Maximum bound value for variables = 100
Sampling Time = 0.2
Release Time = 0
Sampling Jitter = 0.001
Time horizon = 3
Precision = 0.001
Noise Data:
List of Noise/Disturbance Parameters:
Disturbance Data:
List of Noise/Disturbance Parameters:
Upper bound = 10
Lower bound = 5
deadline_miss : 0 out of 0
List of MinMaxBounds Parameters:
Plant file name = benchmarks/thermostat/thermostat.ha
Controller file name = benchmarks/thermostat/thermostat.c
Configuration file name =
Goal constraints(Infix):
x>=5
y>=3
Goal constraints(Prefix):
>= x 5
>= y 3
output file name = test.smt2
-------------Parameters Parsed Successfully -------------
Plant model: parsing Done...
List of Control Variables:
temperature [-100 , 100]
List of UnControl Variables:
u [-100 , 100]
===================Displaying Plant Model===================
Automaton name=thermostat
The variable to index mapping is:
Variable name = temperature Dimension index = 0
Variable name = u Dimension index = 1
List of Locations of the automata
loc_id=0 Loc Name=loc
Invariants:
Flow Equations:
Infix: temperature' == 0.5 * u - 0.5 * temperature
Prefix: (= d/dt[temperature] (-(* 0.5 u)(* 0.5 temperature)))
Transitions:
Assignment: it is kept empty now for controller-program 's output.
Initial Symbolic state(s):
Initial Loc-ID: 0
Initial Set (Infix):
u == 20
temperature <= 75
temperature >= 55
Initial Set (Prefix):
== u 20
<= temperature 75
>= temperature 55
sh: 1: clang: not found
sh: 1: opt: not found
sh: 1: opt: not found
Controller Program: parsing Done...
Controller Program:
Intermediate Variables:
Input Variables:
Real state_x2 [-100 , 100]
Real state_w [-100 , 100]
Output Variables:
Real next_u [-100 , 100]
SSA Statements:
(= next_u (- (* state_x2 2.34 ) (* state_w 0.468 ) ) )
File test.smt2_5.smt2 created .....
Running solver please wait ...
# Error: undeclared identifier x (triggered at /usr0/home/soonhok/work/dreal3/src/opensmt/egraph/EgraphStore.C, 573)
Boost/Wall clock time taken: (in Seconds) = 0.002
Safety violation detected in unrolling(bound): 5
Output file(test.smt2_5.smt2.json) generated. To view the trace of counter example, visualize data.json in ODE_Visualization folder.
Visualize counter example in localhost (Y/N)?Open localhost:8000. Once visualized, run ./shut_websvr.sh
Total Running Time (in seconds): 5
I do have one small issue, though: I can't seem to find the output file test.smt2_5.smt2.json
.
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver ls | grep test
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver tree | grep test.smt2_5.smt2
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver tree ../../../ | grep test.smt2_5.smt2
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver tree ../../../../ | grep test.smt2_5.smt2
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver tree ../../../../ | grep test.smt
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver tree ../../../../ | grep test.smt*
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver find ../../../. -name 'test.smt2_5.smt2.json'
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver find ../../../. -name 'test.*.json'
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver pwd
/home/SaverECS/src
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver ls | grep test
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$ sudo docker run --rm saver ls .. | grep test
(base) max@max-XPS-13-9310:~/projects/research/nds2/cps-fuzz/phys-fuzz/SaverECS$
When you have a chance, could you please help me with this? Thanks!
opt command is not found
written in the log but the SSA statements are generated while running the model. So guessing you have worked that out nicely. If not, try running the other subproject I referred to earlier. state_x
and state_w
whereas the plant .ha
file has temperature
as the state variable. So in controller code it should be state_temperature
. Refer to the benchmark..smt2
files should be generated. .json
files are generated in the same folder.Dear Max, I suggest you do an independent build of the project https://github.com/saverecs/CProgramToSMT. Follow the instruction mentioned in the project on "How to build" and "How to Run". Once these steps are successful you will be able to generate the "libTestPass.so" and so the main project SaverECS will be able to run the function generate_ssaFile() (https://github.com/saverecs/SaverECS/blob/master/src/coreSystem/controller_program/controller_parser.cpp) with no error. Now I still see that you have two errors "clang not found" and "opt not found".
Once again let me suggest you follow the step in https://github.com/saverecs/CProgramToSMT by making sure you have installed clang/LLVM version 7.0.0. Good Luck
Hi All, thank you for your help.
I have forked the CProgramToSMT repository, and I got it to compile successfully, using LLVM 7.0.0 and Clang 7.0.0. You can find my fork here, and if you'd like, you can reproduce my setup by cloning it, entering the fork, and then running make deps && bash setup_llvm.sh && make build
. And indeed, it seems to work. Here is an example, on the thermostat
benchmark.
(base) max@max-XPS-13-9310:~/projects/research/nds2/CProgramToSMT$ llvm/build/bin/clang -O1 -g -Xclang -emit-llvm -c llvm-pass-moduleTest/benchmarks/thermostat/thermostat.c -o llvm-pass-moduleTest/benchmarks/thermostat/thermostat.bc
(base) max@max-XPS-13-9310:~/projects/research/nds2/CProgramToSMT$ llvm/build/bin/opt -O1 -instnamer -mem2reg -simplifycfg -loops -lcssa -loop-simplify -loop-rotate -loop-unroll -unroll-count=3 -unroll-allow-partial -load llvm-pass-moduleTest/src/build/libTestPass.so -aa llvm-pass-moduleTest/benchmarks/thermostat/thermostat.bc -view-cfg -o llvm-pass-moduleTest/benchmarks/thermostat/thermostat
Function Name = controller
BasicBlock: entry
call void @llvm.dbg.value(metadata %struct.INPUT_VAL* %input, metadata !31, metadata !DIExpression()), !dbg !43
call void @llvm.dbg.value(metadata %struct.RETURN_VAL* %ret_val, metadata !32, metadata !DIExpression()), !dbg !44
call void @llvm.dbg.value(metadata i32 2, metadata !38, metadata !DIExpression()), !dbg !45
call void @llvm.dbg.value(metadata double 7.000000e+01, metadata !41, metadata !DIExpression()), !dbg !46
call void @llvm.dbg.value(metadata double 6.600000e+01, metadata !42, metadata !DIExpression()), !dbg !47
%temperature = getelementptr inbounds %struct.INPUT_VAL, %struct.INPUT_VAL* %input, i64 0, i32 0, !dbg !48
%0 = load double, double* %temperature, align 8, !dbg !48, !tbaa !49
call void @llvm.dbg.value(metadata double %0, metadata !40, metadata !DIExpression()), !dbg !55
%chat_detect = getelementptr inbounds %struct.INPUT_VAL, %struct.INPUT_VAL* %input, i64 0, i32 1, !dbg !56
%1 = load i32, i32* %chat_detect, align 8, !dbg !56, !tbaa !57
call void @llvm.dbg.value(metadata i32 %1, metadata !33, metadata !DIExpression()), !dbg !58
%previous_cmd_to_heater = getelementptr inbounds %struct.INPUT_VAL, %struct.INPUT_VAL* %input, i64 0, i32 2, !dbg !59
%2 = load i32, i32* %previous_cmd_to_heater, align 4, !dbg !59, !tbaa !60
call void @llvm.dbg.value(metadata i32 %2, metadata !34, metadata !DIExpression()), !dbg !61
%on_count = getelementptr inbounds %struct.INPUT_VAL, %struct.INPUT_VAL* %input, i64 0, i32 3, !dbg !62
%3 = load i32, i32* %on_count, align 8, !dbg !62, !tbaa !63
call void @llvm.dbg.value(metadata i32 %3, metadata !35, metadata !DIExpression()), !dbg !64
%off_count = getelementptr inbounds %struct.INPUT_VAL, %struct.INPUT_VAL* %input, i64 0, i32 4, !dbg !65
%4 = load i32, i32* %off_count, align 4, !dbg !65, !tbaa !66
call void @llvm.dbg.value(metadata i32 %4, metadata !36, metadata !DIExpression()), !dbg !67
%cmd_to_heater = getelementptr inbounds %struct.INPUT_VAL, %struct.INPUT_VAL* %input, i64 0, i32 5, !dbg !68
call void @llvm.dbg.value(metadata i32* %cmd_to_heater, metadata !37, metadata !DIExpression(DW_OP_deref)), !dbg !69
%cmp = fcmp oge double %0, 6.600000e+01, !dbg !70
%cmp1 = fcmp olt double %0, 7.000000e+01, !dbg !72
%or.cond81 = and i1 %cmp, %cmp1, !dbg !73
br i1 %or.cond81, label %if.end9, label %if.else, !dbg !73
BasicBlock: if.else
%cmp2 = fcmp ult double %0, 7.000000e+01, !dbg !74
br i1 %cmp2, label %if.else4, label %if.end9, !dbg !76
BasicBlock: if.else4
%cmp5 = fcmp olt double %0, 6.600000e+01, !dbg !77
%. = select i1 %cmp5, i32 1, i32 %2, !dbg !79
br label %if.end9, !dbg !79
BasicBlock: if.end9
%command_to_heater.0 = phi i32 [ 2, %entry ], [ 0, %if.else ], [ %., %if.else4 ], !dbg !80
call void @llvm.dbg.value(metadata i32 %command_to_heater.0, metadata !37, metadata !DIExpression()), !dbg !69
%cmp10 = icmp sgt i32 %4, 4, !dbg !81
%cmp11 = icmp sgt i32 %3, 4, !dbg !83
%or.cond = or i1 %cmp11, %cmp10, !dbg !84
%spec.select = select i1 %or.cond, i32 0, i32 %1, !dbg !84
call void @llvm.dbg.value(metadata i32 %spec.select, metadata !33, metadata !DIExpression()), !dbg !58
%cmp14 = icmp ne i32 %command_to_heater.0, %2, !dbg !85
call void @llvm.dbg.value(metadata i32 %spec.select, metadata !33, metadata !DIExpression(DW_OP_plus_uconst, 1, DW_OP_stack_value)), !dbg !58
%inc = zext i1 %cmp14 to i32, !dbg !87
%chatter_detect.1 = add nsw i32 %spec.select, %inc, !dbg !87
call void @llvm.dbg.value(metadata i32 %chatter_detect.1, metadata !33, metadata !DIExpression()), !dbg !58
%cmp17 = icmp sgt i32 %chatter_detect.1, 2, !dbg !88
%spec.select82 = select i1 %cmp17, i32 %2, i32 %command_to_heater.0, !dbg !90
call void @llvm.dbg.value(metadata i32 %spec.select82, metadata !37, metadata !DIExpression()), !dbg !69
%cmp20 = icmp eq i32 %spec.select82, 0, !dbg !91
call void @llvm.dbg.value(metadata i32 0, metadata !35, metadata !DIExpression()), !dbg !64
%inc22 = add nsw i32 %4, 1, !dbg !93
call void @llvm.dbg.value(metadata i32 %inc22, metadata !36, metadata !DIExpression()), !dbg !67
%inc24 = add nsw i32 %3, 1, !dbg !95
call void @llvm.dbg.value(metadata i32 %inc24, metadata !35, metadata !DIExpression()), !dbg !64
call void @llvm.dbg.value(metadata i32 0, metadata !36, metadata !DIExpression()), !dbg !67
%off_counter.0 = select i1 %cmp20, i32 %inc22, i32 0, !dbg !97
%on_counter.0 = select i1 %cmp20, i32 0, i32 %inc24, !dbg !97
call void @llvm.dbg.value(metadata i32 %on_counter.0, metadata !35, metadata !DIExpression()), !dbg !64
call void @llvm.dbg.value(metadata i32 %off_counter.0, metadata !36, metadata !DIExpression()), !dbg !67
%cond = icmp eq i32 %spec.select82, 2, !dbg !98
%spec.select83 = select i1 %cond, double 7.000000e+01, double 1.000000e+02, !dbg !98
%uVal.0 = select i1 %cmp20, double 2.000000e+01, double %spec.select83, !dbg !100
call void @llvm.dbg.value(metadata double %uVal.0, metadata !39, metadata !DIExpression()), !dbg !101
%u = getelementptr inbounds %struct.RETURN_VAL, %struct.RETURN_VAL* %ret_val, i64 0, i32 0, !dbg !102
store double %uVal.0, double* %u, align 8, !dbg !103, !tbaa !104
store i32 %spec.select82, i32* %cmd_to_heater, align 8, !dbg !106, !tbaa !107
store i32 %chatter_detect.1, i32* %chat_detect, align 8, !dbg !108, !tbaa !57
store i32 %spec.select82, i32* %previous_cmd_to_heater, align 4, !dbg !109, !tbaa !60
store i32 %on_counter.0, i32* %on_count, align 8, !dbg !110, !tbaa !63
store i32 %off_counter.0, i32* %off_count, align 4, !dbg !111, !tbaa !66
ret i8* null, !dbg !112
Writing '/tmp/cfgcontroller-2dc410.dot'... done.
Trying 'xdg-open' program... Remember to erase graph file: /tmp/cfgcontroller-2dc410.dot
Here is the actual image produced by xdot
.
Now I am working on trying to get SaverECS
to work, with my LLVM pass. I forked SaverECS
here, deleted all of your CMake cache data and files that were particular to your build system, and wrote a Makefile
. I will update you on my progress soon.
Thanks a lot, Max. You can initiate a pull request as well if you want.
Yep, I'll cut pull requests to both repositories once I have the SaverECS working too. Hopefully I'll get it done in the next week or two. Thanks!
I got SaverECS working. The main issue was that the bash code run from C++ would default to /usr/bin/clang
instead of my locally compiled v7.0.0 clang
, and the same issue for lli
and opt
. I will cut a pull request soon, where I provide a simple sed
command to fix this on your system, in my Makefile
. Thanks for all the help!
Great work.
Thanks Best wishes, Amit
On Fri, Mar 19, 2021, 8:15 AM Max von Hippel @.***> wrote:
I got SaverECS working. The main issue was that the bash code run from C++ would default to /usr/bin/clang instead of my locally compiled v7.0.0 clang, and the same issue for lli and opt. I will cut a pull request soon, where I provide a simple sed command to fix this on your system, in my Makefile. Thanks for all the help!
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/saverecs/SaverECS/issues/1#issuecomment-802498362, or unsubscribe https://github.com/notifications/unsubscribe-auth/AGCRI2FAB3K5WQ3FFZ653X3TEK3DXANCNFSM4YKVTLJQ .
Hi, thank you for making this interesting tool! I am trying to get it to compile and run, but I can't figure out how to make
libTestPass.so
work, including when I recompile it myself.Here is my Dockerfile, so you can reproduce my exact setup:
Compile the Dockerfile like this:
Then run the demo like this:
Here is the output:
Notice the important line:
Can you please help me with this?