Project

General

Profile

Revision 66e25f0f

View differences:

include/mpfr_lustre.c
1
#include <mpfr.h>
2
#include "mpfr_lustre.h"
3

  
4
void MPFR_LUSTRE_INIT () {
5
  return;
6
}
7

  
8
void MPFR_LUSTRE_CLEAR () {
9
  return;
10
}
11

  
12
void MPFRNeq_step (mpfr_t i1, mpfr_t i2, 
13
                          _Bool (*out)
14
                          )
15
{
16
  *out = mpfr_lessgreater_p(i1, i2);
17
}
18

  
19
void MPFREq_step (mpfr_t i1, mpfr_t i2, 
20
                         _Bool (*out)
21
                         )
22
{
23
  *out = mpfr_equal_p(i1, i2);
24
}
25

  
26
void MPFRGt_step (mpfr_t i1, mpfr_t i2, 
27
                         _Bool (*out)
28
                         )
29
{
30
  *out = mpfr_greater_p(i1, i2);
31
}
32

  
33
void MPFRGe_step (mpfr_t i1, mpfr_t i2, 
34
                         _Bool (*out)
35
                         )
36
{
37
  *out = mpfr_greaterequal_p(i1, i2);
38
}
39

  
40
extern void MPFRLt_step (mpfr_t i1, mpfr_t i2, 
41
                         _Bool (*out)
42
                         )
43
{
44
  *out = mpfr_less_p(i1, i2);
45
}
46
void MPFRLe_step (mpfr_t i1, mpfr_t i2, 
47
                         _Bool (*out)
48
                         )
49
{
50
  *out = mpfr_lessequal_p(i1, i2);
51
}
52

  
53
void MPFRDiv_step (mpfr_t i1, mpfr_t i2, 
54
                          mpfr_t out
55
                          )
56
{
57
  mpfr_div(out, i1, i2, MPFR_RNDN);
58
}
59

  
60
void MPFRTimes_step (mpfr_t i1, mpfr_t i2, 
61
                            mpfr_t out
62
                            )
63
{
64
  mpfr_mul(out, i1, i2, MPFR_RNDN);
65
}
66

  
67
void MPFRMinus_step (mpfr_t i1, mpfr_t i2, 
68
                            mpfr_t out
69
                            )
70
{
71
  mpfr_sub(out, i1, i2, MPFR_RNDN);
72
}
73

  
74
void MPFRPlus_step (mpfr_t i1, mpfr_t i2, 
75
                           mpfr_t out
76
                           )
77
{
78
  mpfr_add(out, i1, i2, MPFR_RNDN);
79
}
80

  
81
void MPFRUminus_step (mpfr_t i, 
82
                             mpfr_t out
83
                             )
84
{
85
  mpfr_neg(out, i, MPFR_RNDN);
86
}
87

  
88
void MPFRInit(mpfr_t i, mpfr_prec_t prec)
89
{
90
  mpfr_init2(i, prec);
91
}
92

  
93
void MPFRClear(mpfr_t i)
94
{
95
  mpfr_clear(i);
96
}
include/mpfr_lustre.lusi
1

  
2

  
3
function MPFRUminus(i: real) returns (out: real) lib gmp lib mpfr;
4

  
5
function MPFRPlus(i1, i2: real) returns (out: real);
6

  
7
function MPFRMinus(i1, i2: real) returns (out: real);
8

  
9
function MPFRTimes(i1, i2: real) returns (out: real);
10

  
11
function MPFRDiv(i1, i2: real) returns (out: real);
12

  
13
function MPFRLe(i1, i2: real) returns (out: bool);
14

  
15
function MPFRLt(i1, i2: real) returns (out: bool);
16

  
17
function MPFRGe(i1, i2: real) returns (out: bool);
18

  
19
function MPFRGt(i1, i2: real) returns (out: bool);
20

  
21
function MPFREq(i1, i2: real) returns (out: bool);
22

  
23
function MPFRNeq(i1, i2: real) returns (out: bool);
src/global.ml
1
let type_env : (Types.type_expr Env.t) ref = ref Env.initial
2
let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial
3
let basename = ref ""
4
let main_node = ref ""
5

  
6
module TypeEnv =
7
struct
8
let lookup_value ident = Env.lookup_value !type_env ident
9
let exists_value ident = Env.exists_value !type_env ident
10
let iter f = Env.iter !type_env f
11
let pp pp_fun fmt () = Env.pp_env pp_fun fmt !type_env
12
end
13

  
14
let initialize () =
15
  begin
