Revision 3e209698
Added by Pierre-Loïc Garoche almost 9 years ago
| ex3.smt2 | ||
|---|---|---|
| 121 | 121 |
(top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x) |
| 122 | 122 |
)) |
| 123 | 123 |
|
| 124 |
; Collecting semantics with main node top
|
|
| 124 |
; Collecting semantics for node top
|
|
| 125 | 125 |
|
| 126 | 126 |
(declare-rel MAIN (Bool Bool Bool Int Bool)) |
| 127 | 127 |
; Initial set |
| ... | ... | |
| 135 | 135 |
)) |
| 136 | 136 |
|
| 137 | 137 |
; Inductive def |
| 138 |
(declare-var dummy Bool) |
|
| 139 | 138 |
(rule (=> |
| 140 |
(and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c dummy)
|
|
| 139 |
(and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.OK)
|
|
| 141 | 140 |
(top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x) |
| 142 | 141 |
) |
| 143 | 142 |
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK) |
| ... | ... | |
| 147 | 146 |
(declare-rel ERR ()) |
| 148 | 147 |
(rule (=> |
| 149 | 148 |
(and (not (= top.OK true)) |
| 150 |
(MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c)) |
|
| 149 |
(MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.OK))
|
|
| 151 | 150 |
ERR)) |
| 152 | 151 |
(query ERR) |
| src/horn_backend.ml | ||
|---|---|---|
| 11 | 11 |
match (Types.repr t).Types.tdesc with |
| 12 | 12 |
| Types.Tbool -> Format.fprintf fmt "Bool" |
| 13 | 13 |
| Types.Tint -> Format.fprintf fmt "Int" |
| 14 |
| Types.Treal -> Format.fprintf fmt "Real" |
|
| 14 | 15 |
| Types.Tclock _ |
| 15 | 16 |
| Types.Tarray _ |
| 16 | 17 |
| Types.Tstatic _ |
| ... | ... | |
| 314 | 315 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
| 315 | 316 |
|
| 316 | 317 |
Format.fprintf fmt "; Inductive def@."; |
| 317 |
Format.fprintf fmt "(declare-var dummy Bool)@."; |
|
| 318 | 318 |
Format.fprintf fmt |
| 319 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
|
|
| 319 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
|
| 320 | 320 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
| 321 | 321 |
node |
| 322 | 322 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 255 | 255 |
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*) |
| 256 | 256 |
end |
| 257 | 257 |
| "horn" -> begin |
| 258 |
let fmt = Format.std_formatter in |
|
| 258 |
let source_file = basename ^ ".smt2" in (* Could be changed *) |
|
| 259 |
let source_out = open_out source_file in |
|
| 260 |
let fmt = formatter_of_out_channel source_out in |
|
| 259 | 261 |
Horn_backend.translate fmt basename normalized_prog machine_code |
| 260 | 262 |
end |
| 261 | 263 |
| _ -> assert false |
| test/test-compile.sh | ||
|---|---|---|
| 11 | 11 |
# echo main:$main |
| 12 | 12 |
# echo opts:$opts |
| 13 | 13 |
if [ "$main" != "" ]; then |
| 14 |
$LUSTREC -d build -verbose 0 $opts -node $main ../$file; |
|
| 14 |
$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
|
|
| 15 | 15 |
else |
| 16 |
$LUSTREC -d build -verbose 0 $opts ../$file
|
|
| 16 |
$LUSTREC -horn -d build -verbose 0 $opts ../$file
|
|
| 17 | 17 |
fi |
| 18 | 18 |
if [ $? -ne 0 ]; then |
| 19 | 19 |
rlustrec="INVALID"; |
| 20 | 20 |
else |
| 21 | 21 |
rlustrec="VALID" |
| 22 | 22 |
fi |
| 23 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null |
|
| 23 |
echo z3 `basename $file .lus`.smt2 | grep unsat |
|
| 24 |
z3 `basename $file .lus`.smt2 | grep unsat > /dev/null |
|
| 24 | 25 |
if [ $? -ne 0 ]; then |
| 25 |
rgcc="INVALID";
|
|
| 26 |
rz3="INVALID";
|
|
| 26 | 27 |
else |
| 27 |
rgcc="VALID"
|
|
| 28 |
rz3="VALID"
|
|
| 28 | 29 |
fi |
| 29 |
echo "lustrec ($rlustrec),gcc ($rgcc),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
|
|
| 30 |
echo "lustrec -horn ($rlustrec),z3 ($rz3),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
|
|
| 30 | 31 |
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}'
|
| 31 | 32 |
done < ../tests_ok.list |
| test/tests_ok.list | ||
|---|---|---|
| 894 | 894 |
./src/kind_fmcad08/protocol/swimmingpool_2.lus,top |
| 895 | 895 |
./src/kind_fmcad08/protocol/rtp_1.lus,top |
| 896 | 896 |
./src/kind_fmcad08/protocol/swimmingpool_7.lus,top |
| 897 |
./src/arrays_arnaud/arrays.lus,,-check-access |
|
| 898 |
./src/arrays_arnaud/RelOpMatrix.lus |
|
| 899 |
./src/arrays_arnaud/access1.lus,,-check-access |
|
| 900 |
./src/arrays_arnaud/generic1.lus |
|
| 901 |
./src/arrays_arnaud/generic2.lus |
|
| 902 |
./src/arrays_arnaud/generic3.lus,top,-dynamic -check-access |
|
| 903 |
./src/clocks/clocks1.lus |
|
| 904 |
./src/clocks/clocks2.lus |
|
| 905 |
./src/clocks/oversampling0.lus |
|
Also available in: Unified diff
First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.