Project

General

Profile

Revision e41592cf

View differences:

.travis.yml
27 27
  - autoconf
28 28
  - ./configure
29 29
  - make
30
  - ./test/regression.sh -r -v 2 horn_regression.list
31

  
32

  
30 33

  
31 34
notifications:
32 35
  email:
33 36
    recipients:
34
     - lememta@gmail.com
37
     - lustrec-build@googlegroups.com
35 38
    on_success: always
36 39
    on_failure: always
autom4te.cache/requests
14 14
                        'configure.ac'
15 15
                      ],
16 16
                      {
17
                        '_LT_AC_TAGCONFIG' => 1,
18 17
                        'AM_PROG_F77_C_O' => 1,
19
                        'AC_INIT' => 1,
18
                        '_LT_AC_TAGCONFIG' => 1,
20 19
                        'm4_pattern_forbid' => 1,
21
                        '_AM_COND_IF' => 1,
20
                        'AC_INIT' => 1,
22 21
                        'AC_CANONICAL_TARGET' => 1,
23
                        'AC_SUBST' => 1,
22
                        '_AM_COND_IF' => 1,
24 23
                        'AC_CONFIG_LIBOBJ_DIR' => 1,
25
                        'AC_FC_SRCEXT' => 1,
24
                        'AC_SUBST' => 1,
26 25
                        'AC_CANONICAL_HOST' => 1,
26
                        'AC_FC_SRCEXT' => 1,
27 27
                        'AC_PROG_LIBTOOL' => 1,
28 28
                        'AM_INIT_AUTOMAKE' => 1,
29
                        'AM_PATH_GUILE' => 1,
30 29
                        'AC_CONFIG_SUBDIRS' => 1,
30
                        'AM_PATH_GUILE' => 1,
31 31
                        'AM_AUTOMAKE_VERSION' => 1,
32 32
                        'LT_CONFIG_LTDL_DIR' => 1,
33
                        'AC_REQUIRE_AUX_FILE' => 1,
34 33
                        'AC_CONFIG_LINKS' => 1,
35
                        'm4_sinclude' => 1,
34
                        'AC_REQUIRE_AUX_FILE' => 1,
36 35
                        'LT_SUPPORTED_TAG' => 1,
36
                        'm4_sinclude' => 1,
37 37
                        'AM_MAINTAINER_MODE' => 1,
38 38
                        'AM_NLS' => 1,
39 39
                        'AC_FC_PP_DEFINE' => 1,
40 40
                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
41
                        'AM_MAKEFILE_INCLUDE' => 1,
42 41
                        '_m4_warn' => 1,
42
                        'AM_MAKEFILE_INCLUDE' => 1,
43 43
                        'AM_PROG_CXX_C_O' => 1,
44
                        '_AM_COND_ENDIF' => 1,
45 44
                        '_AM_MAKEFILE_INCLUDE' => 1,
45
                        '_AM_COND_ENDIF' => 1,
46 46
                        'AM_ENABLE_MULTILIB' => 1,
47 47
                        'AM_SILENT_RULES' => 1,
48 48
                        'AM_PROG_MOC' => 1,
49 49
                        'AC_CONFIG_FILES' => 1,
50
                        'include' => 1,
51 50
                        'LT_INIT' => 1,
52
                        'AM_PROG_AR' => 1,
51
                        'include' => 1,
53 52
                        'AM_GNU_GETTEXT' => 1,
53
                        'AM_PROG_AR' => 1,
54 54
                        'AC_LIBSOURCE' => 1,
55
                        'AM_PROG_FC_C_O' => 1,
56 55
                        'AC_CANONICAL_BUILD' => 1,
56
                        'AM_PROG_FC_C_O' => 1,
57 57
                        'AC_FC_FREEFORM' => 1,
58
                        'AH_OUTPUT' => 1,
59 58
                        'AC_FC_PP_SRCEXT' => 1,
60
                        '_AM_SUBST_NOTMAKE' => 1,
59
                        'AH_OUTPUT' => 1,
61 60
                        'AC_CONFIG_AUX_DIR' => 1,
62
                        'sinclude' => 1,
63
                        'AM_PROG_CC_C_O' => 1,
61
                        '_AM_SUBST_NOTMAKE' => 1,
64 62
                        'm4_pattern_allow' => 1,
65
                        'AM_XGETTEXT_OPTION' => 1,
66
                        'AC_CANONICAL_SYSTEM' => 1,
63
                        'AM_PROG_CC_C_O' => 1,
64
                        'sinclude' => 1,
67 65
                        'AM_CONDITIONAL' => 1,
66
                        'AC_CANONICAL_SYSTEM' => 1,
67
                        'AM_XGETTEXT_OPTION' => 1,
68 68
                        'AC_CONFIG_HEADERS' => 1,
69 69
                        'AC_DEFINE_TRACE_LITERAL' => 1,
70 70
                        'AM_POT_TOOLS' => 1,
regression_tests/local_inline.lus
55 55
let
56 56

  
57 57
  -- MAIN;
58
  -- assert Primary_Side = (Primary_Side -> pre( Primary_Side));
59
  -- assert PFS_Initial_Value =  (PFS_Initial_Value -> pre( PFS_Initial_Value));
58
  assert Primary_Side = (Primary_Side -> pre( Primary_Side));
59
  assert PFS_Initial_Value =  (PFS_Initial_Value -> pre( PFS_Initial_Value));
60 60
  assert State>=0 and State <=5;
61 61
  assert  Inhibit_count>=0 and  Inhibit_count <=2;
62 62
  
......
400 400

  
401 401

  
402 402

  
403
node PFS_contract_R2
403
node top
404 404
  (TS, CLK1, CLK3, CLK2, CLK4 : bool)
405 405
returns
406 406
  (OK : bool) ;
regression_tests/stateful_assert.lus
1 1

  
2
node PFS_Side
2
node top
3 3
  (TS, OSPF : bool;
4 4
   Primary_Side : bool)
5 5

  
src/Makefile
1
OCAMLBUILD=/Users/teme/.opam/4.02.0+trunk/bin/ocamlbuild -classic-display -no-links 
1
OCAMLBUILD=/Users/teme/.opam/4.02.1/bin/ocamlbuild -classic-display -no-links 
2 2

  
3 3
prefix=/usr/local
4 4
exec_prefix=${prefix}
src/backends/Horn/horn_backend.ml
522 522

  
523 523

  
524 524
let translate fmt basename prog machines =
525
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification");
526 525
  List.iter (print_machine machines fmt) (List.rev machines);
527 526
  main_print machines fmt
528 527

  
src/main_lustre_compiler.ml
299 299
	let source_file = destname ^ ".smt2" in (* Could be changed *)
300 300
	let source_out = open_out source_file in
301 301
	let fmt = formatter_of_out_channel source_out in
302
        Log.report ~level:1 (fun fmt -> fprintf fmt "@.. hornification@,");
302 303
	Horn_backend.translate fmt basename prog machine_code;
303 304
	(* Tracability file if option is activated *)
304 305
	if !Options.traces then (
305
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
306
	let traces_out = open_out traces_file in
307
	let fmt = formatter_of_out_channel traces_out in
308
	Horn_backend.traces_file fmt basename prog machine_code;
306
	  let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
307
	  let traces_out = open_out traces_file in
308
	  let fmt = formatter_of_out_channel traces_out in
309
          Log.report ~level:1 (fun fmt -> fprintf fmt "@.. tracing info@,");
310
	  Horn_backend.traces_file fmt basename prog machine_code;
309 311
	)
310 312
      end
311 313
    | "lustre" ->
......
321 323
    | _ -> assert false
322 324
  in
323 325
  begin
324
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
326
    Log.report ~level:1 (fun fmt -> fprintf fmt "@.. done @ @]@.");
325 327
  (* We stop the process here *)
326 328
    exit 0
327 329
  end
src/myocamlbuild.ml
5 5
dispatch begin function
6 6
| After_rules ->
7 7
    (* We declare external libraries *)
8
    ocaml_lib ~extern:true ~dir:"/Users/teme/.opam/4.02.0+trunk/lib/ocamlgraph" "graph";
8
    ocaml_lib ~extern:true ~dir:"/Users/teme/.opam/4.02.1/lib/ocamlgraph" "graph";
9 9
  if @CC_NOASNEEDED@ then
10 10
    flag ["ocaml"; "link"]
11 11
      (S [A"-cclib";A"-Wl,--no-as-needed"]);
src/normalization.ml
379 379
	  annots = List.map (fun v ->
380 380
	    let eq =
381 381
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
383 383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384
	    let expr = substitute_expr diff_vars defs eq.eq_rhs in
384
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
385 385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386 386
	    (["traceability"], pair)
387 387
	  ) diff_vars;
src/scheduling.ml
31 31
   For variables still unrelated, standard compare is used to choose the minimal element.
32 32
   This priority is used since it helps a lot in factorizing generated code.
33 33
   Moreover, the dependency graph is browsed in a depth-first manner whenever possible,
34
   to improve the behavior of optimization algorithms applied in forthcoming compilation steps. 
34
   to improve the behavior of optimization algorithms applied in forthcoming compilation steps.
35 35
   In the following functions:
36 36
   - [eq_equiv] is the equivalence relation between vars of the same equation lhs
37 37
   - [g] the (imperative) graph to be topologically sorted
......
46 46
 List.exists ExprDep.is_instance_var (IdentDepGraph.succ g choice)
47 47

  
48 48
(* Adds successors of [v] in graph [g] in [pending] or [frontier] sets, wrt [eq_equiv],
49
   then removes [v] from [g] 
49
   then removes [v] from [g]
50 50
*)
51 51
let add_successors eq_equiv g v pending frontier =
52 52
  let succs_v = IdentDepGraph.succ g v in
53 53
  begin
54 54
    IdentDepGraph.remove_vertex g v;
55
    List.iter 
56
      (fun v' -> 
57
	if is_graph_root v' g then 
58
	  (if eq_equiv v v' then 
59
	      pending := ISet.add v' !pending 
55
    List.iter
56
      (fun v' ->
57
	if is_graph_root v' g then
58
	  (if eq_equiv v v' then
59
	      pending := ISet.add v' !pending
60 60
	   else
61 61
	      frontier := ISet.add v' !frontier)
62 62
      ) succs_v;
......
134 134
      with Not_found -> false in
135 135

  
136 136
    let n', g = global_dependency n in
137
    Log.report ~level:5 
138
      (fun fmt -> 
137
    Log.report ~level:5
138
      (fun fmt ->
139 139
	Format.fprintf fmt
140
	  "dependency graph for node %s: %a" 
140
	  "dependency graph for node %s: %a"
141 141
	  n'.node_id
142 142
	  pp_dep_graph g
143 143
      );
144
    
144

  
145 145
    (* TODO X: extend the graph with inputs (adapt the causality analysis to deal with inputs
146 146
     compute: coi predecessors of outputs
147 147
     warning (no modification) when memories are non used (do not impact output) or when inputs are not used (do not impact output)
......
152 152
    let sort = topological_sort eq_equiv g in
153 153
    let unused = Liveness.compute_unused_variables n gg in
154 154
    let fanin = Liveness.compute_fanin n gg in
155
 
155

  
156 156
    let (disjoint, reuse) =
157 157
      if !Options.optimization >= 3
158 158
      then
......
166 166
    if !Options.print_reuse
167 167
    then
168 168
      begin
169
	Log.report ~level:0 
170
	  (fun fmt -> 
169
	Log.report ~level:0
170
	  (fun fmt ->
171 171
	    Format.fprintf fmt
172 172
	      "OPT:%B@." (try (Hashtbl.iter (fun s1 v2 -> if s1 = v2.var_id then raise Not_found) reuse; false) with Not_found -> true)
173 173
	  );
174
	Log.report ~level:0 
175
	  (fun fmt -> 
174
	Log.report ~level:0
175
	  (fun fmt ->
176 176
	    Format.fprintf fmt
177
	      "OPT:clock disjoint map for node %s: %a" 
177
	      "OPT:clock disjoint map for node %s: %a"
178 178
	      n'.node_id
179 179
	      Disjunction.pp_disjoint_map disjoint
180 180
	  );
181
	Log.report ~level:0 
182
	  (fun fmt -> 
181
	Log.report ~level:0
182
	  (fun fmt ->
183 183
	    Format.fprintf fmt
184
	      "OPT:reuse policy for node %s: %a" 
184
	      "OPT:reuse policy for node %s: %a"
185 185
	      n'.node_id
186 186
	      Liveness.pp_reuse_policy reuse
187 187
	  );
......
196 196
  List.fold_right (
197 197
    fun top_decl (accu_prog, sch_map)  ->
198 198
      match top_decl.top_decl_desc with
199
	| Node nd -> 
199
	| Node nd ->
200 200
	  let nd', report = schedule_node nd in
201
	  {top_decl with top_decl_desc = Node nd'}::accu_prog, 
201
	  {top_decl with top_decl_desc = Node nd'}::accu_prog,
202 202
	  IMap.add nd.node_id report sch_map
203 203
	| _ -> top_decl::accu_prog, sch_map
204
    ) 
204
    )
205 205
    prog
206 206
    ([],IMap.empty)
207 207

  
......
210 210
  | []  -> assert false
211 211
  | [v] -> Format.fprintf fmt "%s" v
212 212
  | _   -> Format.fprintf fmt "(%a)" (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) vl
213
 
213

  
214 214
let pp_schedule fmt node_schs =
215 215
 IMap.iter
216 216
   (fun nd report ->
test/Makefile
4 4
	@bash ./test-compile.sh -a -v 2 tests_ok.list
5 5
	@rm build/*.o
6 6

  
7
horn:
8
	@bash ./regression.sh -r -v 2 horn_regression.list
9

  
7 10
clean:
8 11
	@rm -rf build
9 12
	@for i in `find . -iname *.lusi`; do grep generated $$i > /dev/null; if [ $$? -eq 0 ]; then rm $$i; fi; done
10 13

  
11 14
distclean: clean
12
	@rm -rf report*
13

  
15
	@rm -rf horn-report*
test/horn_regression.list
1
../regression_tests/check_validity.lus,top
2
../regression_tests/local_inline.lus,top
3
../regression_tests/stateful_assert.lus,top
4
../regression_tests/traffic.lus,top
5

  
test/regression.sh
1
#!/bin/bash
2

  
3
#eval set -- $(getopt -n $0 "-aciwvh:" -- "$@")
4

  
5
declare c i w h a v r
6
declare -a files
7

  
8
#SRC_PREFIX="../.."
9
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
10
NOW=`date "+%y-%m-%d-%H:%M"`
11
report=`pwd`/horn-report-$NOW
12
#LUSTREC="../../_build/src/lustrec"
13
LUSTREC=../bin/lustrec
14
mkdir -p build-$NOW
15
build=`pwd`/build-$NOW
16

  
17

  
18
check_horn () {
19
    while IFS=, read -r file main opts
20
    do
21
	name=`basename "$file" .lus`
22
	if [ "$name" = "$file" ]; then
23
	    return 0
24
	fi
25
	dir=${SRC_PREFIX}`dirname "$file"`
26
	pushd $dir > /dev/null
27

  
28
    # Checking horn backend
29
    if [ "$main" != "" ]; then
30
        $LUSTREC -horn-traces -horn-query -d $build -verbose 0 $opts -node $main "$name".lus
31
    else
32
	$LUSTREC -horn-traces -horn-query -d $build -verbose 0 $opts "$name".lus
33
    fi
34
    if [ $? -ne 0 ]; then
35
        rlustrec="ERROR";
36
    else
37
        rlustrec="OK"
38
    fi
39
    if [ $verbose -gt 0 ]; then
40
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
41
    else
42
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
43
    fi
44
    popd > /dev/null
45
done < $file_list
46
}
47

  
48
usage () {
49
echo "usage: $0 [-aciwh] file_list"
50
echo "-r: regression test for horn backend"
51
echo "-v <int>: verbose level"
52
}
53

  
54
verbose=0
55
nobehavior=1
56

  
57
while [ $# -gt 0 ] ; do
58
        case "$1" in
59
	        -v) shift ; verbose="$1"; shift ;;
60
                -r) nobehavior=0; r=1 ; shift ;;
61
                --) shift ;;
62
                -*) echo "bad option '$1'" ; exit 1 ;;
63
                *) files=("${files[@]}" "$1") ; shift ;;
64
         esac
65
done
66

  
67
file_list=${files[0]}
68

  
69

  
70
if [ ${#files} -eq 0 ] ; then
71
    echo input list required
72
    usage
73
    exit 1
74
fi
75

  
76
[ ! -z "$r" ] && check_horn
77
mv $report $build
78
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
test/test-compile.sh
131 131
        rgcc2="INVALID";
132 132
    else
133 133
        rgcc2="VALID"
134
    fi	
134
    fi
135 135
    popd > /dev/null
136 136
	# Cheching witness
137 137
    pushd $build > /dev/null
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
139 139
    popd > /dev/null
140 140
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141 141
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
146 146
	rinlining="UNKNOWN";
147 147
    else
148 148
	rinlining="INVALID/TIMEOUT"
149
    fi  
149
    fi
150 150
    if [ $verbose -gt 0 ]; then
151 151
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
152 152
    else
......
166 166
	fi
167 167
	dir=${SRC_PREFIX}/`dirname "$file"`
168 168
	pushd $dir > /dev/null
169
	
169

  
170 170
    # Checking horn backend
171 171
    if [ "$main" != "" ]; then
172 172
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
......
178 178
    else
179 179
        rlustrec="VALID"
180 180
    fi
181
    # echo "z3 $build/$name".smt2 
181
    # echo "z3 $build/$name".smt2
182 182
    # TODO: This part of the script has to be optimized
183 183
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
184 184
    if [ $? -ne 0 ]; then
......
195 195
done < $file_list
196 196
}
197 197

  
198
check_horn () {
199
    while IFS=, read -r file main opts
200
    do
201
	name=`basename "$file" .lus`
202
	if [ "$name" = "$file" ]; then
203
	    return 0
204
	fi
205
	dir=${SRC_PREFIX}/`dirname "$file"`
206
	pushd $dir > /dev/null
207

  
208
    # Checking horn backend
209
    if [ "$main" != "" ]; then
210
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
211
    else
212
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
213
    fi
214
    if [ $? -ne 0 ]; then
215
        rlustrec="INVALID";
216
    else
217
        rlustrec="VALID"
218
    fi
219
    if [ $verbose -gt 0 ]; then
220
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
221
    else
222
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
223
    fi
224
    popd > /dev/null
225
done < $file_list
226
}
227

  
198 228
usage () {
199 229
echo "usage: $0 [-aciwh] file_list"
200 230
echo "-a: perform all steps"
......
202 232
echo "-i: compile with inline mode"
203 233
echo "-w: compile with inline mode. Check the inlining with z3"
204 234
echo "-h: check files with the horn-pdf backend (requires z3)"
235
echo "-r: regression test for horn backend"
205 236
echo "-v <int>: verbose level"
206 237
}
207 238

  
......
215 246
                -c) nobehavior=0; c=1 ; shift ;;
216 247
                -i) nobehavior=0; i=1 ; shift ;;
217 248
                -w) nobehavior=0; w=1 ; shift ;;
249
                -r) nobehavior=0; r=1 ; shift ;;
218 250
                -h) nobehavior=0; h=1 ; shift ;;
219 251
                --) shift ;;
220 252
                -*) echo "bad option '$1'" ; exit 1 ;;
......
235 267
[ ! -z "$i" ] && inline_compile
236 268
[ ! -z "$w" ] && inline_compile_with_check
237 269
[ ! -z "$h" ] && check_prop
270
[ ! -z "$r" ] && check_horn
238 271
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
239 272

  
240 273

  
......
243 276
	#if [ $? -ne 1 ];then
244 277
	#  rm ../${file}i
245 278
	#fi
246

  

Also available in: Unified diff