16
    main_node := !Options.main_node;
17
  end
18

  
19
(* Local Variables: *)
20
(* compile-command:"make -C .." *)
21
(* End: *)
src/mpfr.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Utils
13
open LustreSpec
14
open Corelang
15
open Normalization
16
open Machine_code
17

  
18
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
19

  
20
let mpfr_rnd () = "MPFR_RNDN"
21

  
22
let mpfr_prec () = !Options.mpfr_prec
23

  
24
let inject_id = "MPFRId"
25

  
26
let inject_copy_id = "mpfr_set"
27

  
28
let inject_real_id = "mpfr_set_flt"
29

  
30
let inject_init_id = "mpfr_init2"
31

  
32
let inject_clear_id = "mpfr_clear"
33

  
34
let mpfr_t = "mpfr_t"
35

  
36
let unfoldable_value value =
37
  not (Types.is_real_type value.value_type && is_const_value value)
38

  
39
let inject_id_id expr =
40
  let e = mkpredef_call expr.expr_loc inject_id [expr] in
41
  { e with
42
    expr_type = Type_predef.type_real;
43
    expr_clock = expr.expr_clock;
44
  }
45

  
46
let pp_inject_real pp_var pp_val fmt var value =
47
  Format.fprintf fmt "%s(%a, %a, %s);"
48
    inject_real_id
49
    pp_var var
50
    pp_val value
51
    (mpfr_rnd ())
52

  
53
let inject_assign expr =
54
  let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
55
  { e with
56
    expr_type = Type_predef.type_real;
57
    expr_clock = expr.expr_clock;
58
  }
59

  
60
let pp_inject_copy pp_var fmt var value =
61
  Format.fprintf fmt "%s(%a, %a, %s);"
62
    inject_copy_id
63
    pp_var var
64
    pp_var value
65
    (mpfr_rnd ())
66

  
67
let rec pp_inject_assign pp_var fmt var value =
68
  if is_const_value value
69
  then
70
    pp_inject_real pp_var pp_var fmt var value
71
  else
72
    pp_inject_copy pp_var fmt var value
73

  
74
let pp_inject_init pp_var fmt var =
75
  Format.fprintf fmt "%s(%a, %i);"
76
    inject_init_id
77
    pp_var var
78
    (mpfr_prec ())
79

  
80
let pp_inject_clear pp_var fmt var =
81
  Format.fprintf fmt "%s(%a);"
82
    inject_clear_id
83
    pp_var var
84

  
85
let base_inject_op id =
86
  match id with
87
  | "+"      -> "MPFRPlus"
88
  | "-"      -> "MPFRMinus"
89
  | "*"      -> "MPFRTimes"
90
  | "/"      -> "MPFRDiv"
91
  | "uminus" -> "MPFRUminus"
92
  | "<="     -> "MPFRLe"
93
  | "<"      -> "MPFRLt"
94
  | ">="     -> "MPFRGe"
95
  | ">"      -> "MPFRGt"
96
  | "="      -> "MPFREq"
97
  | "!="     -> "MPFRNeq"
98
  | _        -> raise Not_found
99

  
100
let inject_op id =
101
  try
102
    base_inject_op id
103
  with Not_found -> id
104

  
105
let homomorphic_funs =
106
  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
107

  
108
let is_homomorphic_fun id =
109
  List.mem id homomorphic_funs
110

  
111
let inject_call expr =
112
  match expr.expr_desc with
113
  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
114
    { expr with expr_desc = Expr_appl (inject_op id, args, None) }
115
  | _ -> expr
116

  
117
let expr_of_const_array expr =
118
  match expr.expr_desc with
119
  | Expr_const (Const_array cl) ->
120
    let typ = Types.array_element_type expr.expr_type in
121
    let expr_of_const c =
122
      { expr_desc = Expr_const c;
123
	expr_type = typ;
124
	expr_clock = expr.expr_clock;
125
	expr_loc = expr.expr_loc;
126
	expr_delay = Delay.new_var ();
127
	expr_annot = None;
128
	expr_tag = new_tag ();
129
      }
130
    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
131
  | _                           -> assert false
132

  
133
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
134
let rec inject_list alias node inject_element defvars elist =
135
  List.fold_right
136
    (fun t (defvars, qlist) ->
137
      let defvars, norm_t = inject_element alias node defvars t in
138
      (defvars, norm_t :: qlist)
139
    ) elist (defvars, [])
140

  
141
let rec inject_expr ?(alias=true) node defvars expr =
142
let res=
143
  match expr.expr_desc with
144
  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr
145
  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
146
  | Expr_const (Const_struct _) -> assert false
147
  | Expr_ident _
148
  | Expr_const _  -> defvars, expr
149
  | Expr_array elist ->
150
    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
151
    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
152
    defvars, norm_expr
153
  | Expr_power (e1, d) ->
154
    let defvars, norm_e1 = inject_expr node defvars e1 in
155
    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
156
    defvars, norm_expr
157
  | Expr_access (e1, d) ->
158
    let defvars, norm_e1 = inject_expr node defvars e1 in
159
    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
160
    defvars, norm_expr
161
  | Expr_tuple elist -> 
162
    let defvars, norm_elist =
163
      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
164
    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
165
    defvars, norm_expr
166
  | Expr_appl (id, args, r) ->
167
    let defvars, norm_args = inject_expr node defvars args in
168
    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
169
    mk_expr_alias_opt alias node defvars (inject_call norm_expr)
170
  | Expr_arrow _ -> defvars, expr
171
  | Expr_pre e ->
172
    let defvars, norm_e = inject_expr node defvars e in
173
    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
174
    defvars, norm_expr
175
  | Expr_fby (e1, e2) ->
176
    let defvars, norm_e1 = inject_expr node defvars e1 in
177
    let defvars, norm_e2 = inject_expr node defvars e2 in
178
    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
179
    defvars, norm_expr
180
  | Expr_when (e, c, l) ->
181
    let defvars, norm_e = inject_expr node defvars e in
182
    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
183
    defvars, norm_expr
184
  | Expr_ite (c, t, e) ->
185
    let defvars, norm_c = inject_expr node defvars c in
186
    let defvars, norm_t = inject_expr node defvars t in
187
    let defvars, norm_e = inject_expr node defvars e in
188
    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
189
    defvars, norm_expr
190
  | Expr_merge (c, hl) ->
191
    let defvars, norm_hl = inject_branches node defvars hl in
192
    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
193
    defvars, norm_expr
194
in
195
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
196
res
197

  
198
and inject_branches node defvars hl =
199
 List.fold_right
200
   (fun (t, h) (defvars, norm_q) ->
201
     let (defvars, norm_h) = inject_expr node defvars h in
202
     defvars, (t, norm_h) :: norm_q
203
   )
204
   hl (defvars, [])
205

  
206

  
207
let rec inject_eq node defvars eq =
208
  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
209
  let norm_eq = { eq with eq_rhs = norm_rhs } in
210
  norm_eq::defs', vars'
211

  
212
(** normalize_node node returns a normalized node, 
213
    ie. 
214
    - updated locals
215
    - new equations
216
    - 
217
*)
218
let inject_node node = 
219
  cpt_fresh := 0;
220
  let inputs_outputs = node.node_inputs@node.node_outputs in
221
  let is_local v =
222
    List.for_all ((!=) v) inputs_outputs in
223
  let orig_vars = inputs_outputs@node.node_locals in
224
  let defs, vars = 
225
    List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) in
226
  (* Normalize the asserts *)
227
  let vars, assert_defs, asserts = 
228
    List.fold_left (
229
    fun (vars, def_accu, assert_accu) assert_ ->
230
      let assert_expr = assert_.assert_expr in
231
      let (defs, vars'), expr = 
232
	inject_expr 
233
	  ~alias:false 
234
	  node 
235
	  ([], vars) (* defvar only contains vars *)
236
	  assert_expr
237
      in
238
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
239
    ) (vars, [], []) node.node_asserts in
240
  let new_locals = List.filter is_local vars in
241
  (* Compute traceability info: 
242
     - gather newly bound variables
243
     - compute the associated expression without aliases     
244
  *)
245
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
246
  let node =
247
  { node with 
248
    node_locals = new_locals; 
249
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
250
  }
251
  in ((*Printers.pp_node Format.err_formatter node;*) node)
252

  
253
let inject_decl decl =
254
  match decl.top_decl_desc with
255
  | Node nd ->
256
    {decl with top_decl_desc = Node (inject_node nd)}
257
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
258
  
259
let inject_prog decls = 
260
  List.map inject_decl decls
261

  
262

  
263
(* Local Variables: *)
264
(* compile-command:"make -C .." *)
265
(* End: *)
src/plugins.ml
1
open LustreSpec
2

  
3
module type PluginType =
4
sig
5

  
6
end
7

  
8

  
9

  
10
let inline_annots rename_var_fun annot_list =
11
  List.map (
12
    fun ann -> 
13
      { ann with 
14
	annots = List.fold_left (
15
	  fun accu (sl, eexpr) -> 
16
	    let items = 
17
	      match sl with 
18
	      | plugin_name::args -> 
19
		if plugin_name = "salsa" then
20
		  match args with
21
		  | ["ranges";varname] -> 
22
		    [["salsa";"ranges";(rename_var_fun varname)], eexpr]
23
		  | _ -> [(sl, eexpr)]
24
		else
25
		  [(sl, eexpr)]
26
	    | _ -> assert false
27
	    in
28
	    items@accu
29
	) [] ann.annots
30
      }
31
  ) annot_list
32

  
33
(* Local Variables: *)
34
(* compile-command:"make -C .." *)
35
(* End: *)
test/test-compile.sh.in
1
#!/bin/bash
2

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

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

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

  
16
gcc_compile() {
17
    if [ $verbose -gt 1 ]; then
18
	echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
19
    fi
20
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
21
    if [ $? -ne 0 ]; then
22
	rgcc="INVALID";
23
    else
24
	rgcc="VALID"
25
    fi
26
}
27

  
28
lustrec_compile() {
29
    if [ $verbose -gt 1 ]; then
30
       echo "$LUSTREC $@"
31
    fi
32
    $LUSTREC "$@";
33
    if [ $? -ne 0 ]; then
34
        rlustrec="INVALID";
35
    else
36
        rlustrec="VALID"
37
    fi
38
}
39

  
40
base_compile() {
41
    while IFS=, read -r file main opts
42
    do
43
	name=`basename "$file" .lus`
44
        ext=".lus"
45
	if [ `dirname "$file"`/"$name" = "$file" ]; then
46
	    name=`basename "$file" .lusi`
47
	    ext=".lusi"
48
	fi
49
        dir=${SRC_PREFIX}/`dirname "$file"`
50
	pushd $dir > /dev/null
51

  
52
	if [ "$main" != "" ]; then
53
	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
54
	else
55
	    lustrec_compile -d $build -verbose 0 $opts $name$ext
56
	fi
57
	pushd $build > /dev/null
58

  
59
	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
60
            gcc_compile "$name";
61
	else
62
	    rgcc="NONE"
63
	fi
64
	popd > /dev/null
65
	popd > /dev/null
66

  
67
	if [ $verbose -gt 0 ]; then
68
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
69
	else
70
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
71
	fi;
72
    done < $file_list
73
}
74

  
75
inline_compile () {
76
    while IFS=, read -r file main opts
77
    do
78
	name=`basename "$file" .lus`
79
	ext=".lus"
80
	if [ `dirname "$file"`/"$name" = "$file" ]; then
81
	    name=`basename "$file" .lusi`
82
	    ext=".lusi"
83
	fi
84
	dir=${SRC_PREFIX}/`dirname "$file"`
85
	pushd $dir > /dev/null
86

  
87
	if [ "$main" != "" ]; then
88
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
89
	else
90
	    if [ "$ext" = ".lusi" ]; then
91
		lustrec_compile -d $build -verbose 0 $opts $name$ext;
92
	    else
93
		rlustrec="NONE"
94
		rgcc="NONE"
95
	    fi
96
	fi
97
	pushd $build > /dev/null
98

  
99
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
100
	    gcc_compile "$name";
101
	else
102
	    rgcc="NONE"
103
	fi
104
	popd > /dev/null
105
	popd > /dev/null
106

  
107
	if [ $verbose -gt 0 ]; then
108
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
109
	else
110
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
111
	fi;
112
    done < $file_list
113
}
114

  
115
inline_compile_with_check () {
116
# Checking inlining
117
    while IFS=, read -r file main opts
118
    do
119
	name=`basename "$file" .lus`
120
	ext=".lus"
121
	if [ `dirname "$file"`/"$name" = "$file" ]; then
122
	    name=`basename "$file" .lusi`
123
	    ext=".lusi"
124
	fi
125
	dir=${SRC_PREFIX}/`dirname "$file"`
126
	pushd $dir > /dev/null
127

  
128
	if [ "$main" != "" ]; then
129
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
130
	else
131
	    if [ "$ext" = ".lusi" ]; then
132
		lustrec_compile -d $build -verbose 0 $opts $name$ext;
133
	    else
134
		rlustrec="NONE"
135
		rgcc="NONE"
136
	    fi
137
	fi
138
	popd > /dev/null
139
	pushd $build > /dev/null
140
	
141
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
142
	    gcc_compile "$name";
143
	else
144
	    rgcc="NONE"
145
	fi
146
	# Cheching witness
147
       
148
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
149
	    mv ${name}_witnesses/inliner_witness.lus ${name}_inliner_witness.lus
150
	    lustrec_compile -verbose 0 -horn-traces -node check ${name}_inliner_witness.lus
151
	    z3="`z3 -T:10 ${name}_inliner_witness.smt2 | xargs`"
152
	    if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
153
		rinlining="VALID";
154
	    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
155
		rinlining="ERROR";
156
	    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
157
		rinlining="UNKNOWN";
158
	    elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
159
		rinlining="TIMEOUT"
160
	    else
161
		rinlining="INVALID"
162
	    fi
163
	else
164
	    rinlining="NONE"
165
	fi
166
	popd > /dev/null
167

  
168
	if [ $verbose -gt 0 ]; then
169
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
170
	else
171
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
172
	fi
173
done < $file_list
174

  
175
}
176

  
177
check_prop () {
178
    while IFS=, read -r file main opts
179
    do
180
	name=`basename "$file" .lus`
181
	if [ "$name" = "$file" ]; then
182
	    return 0
183
	fi
184
	dir=${SRC_PREFIX}/`dirname "$file"`
185
	pushd $dir > /dev/null
186
	
187
    # Checking horn backend
188
    if [ "$main" != "" ]; then
189
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
190
    else
191
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
192
    fi
193

  
194
    # echo "z3 $build/$name".smt2 
195
    # TODO: This part of the script has to be optimized
196
    z3="`z3 -T:10 ${build}/${name}.smt2 | xargs`"
197
    if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
198
	rhorn="VALID";
199
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
200
	rhorn="ERROR";
201
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
202
	rhorn="UNKNOWN";
203
    elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
204
	rhorn="TIMEOUT"
205
    else
206
	rhorn="INVALID"
207
    fi
208
    if [ $verbose -gt 0 ]; then
209
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
210
    else
211
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
212
    fi
213
    popd > /dev/null
214
done < $file_list
215
}
216

  
217
usage () {
218
echo "usage: $0 [-aciwh] file_list"
219
echo "-a: perform all steps"
220
echo "-c: basic compilation"
221
echo "-i: compile with inline mode"
222
echo "-w: compile with inline mode. Check the inlining with z3"
223
echo "-h: check files with the horn-pdf backend (requires z3)"
224
echo "-v <int>: verbose level"
225
}
226

  
227
verbose=0
228
nobehavior=1
229

  
230
while [ $# -gt 0 ] ; do
231
        case "$1" in
232
	        -v) shift ; verbose="$1"; shift ;;
233
	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
234
                -c) nobehavior=0; c=1 ; shift ;;
235
                -i) nobehavior=0; i=1 ; shift ;;
236
                -w) nobehavior=0; w=1 ; shift ;;
237
                -h) nobehavior=0; h=1 ; shift ;;
238
                --) shift ;;
239
                -*) echo "bad option '$1'" ; exit 1 ;;
240
                *) files=("${files[@]}" "$1") ; shift ;;
241
         esac
242
done
243

  
244
file_list=${files[0]}
245

  
246

  
247
if [ ${#files} -eq 0 ] ; then
248
    echo input list required
249
    usage
250
    exit 1
251
fi
252

  
253
# cleaning directory $build
254

  
255
rm -f "$build"/* 2> /dev/null
256

  
257
# executing tests
258

  
259
[ ! -z "$c" ] && base_compile
260
[ ! -z "$i" ] && inline_compile
261
[ ! -z "$w" ] && inline_compile_with_check
262
[ ! -z "$h" ] && check_prop
263
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
264

  
265

  
266
	# Removing Generated lusi file
267
	#grep generated ../${file}i > /dev/null
268
	#if [ $? -ne 1 ];then
269
	#  rm ../${file}i
270
	#fi
271

  

Also available in: Unified diff