From c61e01f19b1ba768117cfef0a0ae23f4d3cec5a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Tue, 14 Jan 2014 23:09:22 +0100 Subject: [PATCH 1/8] Correct handling of comparison operators in Sigali - bug fix: comparison between two non-constant integer expressions in Sigali - bug fix: correct handling of "=" and "<>" operators in Sigali --- CHANGES | 8 +++- Makefile-distrib | 2 +- compiler/minils/sigali/sigali.ml | 3 ++ compiler/minils/sigali/sigali.mli | 2 + compiler/minils/sigali/sigalimain.ml | 45 ++++++++++++------- compiler/utilities/global/compiler_options.ml | 2 +- 6 files changed, 43 insertions(+), 19 deletions(-) diff --git a/CHANGES b/CHANGES index 5090f23..56ba9ef 100644 --- a/CHANGES +++ b/CHANGES @@ -1,8 +1,14 @@ +Heptagon 1.00.04 (14/01/2014) +----------------------------- + + - bug fix: comparison between two non-constant integer expressions in Sigali + - bug fix: correct handling of "=" and "<>" operators in Sigali + Heptagon 1.00.03 (20/11/2013) ----------------------------- - - buf fix: tomato application with contracts + - bug fix: tomato application with contracts Heptagon 1.00.02 (29/10/2013) ----------------------------- diff --git a/Makefile-distrib b/Makefile-distrib index 5b5a579..7c78be6 100644 --- a/Makefile-distrib +++ b/Makefile-distrib @@ -2,7 +2,7 @@ include config #version = $(shell date +"%d%m%y") -version = 1.00.03 +version = 1.00.04 osname=$(shell uname -s) hardware=$(shell uname -m) heptdir = heptagon-$(version) diff --git a/compiler/minils/sigali/sigali.ml b/compiler/minils/sigali/sigali.ml index 3143af7..65e6382 100644 --- a/compiler/minils/sigali/sigali.ml +++ b/compiler/minils/sigali/sigali.ml @@ -153,6 +153,9 @@ let a_inf e1 e2 = let a_sup e1 e2 = Sprim ("a_sup", [e1;e2]) +let a_iminv e1 e2 = + Sprim ("a_iminv", [e1;e2]) + module Printer = struct open Format diff --git a/compiler/minils/sigali/sigali.mli b/compiler/minils/sigali/sigali.mli index 6d53909..4dbdf19 100644 --- a/compiler/minils/sigali/sigali.mli +++ b/compiler/minils/sigali/sigali.mli @@ -119,6 +119,8 @@ val a_inf : exp -> exp -> exp val a_sup : exp -> exp -> exp +val a_iminv : exp -> exp -> exp + module Printer : sig val print : string -> processus list -> unit diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 64b82a0..c423a7d 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -126,8 +126,7 @@ let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty }) = | Minils.Wreinit _ -> raise Untranslatable (* [translate e = c] *) -let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = - let ty = actual_ty ty in +let rec translate prefix ({ Minils.e_desc = desc } as e) = match desc with | Minils.Eextvalue(ext) -> translate_ext prefix ext | Minils.Eapp (* pervasives binary or unary stateless operations *) @@ -140,13 +139,24 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = (translate_ext prefix e2)) | "&", [e1;e2] -> Sand((translate_ext prefix e1), (translate_ext prefix e2)) - | ("<="|"<"|">="|">"), [e1;e2] -> + | "=", [e1;e2] when (actual_ty e1.Minils.w_ty) = Tbool -> + let e1 = translate_ext prefix e1 in + let e2 = translate_ext prefix e2 in + (* e1 = e2 iff (e1 and e2) or (not e1 and not e2) *) + (e1 &~ e2) |~ ((~~ e1) &~ (~~ e2)) + | "<>", [e1;e2] when (actual_ty e1.Minils.w_ty) = Tbool -> + let e1 = translate_ext prefix e1 in + let e2 = translate_ext prefix e2 in + (* e1 <> e2 iff (e1 and not e2) or (not e1 and e2) *) + (e1 &~ (~~ e2)) |~ ((~~ e1) &~ e2) + | ("<="|"<"|">="|">"|"="), [e1;e2] -> let op,modv = begin match n with | "<=" -> a_inf,0 | "<" -> a_inf,-1 | ">=" -> a_sup,0 - | _ -> a_sup,1 + | ">" -> a_sup,1 + | _ -> a_iminv,0 (* p(x)=k <> p = inverse image of k *) end in let e1 = translate_ext prefix e1 in let sig_e = @@ -155,27 +165,30 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = op e1 (Sconst(Cint(v+modv))) | _ -> let e2 = translate_ext prefix e2 in - op (Sminus(e1,e2)) (Sconst(Cint(modv))) + op (Splus(e1,(Sprod(e2,(Sconst(Cint(-1))))))) (Sconst(Cint(modv))) end in - (* a_inf and a_sup : +1 to translate ideals to boolean + (* a_inf, a_sup and a_iminv : +1 to translate ideals to boolean polynomials *) Splus(sig_e,Sconst(Ctrue)) + | "<>", [e1;e2] -> + (* e1 <> e2 --> not(a_iminv((e1+(e2*(-1))),0)) *) + let e1 = translate_ext prefix e1 in + let sig_e = + begin match e2.Minils.w_desc with + | Minils.Wconst({se_desc = Sint(v)}) -> + a_iminv e1 (Sconst(Cint(v))) + | _ -> + let e2 = translate_ext prefix e2 in + a_iminv (Splus(e1,(Sprod(e2,(Sconst(Cint(-1))))))) (Sconst(Cint(0))) + end in + (* a_iminv : +1 to translate ideals to boolean polynomials *) + Snot(Splus(sig_e,Sconst(Ctrue))) | "+", [e1;e2] -> Splus((translate_ext prefix e1), (translate_ext prefix e2)) | "-", [e1;e2] -> Splus((translate_ext prefix e1), (Sprod((translate_ext prefix e2),(Sconst(Cint(-1)))))) | "*", [e1;e2] -> Sprod((translate_ext prefix e1), (translate_ext prefix e2)) - | "=", [e1;e2] when (ty = Tbool) -> - let e1 = translate_ext prefix e1 in - let e2 = translate_ext prefix e2 in - (* e1 = e2 iff (e1 and e2) or (not e1 and not e2) *) - (e1 &~ e2) |~ ((~~ e1) &~ (~~ e2)) - | "<>", [e1;e2] when ty = Tbool -> - let e1 = translate_ext prefix e1 in - let e2 = translate_ext prefix e2 in - (* e1 <> e2 iff (e1 and not e2) or (not e1 and e2) *) - (e1 &~ (~~ e2)) |~ ((~~ e1) &~ e2) | _ -> raise Untranslatable end (* | Minils.Ewhen(e, c, var) when ((actual_ty e.Minils.e_ty) = Tbool) -> *) diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index e6761f7..751d84d 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -32,7 +32,7 @@ open Names (* version of the compiler *) -let version = "1.00.03" +let version = "1.00.04" let date = "DATE" (* standard module *) From 1a373b84eb4124e100e204d93b4ccaf6197b6698 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Wed, 15 Jan 2014 00:07:29 +0100 Subject: [PATCH 2/8] Added some tests Tests from image_filters Examples of array iterators used --- test/good/convolutions.ept | 47 ++++++++++++ test/good/downscale.ept | 152 +++++++++++++++++++++++++++++++++++++ test/good/foldi_arrays.ept | 24 ++++++ test/good/mapnot.ept | 15 ++++ test/good/pip.ept | 19 +++++ test/good/pip_slice.ept | 19 +++++ test/good/quasi.ept | 51 +++++++++++++ 7 files changed, 327 insertions(+) create mode 100644 test/good/convolutions.ept create mode 100644 test/good/downscale.ept create mode 100644 test/good/foldi_arrays.ept create mode 100644 test/good/mapnot.ept create mode 100644 test/good/pip.ept create mode 100644 test/good/pip_slice.ept create mode 100644 test/good/quasi.ept diff --git a/test/good/convolutions.ept b/test/good/convolutions.ept new file mode 100644 index 0000000..a20bbe6 --- /dev/null +++ b/test/good/convolutions.ept @@ -0,0 +1,47 @@ +(* Deal with matrix of size n*m, apply coeff : + kt + kl k kr + kb + centered on [>i<][>j<]. *) +fun kernel_1 << n,m,k,kl,kt,kr,kb :int>> (t :int^n^m; i,x,j :int) returns (r :int) +let + r = k*t[>i<][>j<] + kl*t[>i<][>j-1<] + kt*t[>i-1<][>j<] + kr*t[>i<][>j+1<] + kb*t[>i+1<][>j<] +tel + +fun convol_1_h <> (t:int^n^m; line : int^m; i :int) returns (r :int^m) +let + r = mapi<> (kernel_1<>)<(t,i)> (line) +tel + +fun convol_1 <> (t:int^n^m) returns (r :int^n^m) +let + r = mapi<> ( convol_1_h<> ) <(t)> (t) +tel + + +(* Deal with matrix of size n*m, apply coeff : + ktt + klt kt ktr + kll kl k kr krr + kbl kb krb + kbb + centered on [>i<][>j<]. *) +fun kernel_2 <> (t :int^n^m; i,x,j :int) returns (r :int) +let + r = ktt*t[>i-2<][>j<]+ + klt*t[>i-1<][>j-1<]+ kt*t[>i-1<][>j<]+ ktr*t[>i-1<][>j+1<]+ + kll*t[>i<][>j-2<]+ kl*t[>i<][>j-1<]+ k*t[>i<][>j<]+ kr*t[>i<][>j+1<]+ krr*t[>i<][>j+2<]+ + kbl*t[>i+1<][>j-1<]+ kb*t[>i+1<][>j<]+ krb*t[>i+1<][>j+1<]+ + kbb*t[>i+2<][>j<]; +tel + +fun convol_2_h<> (t:int^n^m; line : int^m; i :int) returns (r :int^m) +let + r = mapi<> (kernel_2<>) <(t,i)> (line) +tel + +fun convol_2<>(t:int^n^m) returns (r :int^n^m) +let + r = mapi<> (convol_2_h<>) <(t)> (t) +tel + diff --git a/test/good/downscale.ept b/test/good/downscale.ept new file mode 100644 index 0000000..4fc1c9f --- /dev/null +++ b/test/good/downscale.ept @@ -0,0 +1,152 @@ + +type pixel = float^3 + +node nat() returns (n :int) +let + n = 0 fby n+1 +tel + +fun pix_sum(x1,x2 :pixel) returns (r :pixel) +let + r = map<<3>> (+.) (x1,x2); +tel + +fun pix_div(x :pixel; c :float) returns (r :pixel) +let + r = map<<3>> (/.) (x, c^3); +tel + +const pix_zero :pixel = 0.0^3 +const pix_o :pixel = [1.0,1.0,1.0] + +node counter() returns (cpt :int) +let + cpt = (0 fby cpt) + 1 +tel + +node counter_r(res :bool) returns (cpt :int) +let + reset + cpt = inlined counter() + every res +tel + +(* count from 1 to m included, reset to 1 when [res] *) +node mod_counter_r<>(res :bool) returns (cpt :int) +let + reset + cpt = (0 fby cpt) + 1 + every (res or (0 fby cpt = m)) +tel + +(* count from 1 to m included *) +node mod_counter<>() returns (cpt :int) +let + cpt = inlined mod_counter_r<>(false) +tel + + +node current(x :int; ck :bool) returns (c :int) +let + c = merge ck x ((0 fby c) whenot ck) +tel +node current_bool(x :bool; ck :bool) returns (c :bool) +let + c = merge ck x ((false fby c) whenot ck) +tel + +fun flatten_clock(x :pixel ::.on ck on ck2; ck :bool ::.; ck2 :bool ::.on ck) returns (y :pixel; ck2_flat :bool :: .) +var x_ck, x_base : pixel; +let + x_ck = merge ck2 x pix_o; + x_base = merge ck x_ck pix_o; + ck2_flat = merge ck ck2 false; + y = x_base when ck2_flat; +tel + + +node transpose<>(i :pixel) returns (o :pixel) +var store :pixel^x^y^2; (*This is the double buffer*) + i_x, i_y, o_x, o_y :int; (*These are current buffer indexes*) + i_line, o_line, i_img :bool; (*These define line and img beginning*) + i_buff, o_buff :int; (*These are used to control the double buffering*) +let + i_x = mod_counter<>() - 1; + i_line = i_x = 0; + i_y = current (mod_counter<>() - 1, i_line); + i_img = (i_x = 0) & (i_y = 0); + i_buff = current(mod_counter<<2>>() - 1, i_img); + o_buff = (i_buff + 1) % 2; + o_y = mod_counter<>() -1; + o_line = o_y = 0; + o_x = current (mod_counter<>()-1, o_line); + store = (pix_zero^x^y^2) fby [store with [i_buff][i_y][i_x] = i]; + o = store[>o_buff<][>o_y<][>o_x<]; +tel + + +(* a fby-n would be nice to allow average of the last n pixels *) +(* returns the average of the last 3 pixels when asked *) +node down(x :pixel; out :bool) returns (r :pixel :: . on out) +var x1, x2 : pixel; +let + x1 = x fby x; + x2 = x fby x1; + r = pix_div(pix_sum(x when out, pix_sum(x1 when out, x2 when out)), 3.0 ); +tel + +node down_line<>(x :pixel) returns (r :pixel; r_clock :bool) +let + r_clock = mod_counter<>() = ratio; + r = down(x,r_clock); +tel + + +node down_img <> (x :pixel :: .) +returns (y_flat :pixel; y_clock :bool; + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool + ) +var + x_line, y_dh_t_line :bool; + +let + x_line = mod_counter<>() = 1; + reset + (y_dh, ck_y_dh) = down_line<>(x) + every x_line; + y_dh_t = transpose<>(y_dh); + y_dh_t_line = current_bool(mod_counter<>() = 1, ck_y_dh); + reset + (y_dhv_t, ck_y_dhv) = down_line<>(y_dh_t) + every y_dh_t_line; + y = transpose<>(y_dhv_t); + (*flatten clock of y, in order to return only one, instead of ck_y_dh on ck_y_dhv*) + (y_flat, y_clock) = flatten_clock(y, ck_y_dh, ck_y_dhv); +tel + + +(*node main () returns (img, out : pixel; ck_out, ck_out_2 :bool) +(*var img : pixel;*) +let + img = pix_o; + (out, ck_out, ck_out_2) = down_img<<2,2,2,2>>(img); +tel*) + +node mainp<> () returns (img, out : pixel; ck_out :bool; + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool) +(*var img : pixel;*) +let + (*ck_out = true fby false fby not ck_out;*) + img = pix_o fby pix_sum(img, pix_o); + (out, ck_out, y, y_dh, y_dh_t, y_dhv_t, ck_y_dh, ck_y_dhv) = down_img<>(img); +tel + +node main() returns (img, out : pixel; ck_out :bool; + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool) +let + (img, out, ck_out, y, y_dh, y_dh_t, y_dhv_t, ck_y_dh, ck_y_dhv) = mainp<<640,480>>(); +tel + diff --git a/test/good/foldi_arrays.ept b/test/good/foldi_arrays.ept new file mode 100644 index 0000000..1046546 --- /dev/null +++ b/test/good/foldi_arrays.ept @@ -0,0 +1,24 @@ + +type t = A | B | C + +const n:int = 10 + +type couple = { t1 : int^n; t2 : int^n } + +fun f (a:t;b:float;i:int;acc_in:couple) = (acc_out:couple) +let + switch a + | A do acc_out = { t1 = [ acc_in.t1 with [1] = acc_in.t1[1] + 1 ]; t2 = acc_in.t2 } + | B do acc_out = acc_in + | C do acc_out = { acc_in with .t2 = map<> (+)(acc_in.t1,acc_in.t2) } + end +tel + + +node main() returns (o:couple) +var a:t^n; b:float^n; +let + a = [A, B, C, A, B, C, A, B, C, A]; + b = 0.001^n; + o = foldi<> f (a, b, { t1 = 0^n; t2 = 0^n }); +tel diff --git a/test/good/mapnot.ept b/test/good/mapnot.ept new file mode 100644 index 0000000..cbf0724 --- /dev/null +++ b/test/good/mapnot.ept @@ -0,0 +1,15 @@ +type s = bool^10 +type t = { x : s } + +node g() returns (c : t) +var + b : s; +let + c = {x = false^10}; + b = map <<10>> (not) (true^10); +tel + +node main() returns (c:t) +let + c = g(); +tel diff --git a/test/good/pip.ept b/test/good/pip.ept new file mode 100644 index 0000000..c93f11b --- /dev/null +++ b/test/good/pip.ept @@ -0,0 +1,19 @@ +fun pip_line<> (line1 :int^m1; line2 :int^m2) returns (r :int^m1) +let + r = line1[0 .. y-1] @ line2 @ line1[y+m2 .. m1-1] +tel + +fun pip<> (t1 :int^n1^m1; t2 :int^n2^m2) returns (r :int^n1^m1) +var t12 :int^m1^n2; +let + t12 = map<> (pip_line<>) (t1[x..x+n2-1], t2); + r = t1[0 .. x-1] @ t12 @ t1[x+n2 .. n1-1]; +tel + +node main() returns (r :int^10^10) +var x,y:int; +let + x = 0 fby x+1; + y = x*x; + r = pip<<10,10,2,2,3,3>>(x^10^10,y^2^2); +tel diff --git a/test/good/pip_slice.ept b/test/good/pip_slice.ept new file mode 100644 index 0000000..c93f11b --- /dev/null +++ b/test/good/pip_slice.ept @@ -0,0 +1,19 @@ +fun pip_line<> (line1 :int^m1; line2 :int^m2) returns (r :int^m1) +let + r = line1[0 .. y-1] @ line2 @ line1[y+m2 .. m1-1] +tel + +fun pip<> (t1 :int^n1^m1; t2 :int^n2^m2) returns (r :int^n1^m1) +var t12 :int^m1^n2; +let + t12 = map<> (pip_line<>) (t1[x..x+n2-1], t2); + r = t1[0 .. x-1] @ t12 @ t1[x+n2 .. n1-1]; +tel + +node main() returns (r :int^10^10) +var x,y:int; +let + x = 0 fby x+1; + y = x*x; + r = pip<<10,10,2,2,3,3>>(x^10^10,y^2^2); +tel diff --git a/test/good/quasi.ept b/test/good/quasi.ept new file mode 100644 index 0000000..617ea7d --- /dev/null +++ b/test/good/quasi.ept @@ -0,0 +1,51 @@ +(* include "notsameperiod2.lus" *) + +type data = int + +const v:data = 0 + +node current (v : data; c : bool; u : data) +returns (o : data) +let + o = merge c u ((v fby o) whenot c) +tel + +node mem (v : data; cw : bool; u : data) +returns (o : data) +let + o = v fby (current (v, cw, u)) +tel + +node mcounter (start, limit : int) +returns (o : int) +let + o = (start -> (pre o + 1)) % limit; +tel + +node twonodes (cw, cr : bool) +returns (ok : bool) +var uw, ur : int; +let + uw = mcounter((0, 5) when cw); + ur = mem(v, cw, uw) when cr; + ok = (mem(v, cr, ur) = mem(v, cw, uw)) + or (mem(v, cr, ur)= mem(v, cw, v fby uw)) + or (mem(v, cr, ur) = mem(v, cw, v fby v fby uw)); +tel + +(* +node verify (cw, cr : bool) +returns (ok : bool) +let + ok = twonodes(cw, cr); + assert(not notsameperiod2(cw, cr)); +tel +*) + +node main() returns (ok:bool) + var cw, cr : bool; +let + cw = false fby not cw; + cr = not cw; + ok = twonodes(cw,cr); +tel From 2d96b60c49726c2c5c6bd44f811ac48b116eaa91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Mon, 27 Jan 2014 00:26:24 +0100 Subject: [PATCH 3/8] Bug corrections in contracts Contracts handling : added variables for assume/guarantee parts of subnodes as defined names in b_defnames --- .../heptagon/transformations/contracts.ml | 65 +++++++++++-------- 1 file changed, 39 insertions(+), 26 deletions(-) diff --git a/compiler/heptagon/transformations/contracts.ml b/compiler/heptagon/transformations/contracts.ml index 26bbc87..2016c6a 100644 --- a/compiler/heptagon/transformations/contracts.ml +++ b/compiler/heptagon/transformations/contracts.ml @@ -164,9 +164,11 @@ let mk_unique_contract nd = edesc = subst_edesc; } in fst (Hept_mapfold.node_dec funs () nd) -let exp funs (env, newvars, newequs, contracts) exp = - let exp, (env, newvars, newequs, contracts) = - Hept_mapfold.exp funs (env, newvars, newequs, contracts) exp in +let mk_vd_bool v = mk_var_dec ~last:(Last (Some (mk_static_bool true))) v tbool ~linearity:Ltop + +let exp funs (env, newvars, newequs, cont_vars, contracts) exp = + let exp, (env, newvars, newequs, cont_vars, contracts) = + Hept_mapfold.exp funs (env, newvars, newequs, cont_vars, contracts) exp in match exp.e_desc with | Eapp ({ a_op = (Enode nn | Efun nn); } as op, argl, rso) -> begin try @@ -219,17 +221,22 @@ let exp funs (env, newvars, newequs, contracts) exp = (* variables for assume and guarantee *) let v_a = fresh ((shortname nn) ^ "_assume") in let v_g = fresh ((shortname nn) ^ "_guarantee") in + (* variable declarations for assume/guarantee *) + let vd_a = mk_vd_bool v_a in + let vd_g = mk_vd_bool v_g in (* equations for assume/guarantee *) let eq_a = mk_equation (Eeq (Evarpat v_a, ci.c_assume)) in let eq_g = mk_equation (Eeq (Evarpat v_g, ci.c_enforce)) in + let newvars = ni.n_input @ ci.c_block.b_local @ ni.n_output @ newvars and newequs = List.map2 mk_input_equ ni.n_input argl @ List.map add_reset ci.c_block.b_equs @ [ eq_app; eq_a; eq_g ] @ newequs - and contracts = (v_a,v_g)::contracts in + and cont_vars = vd_a :: vd_g :: cont_vars + and contracts = (vd_a,vd_g)::contracts in (* For clocking reason we cannot create 1-tuples. *) let res_e = match ni.n_output with @@ -239,19 +246,27 @@ let exp funs (env, newvars, newequs, contracts) exp = List.map mk_output_exp ni.n_output, None)) exp.e_ty ~linearity:exp.e_linearity in - (res_e, (env, newvars, newequs, contracts)) + (res_e, (env, newvars, newequs, cont_vars, contracts)) with | Not_found -> - exp, (env, newvars, newequs, contracts) + exp, (env, newvars, newequs, cont_vars, contracts) end - | _ -> exp, (env, newvars, newequs, contracts) + | _ -> exp, (env, newvars, newequs, cont_vars, contracts) -let block funs (env, newvars, newequs, contracts) blk = - let (blk, (env, newvars', newequs', contracts')) = - Hept_mapfold.block funs (env, [], [], contracts) blk in - ({ blk with b_local = newvars' @ blk.b_local; b_equs = newequs' @ blk.b_equs; }, - (env, newvars, newequs, contracts')) +let block funs (env, newvars, newequs, cont_vars, contracts) blk = + let (blk, (env, newvars', newequs', cont_vars', contracts')) = + Hept_mapfold.block funs (env, [], [], [], contracts) blk in + (* let defnames = List.fold_left (fun env v -> Env.add v.v_ident v env) blk.b_defnames newvars' in *) + let defnames = List.fold_left + (fun env v -> Env.add v.v_ident v env) + blk.b_defnames cont_vars' in + ({ blk with + b_local = newvars' @ blk.b_local; + b_equs = newequs' @ blk.b_equs; + b_defnames = defnames; + }, + (env, newvars, newequs, (cont_vars @ cont_vars'), contracts')) let not_exp e = mk_exp (mk_op_app (Efun pnot) [e]) tbool ~linearity:Ltop @@ -264,11 +279,9 @@ let var_exp v = mk_exp (Evar v) tbool ~linearity:Ltop let true_exp = mk_exp (Econst (mk_static_bool true)) tbool ~linearity:Ltop -let mk_vd_bool v = mk_var_dec ~last:(Last (Some (mk_static_bool true))) v tbool ~linearity:Ltop - -let node_dec funs (env, newvars, newequs, contracts) nd = - let nd, (env, newvars, newequs, contracts) = - Hept_mapfold.node_dec funs (env, newvars, newequs, contracts) nd in +let node_dec funs (env, newvars, newequs, cont_vars, contracts) nd = + let nd, (env, newvars, newequs, cont_vars, contracts) = + Hept_mapfold.node_dec funs (env, newvars, newequs, cont_vars, contracts) nd in (* Build assume and guarantee parts from contract list (list of ident pairs (v_a,v_g)). Returns also a list of variable @@ -277,16 +290,16 @@ let node_dec funs (env, newvars, newequs, contracts) nd = match contracts with [] -> true_exp, true_exp, [] | [(v_a,v_g)] -> - let e_a = var_exp v_a in - let e_g = var_exp v_g in + let e_a = var_exp v_a.v_ident in + let e_g = var_exp v_g.v_ident in (* assume part : e_a => e_g ; guarantee part : e_a *) - (e_a => e_g), e_a, [mk_vd_bool v_a; mk_vd_bool v_g] + (e_a => e_g), e_a, [v_a; v_g] | (v_a,v_g)::l -> let e_a_l,e_g_l,vd_l = build_contract l in - let e_a = var_exp v_a in - let e_g = var_exp v_g in + let e_a = var_exp v_a.v_ident in + let e_g = var_exp v_g.v_ident in ((e_a => e_g) &&& e_a_l), (e_a &&& e_g_l), - ((mk_vd_bool v_a) :: (mk_vd_bool v_g) :: vd_l) + (v_a :: v_g :: vd_l) in let assume_loc, enforce_loc, vd_contracts = build_contract contracts in @@ -312,13 +325,13 @@ let node_dec funs (env, newvars, newequs, contracts) nd = b_local = newvars @ vd_contracts @ nd.n_block.b_local; b_equs = newequs @ nd.n_block.b_equs } } in let env = QualEnv.add nd.n_name nd env in - nd, (env, [], [], []) + nd, (env, [], [], [], []) let program p = let funs = { defaults with exp = exp; block = block; node_dec = node_dec; eq = eq; } in - let (p, (_, newvars, newequs, contracts)) = - Hept_mapfold.program funs (QualEnv.empty, [], [], []) p in + let (p, (_, newvars, newequs, cont_vars, contracts)) = + Hept_mapfold.program funs (QualEnv.empty, [], [], [], []) p in assert (newvars = []); assert (newequs = []); assert (contracts = []); From 9c4b3f326790cc9265acdc682a2ed0f23c1e71fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Tue, 28 Jan 2014 16:31:16 +0100 Subject: [PATCH 4/8] Version 1.00.05 --- CHANGES | 4 ++++ Makefile-distrib | 2 +- compiler/utilities/global/compiler_options.ml | 2 +- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 56ba9ef..d39f7f5 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,7 @@ +Heptagon 1.00.05 (28/01/2014) +----------------------------- + + - bug fix: correct handling of nodes with contracts inside automata and switches Heptagon 1.00.04 (14/01/2014) ----------------------------- diff --git a/Makefile-distrib b/Makefile-distrib index 7c78be6..b6bef16 100644 --- a/Makefile-distrib +++ b/Makefile-distrib @@ -2,7 +2,7 @@ include config #version = $(shell date +"%d%m%y") -version = 1.00.04 +version = 1.00.05 osname=$(shell uname -s) hardware=$(shell uname -m) heptdir = heptagon-$(version) diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 751d84d..be3f969 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -32,7 +32,7 @@ open Names (* version of the compiler *) -let version = "1.00.04" +let version = "1.00.05" let date = "DATE" (* standard module *) From e885f82e00d5ffd726695f5bd21461cd3a0af47c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Fri, 21 Feb 2014 17:39:37 +0100 Subject: [PATCH 5/8] Bug correction/feature adding: abstraction within contracts Allowing additional inputs from abstractions within contracts. Thus, calling non-inlined subnodes is allowed, as well as operations on non-Boolean inputs or states (in contracts). --- compiler/minils/sigali/sigalimain.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index c423a7d..fa135af 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -346,7 +346,7 @@ let translate_contract f contract = let body = [{ stmt_name = var_g; stmt_def = Sconst(Ctrue) }; { stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in - [],[],body,(Svar(var_a),Svar(var_g)),[],[],[] + [],[],[],body,(Svar(var_a),Svar(var_g)),[],[],[] | Some {Minils.c_local = locals; Minils.c_eq = l_eqs; Minils.c_assume = e_a; @@ -355,7 +355,6 @@ let translate_contract f contract = Minils.c_enforce_loc = e_g_loc; Minils.c_controllables = cl} -> let states,init,inputs,body = translate_eq_list f l_eqs in - assert (inputs = []); let e_a = translate_ext prefix e_a in let e_g = translate_ext prefix e_g in let e_a_loc = translate_ext prefix e_a_loc in @@ -367,7 +366,7 @@ let translate_contract f contract = let controllables = List.map (fun ({ Minils.v_ident = id } as v) -> v,(prefix ^ (name id))) cl in - states,init,body,(Svar(var_a),Svar(var_g)),controllables,(locals@cl),l_eqs + states,init,inputs,body,(Svar(var_a),Svar(var_g)),controllables,(locals@cl),l_eqs @@ -395,9 +394,9 @@ let translate_node (fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in let states,init,add_inputs,body = translate_eq_list f eq_list in - let states_c,init_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c = + let states_c,init_c,inputs_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c = translate_contract f contract in - let inputs = inputs @ add_inputs in + let inputs = inputs @ add_inputs @ inputs_c in let body = List.rev body in let states = List.rev states in let body_c = List.rev body_c in From bcba3569edaa5a4caabc2fdbb14b65c7238f2f78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Fri, 21 Feb 2014 17:45:10 +0100 Subject: [PATCH 6/8] Added tests - types, constants, contracts - ais.ept: tests inclusion of array types into structure types - ce.ept: constant propagation - contract.ept: contract constructs - contract_automaton.ept: contract constructs and automata --- test/CTestTestfile.cmake | 121 +++++++++++++++++++++++++++++++ test/good/ais.ept | 8 ++ test/good/ce.ept | 3 + test/good/contract.ept | 41 +++++++++++ test/good/contract_automaton.ept | 50 +++++++++++++ test/good/tuple_args.ept | 0 6 files changed, 223 insertions(+) create mode 100644 test/good/ais.ept create mode 100644 test/good/ce.ept create mode 100644 test/good/contract.ept create mode 100644 test/good/contract_automaton.ept mode change 100755 => 100644 test/good/tuple_args.ept diff --git a/test/CTestTestfile.cmake b/test/CTestTestfile.cmake index 3e62d72..5ef3706 100644 --- a/test/CTestTestfile.cmake +++ b/test/CTestTestfile.cmake @@ -30,6 +30,7 @@ ADD_TEST(compile_fail_t7 "scripts/compile_fail" "bad/t7.ept" "-memalloc") ADD_TEST(compile_fail_t8-causality "scripts/compile_fail" "bad/t8-causality.ept" "-memalloc") ADD_TEST(compile_fail_t9-initialization "scripts/compile_fail" "bad/t9-initialization.ept" "-memalloc") ADD_TEST(compile_fail_when_merge1 "scripts/compile_fail" "bad/when_merge1.ept" "-memalloc") +ADD_TEST(compile_only_ais "scripts/compile_only" "good/ais.ept") ADD_TEST(compile_only_alloc "scripts/compile_only" "good/alloc.ept") ADD_TEST(compile_only_array1 "scripts/compile_only" "good/array1.ept") ADD_TEST(compile_only_array2 "scripts/compile_only" "good/array2.ept") @@ -42,12 +43,18 @@ ADD_TEST(compile_only_auto "scripts/compile_only" "good/auto.ept") ADD_TEST(compile_only_autohiera2 "scripts/compile_only" "good/autohiera2.ept") ADD_TEST(compile_only_autohiera "scripts/compile_only" "good/autohiera.ept") ADD_TEST(compile_only_bad_updown "scripts/compile_only" "good/bad_updown.ept") +ADD_TEST(compile_only_ce "scripts/compile_only" "good/ce.ept") ADD_TEST(compile_only_ckannot "scripts/compile_only" "good/ckannot.ept") ADD_TEST(compile_only_clock_causality "scripts/compile_only" "good/clock_causality.ept") ADD_TEST(compile_only_clocks "scripts/compile_only" "good/clocks.ept") +ADD_TEST(compile_only_contract_automaton "scripts/compile_only" "good/contract_automaton.ept") +ADD_TEST(compile_only_contract "scripts/compile_only" "good/contract.ept") +ADD_TEST(compile_only_convolutions "scripts/compile_only" "good/convolutions.ept") ADD_TEST(compile_only_counter "scripts/compile_only" "good/counter.ept") ADD_TEST(compile_only_current "scripts/compile_only" "good/current.ept") +ADD_TEST(compile_only_downscale "scripts/compile_only" "good/downscale.ept") ADD_TEST(compile_only_fbyfby2 "scripts/compile_only" "good/fbyfby2.ept") +ADD_TEST(compile_only_foldi_arrays "scripts/compile_only" "good/foldi_arrays.ept") ADD_TEST(compile_only_foldi "scripts/compile_only" "good/foldi.ept") ADD_TEST(compile_only_format "scripts/compile_only" "good/format.ept") ADD_TEST(compile_only_grosauto_clock "scripts/compile_only" "good/grosauto_clock.ept") @@ -58,6 +65,7 @@ ADD_TEST(compile_only_linear "scripts/compile_only" "good/linear.ept") ADD_TEST(compile_only_linear_init "scripts/compile_only" "good/linear_init.ept") ADD_TEST(compile_only_linear_split "scripts/compile_only" "good/linear_split.ept") ADD_TEST(compile_only_linear_vars "scripts/compile_only" "good/linear_vars.ept") +ADD_TEST(compile_only_mapnot "scripts/compile_only" "good/mapnot.ept") ADD_TEST(compile_only_memalloc_clocks "scripts/compile_only" "good/memalloc_clocks.ept") ADD_TEST(compile_only_memalloc_record "scripts/compile_only" "good/memalloc_record.ept") ADD_TEST(compile_only_memalloc_simple "scripts/compile_only" "good/memalloc_simple.ept") @@ -65,7 +73,10 @@ ADD_TEST(compile_only_name_clash "scripts/compile_only" "good/name_clash.ept") ADD_TEST(compile_only_norm "scripts/compile_only" "good/norm.ept") ADD_TEST(compile_only_or_keep "scripts/compile_only" "good/or_keep.ept") ADD_TEST(compile_only_parametrize "scripts/compile_only" "good/parametrize.ept") +ADD_TEST(compile_only_pip "scripts/compile_only" "good/pip.ept") +ADD_TEST(compile_only_pip_slice "scripts/compile_only" "good/pip_slice.ept") ADD_TEST(compile_only_pre_tuple "scripts/compile_only" "good/pre_tuple.ept") +ADD_TEST(compile_only_quasi "scripts/compile_only" "good/quasi.ept") ADD_TEST(compile_only_reinit "scripts/compile_only" "good/reinit.ept") ADD_TEST(compile_only_sampling_stateful_output2 "scripts/compile_only" "good/sampling_stateful_output2.ept") ADD_TEST(compile_only_sampling_stateful_output "scripts/compile_only" "good/sampling_stateful_output.ept") @@ -102,6 +113,7 @@ ADD_TEST(compile_only_tuple_args "scripts/compile_only" "good/tuple_args.ept") ADD_TEST(compile_only_type_alias "scripts/compile_only" "good/type_alias.ept") ADD_TEST(compile_only_updown "scripts/compile_only" "good/updown.ept") ADD_TEST(compile_only_when_merge1 "scripts/compile_only" "good/when_merge1.ept") +ADD_TEST(compile_gcc_run_ais "scripts/compile_gcc_run" "good/ais.ept") ADD_TEST(compile_gcc_run_alloc "scripts/compile_gcc_run" "good/alloc.ept") ADD_TEST(compile_gcc_run_array1 "scripts/compile_gcc_run" "good/array1.ept") ADD_TEST(compile_gcc_run_array2 "scripts/compile_gcc_run" "good/array2.ept") @@ -114,12 +126,18 @@ ADD_TEST(compile_gcc_run_auto "scripts/compile_gcc_run" "good/auto.ept") ADD_TEST(compile_gcc_run_autohiera2 "scripts/compile_gcc_run" "good/autohiera2.ept") ADD_TEST(compile_gcc_run_autohiera "scripts/compile_gcc_run" "good/autohiera.ept") ADD_TEST(compile_gcc_run_bad_updown "scripts/compile_gcc_run" "good/bad_updown.ept") +ADD_TEST(compile_gcc_run_ce "scripts/compile_gcc_run" "good/ce.ept") ADD_TEST(compile_gcc_run_ckannot "scripts/compile_gcc_run" "good/ckannot.ept") ADD_TEST(compile_gcc_run_clock_causality "scripts/compile_gcc_run" "good/clock_causality.ept") ADD_TEST(compile_gcc_run_clocks "scripts/compile_gcc_run" "good/clocks.ept") +ADD_TEST(compile_gcc_run_contract_automaton "scripts/compile_gcc_run" "good/contract_automaton.ept") +ADD_TEST(compile_gcc_run_contract "scripts/compile_gcc_run" "good/contract.ept") +ADD_TEST(compile_gcc_run_convolutions "scripts/compile_gcc_run" "good/convolutions.ept") ADD_TEST(compile_gcc_run_counter "scripts/compile_gcc_run" "good/counter.ept") ADD_TEST(compile_gcc_run_current "scripts/compile_gcc_run" "good/current.ept") +ADD_TEST(compile_gcc_run_downscale "scripts/compile_gcc_run" "good/downscale.ept") ADD_TEST(compile_gcc_run_fbyfby2 "scripts/compile_gcc_run" "good/fbyfby2.ept") +ADD_TEST(compile_gcc_run_foldi_arrays "scripts/compile_gcc_run" "good/foldi_arrays.ept") ADD_TEST(compile_gcc_run_foldi "scripts/compile_gcc_run" "good/foldi.ept") ADD_TEST(compile_gcc_run_format "scripts/compile_gcc_run" "good/format.ept") ADD_TEST(compile_gcc_run_grosauto_clock "scripts/compile_gcc_run" "good/grosauto_clock.ept") @@ -130,6 +148,7 @@ ADD_TEST(compile_gcc_run_linear "scripts/compile_gcc_run" "good/linear.ept") ADD_TEST(compile_gcc_run_linear_init "scripts/compile_gcc_run" "good/linear_init.ept") ADD_TEST(compile_gcc_run_linear_split "scripts/compile_gcc_run" "good/linear_split.ept") ADD_TEST(compile_gcc_run_linear_vars "scripts/compile_gcc_run" "good/linear_vars.ept") +ADD_TEST(compile_gcc_run_mapnot "scripts/compile_gcc_run" "good/mapnot.ept") ADD_TEST(compile_gcc_run_memalloc_clocks "scripts/compile_gcc_run" "good/memalloc_clocks.ept") ADD_TEST(compile_gcc_run_memalloc_record "scripts/compile_gcc_run" "good/memalloc_record.ept") ADD_TEST(compile_gcc_run_memalloc_simple "scripts/compile_gcc_run" "good/memalloc_simple.ept") @@ -137,7 +156,10 @@ ADD_TEST(compile_gcc_run_name_clash "scripts/compile_gcc_run" "good/name_clash.e ADD_TEST(compile_gcc_run_norm "scripts/compile_gcc_run" "good/norm.ept") ADD_TEST(compile_gcc_run_or_keep "scripts/compile_gcc_run" "good/or_keep.ept") ADD_TEST(compile_gcc_run_parametrize "scripts/compile_gcc_run" "good/parametrize.ept") +ADD_TEST(compile_gcc_run_pip "scripts/compile_gcc_run" "good/pip.ept") +ADD_TEST(compile_gcc_run_pip_slice "scripts/compile_gcc_run" "good/pip_slice.ept") ADD_TEST(compile_gcc_run_pre_tuple "scripts/compile_gcc_run" "good/pre_tuple.ept") +ADD_TEST(compile_gcc_run_quasi "scripts/compile_gcc_run" "good/quasi.ept") ADD_TEST(compile_gcc_run_reinit "scripts/compile_gcc_run" "good/reinit.ept") ADD_TEST(compile_gcc_run_sampling_stateful_output2 "scripts/compile_gcc_run" "good/sampling_stateful_output2.ept") ADD_TEST(compile_gcc_run_sampling_stateful_output "scripts/compile_gcc_run" "good/sampling_stateful_output.ept") @@ -174,6 +196,7 @@ ADD_TEST(compile_gcc_run_tuple_args "scripts/compile_gcc_run" "good/tuple_args.e ADD_TEST(compile_gcc_run_type_alias "scripts/compile_gcc_run" "good/type_alias.ept") ADD_TEST(compile_gcc_run_updown "scripts/compile_gcc_run" "good/updown.ept") ADD_TEST(compile_gcc_run_when_merge1 "scripts/compile_gcc_run" "good/when_merge1.ept") +ADD_TEST(test_option_bool_ais "scripts/test_option" "good/ais.ept" "-bool") ADD_TEST(test_option_bool_alloc "scripts/test_option" "good/alloc.ept" "-bool") ADD_TEST(test_option_bool_array1 "scripts/test_option" "good/array1.ept" "-bool") ADD_TEST(test_option_bool_array2 "scripts/test_option" "good/array2.ept" "-bool") @@ -186,12 +209,18 @@ ADD_TEST(test_option_bool_auto "scripts/test_option" "good/auto.ept" "-bool") ADD_TEST(test_option_bool_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-bool") ADD_TEST(test_option_bool_autohiera "scripts/test_option" "good/autohiera.ept" "-bool") ADD_TEST(test_option_bool_bad_updown "scripts/test_option" "good/bad_updown.ept" "-bool") +ADD_TEST(test_option_bool_ce "scripts/test_option" "good/ce.ept" "-bool") ADD_TEST(test_option_bool_ckannot "scripts/test_option" "good/ckannot.ept" "-bool") ADD_TEST(test_option_bool_clock_causality "scripts/test_option" "good/clock_causality.ept" "-bool") ADD_TEST(test_option_bool_clocks "scripts/test_option" "good/clocks.ept" "-bool") +ADD_TEST(test_option_bool_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-bool") +ADD_TEST(test_option_bool_contract "scripts/test_option" "good/contract.ept" "-bool") +ADD_TEST(test_option_bool_convolutions "scripts/test_option" "good/convolutions.ept" "-bool") ADD_TEST(test_option_bool_counter "scripts/test_option" "good/counter.ept" "-bool") ADD_TEST(test_option_bool_current "scripts/test_option" "good/current.ept" "-bool") +ADD_TEST(test_option_bool_downscale "scripts/test_option" "good/downscale.ept" "-bool") ADD_TEST(test_option_bool_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-bool") +ADD_TEST(test_option_bool_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-bool") ADD_TEST(test_option_bool_foldi "scripts/test_option" "good/foldi.ept" "-bool") ADD_TEST(test_option_bool_format "scripts/test_option" "good/format.ept" "-bool") ADD_TEST(test_option_bool_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-bool") @@ -202,6 +231,7 @@ ADD_TEST(test_option_bool_linear "scripts/test_option" "good/linear.ept" "-bool" ADD_TEST(test_option_bool_linear_init "scripts/test_option" "good/linear_init.ept" "-bool") ADD_TEST(test_option_bool_linear_split "scripts/test_option" "good/linear_split.ept" "-bool") ADD_TEST(test_option_bool_linear_vars "scripts/test_option" "good/linear_vars.ept" "-bool") +ADD_TEST(test_option_bool_mapnot "scripts/test_option" "good/mapnot.ept" "-bool") ADD_TEST(test_option_bool_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-bool") ADD_TEST(test_option_bool_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-bool") ADD_TEST(test_option_bool_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-bool") @@ -209,7 +239,10 @@ ADD_TEST(test_option_bool_name_clash "scripts/test_option" "good/name_clash.ept" ADD_TEST(test_option_bool_norm "scripts/test_option" "good/norm.ept" "-bool") ADD_TEST(test_option_bool_or_keep "scripts/test_option" "good/or_keep.ept" "-bool") ADD_TEST(test_option_bool_parametrize "scripts/test_option" "good/parametrize.ept" "-bool") +ADD_TEST(test_option_bool_pip "scripts/test_option" "good/pip.ept" "-bool") +ADD_TEST(test_option_bool_pip_slice "scripts/test_option" "good/pip_slice.ept" "-bool") ADD_TEST(test_option_bool_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-bool") +ADD_TEST(test_option_bool_quasi "scripts/test_option" "good/quasi.ept" "-bool") ADD_TEST(test_option_bool_reinit "scripts/test_option" "good/reinit.ept" "-bool") ADD_TEST(test_option_bool_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-bool") ADD_TEST(test_option_bool_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-bool") @@ -246,6 +279,7 @@ ADD_TEST(test_option_bool_tuple_args "scripts/test_option" "good/tuple_args.ept" ADD_TEST(test_option_bool_type_alias "scripts/test_option" "good/type_alias.ept" "-bool") ADD_TEST(test_option_bool_updown "scripts/test_option" "good/updown.ept" "-bool") ADD_TEST(test_option_bool_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-bool") +ADD_TEST(test_option_deadcode_ais "scripts/test_option" "good/ais.ept" "-deadcode") ADD_TEST(test_option_deadcode_alloc "scripts/test_option" "good/alloc.ept" "-deadcode") ADD_TEST(test_option_deadcode_array1 "scripts/test_option" "good/array1.ept" "-deadcode") ADD_TEST(test_option_deadcode_array2 "scripts/test_option" "good/array2.ept" "-deadcode") @@ -258,12 +292,18 @@ ADD_TEST(test_option_deadcode_auto "scripts/test_option" "good/auto.ept" "-deadc ADD_TEST(test_option_deadcode_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-deadcode") ADD_TEST(test_option_deadcode_autohiera "scripts/test_option" "good/autohiera.ept" "-deadcode") ADD_TEST(test_option_deadcode_bad_updown "scripts/test_option" "good/bad_updown.ept" "-deadcode") +ADD_TEST(test_option_deadcode_ce "scripts/test_option" "good/ce.ept" "-deadcode") ADD_TEST(test_option_deadcode_ckannot "scripts/test_option" "good/ckannot.ept" "-deadcode") ADD_TEST(test_option_deadcode_clock_causality "scripts/test_option" "good/clock_causality.ept" "-deadcode") ADD_TEST(test_option_deadcode_clocks "scripts/test_option" "good/clocks.ept" "-deadcode") +ADD_TEST(test_option_deadcode_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-deadcode") +ADD_TEST(test_option_deadcode_contract "scripts/test_option" "good/contract.ept" "-deadcode") +ADD_TEST(test_option_deadcode_convolutions "scripts/test_option" "good/convolutions.ept" "-deadcode") ADD_TEST(test_option_deadcode_counter "scripts/test_option" "good/counter.ept" "-deadcode") ADD_TEST(test_option_deadcode_current "scripts/test_option" "good/current.ept" "-deadcode") +ADD_TEST(test_option_deadcode_downscale "scripts/test_option" "good/downscale.ept" "-deadcode") ADD_TEST(test_option_deadcode_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-deadcode") +ADD_TEST(test_option_deadcode_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-deadcode") ADD_TEST(test_option_deadcode_foldi "scripts/test_option" "good/foldi.ept" "-deadcode") ADD_TEST(test_option_deadcode_format "scripts/test_option" "good/format.ept" "-deadcode") ADD_TEST(test_option_deadcode_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-deadcode") @@ -274,6 +314,7 @@ ADD_TEST(test_option_deadcode_linear "scripts/test_option" "good/linear.ept" "-d ADD_TEST(test_option_deadcode_linear_init "scripts/test_option" "good/linear_init.ept" "-deadcode") ADD_TEST(test_option_deadcode_linear_split "scripts/test_option" "good/linear_split.ept" "-deadcode") ADD_TEST(test_option_deadcode_linear_vars "scripts/test_option" "good/linear_vars.ept" "-deadcode") +ADD_TEST(test_option_deadcode_mapnot "scripts/test_option" "good/mapnot.ept" "-deadcode") ADD_TEST(test_option_deadcode_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-deadcode") ADD_TEST(test_option_deadcode_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-deadcode") ADD_TEST(test_option_deadcode_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-deadcode") @@ -281,7 +322,10 @@ ADD_TEST(test_option_deadcode_name_clash "scripts/test_option" "good/name_clash. ADD_TEST(test_option_deadcode_norm "scripts/test_option" "good/norm.ept" "-deadcode") ADD_TEST(test_option_deadcode_or_keep "scripts/test_option" "good/or_keep.ept" "-deadcode") ADD_TEST(test_option_deadcode_parametrize "scripts/test_option" "good/parametrize.ept" "-deadcode") +ADD_TEST(test_option_deadcode_pip "scripts/test_option" "good/pip.ept" "-deadcode") +ADD_TEST(test_option_deadcode_pip_slice "scripts/test_option" "good/pip_slice.ept" "-deadcode") ADD_TEST(test_option_deadcode_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-deadcode") +ADD_TEST(test_option_deadcode_quasi "scripts/test_option" "good/quasi.ept" "-deadcode") ADD_TEST(test_option_deadcode_reinit "scripts/test_option" "good/reinit.ept" "-deadcode") ADD_TEST(test_option_deadcode_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-deadcode") ADD_TEST(test_option_deadcode_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-deadcode") @@ -318,6 +362,7 @@ ADD_TEST(test_option_deadcode_tuple_args "scripts/test_option" "good/tuple_args. ADD_TEST(test_option_deadcode_type_alias "scripts/test_option" "good/type_alias.ept" "-deadcode") ADD_TEST(test_option_deadcode_updown "scripts/test_option" "good/updown.ept" "-deadcode") ADD_TEST(test_option_deadcode_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-deadcode") +ADD_TEST(test_option_tomato_ais "scripts/test_option" "good/ais.ept" "-tomato") ADD_TEST(test_option_tomato_alloc "scripts/test_option" "good/alloc.ept" "-tomato") ADD_TEST(test_option_tomato_array1 "scripts/test_option" "good/array1.ept" "-tomato") ADD_TEST(test_option_tomato_array2 "scripts/test_option" "good/array2.ept" "-tomato") @@ -330,12 +375,18 @@ ADD_TEST(test_option_tomato_auto "scripts/test_option" "good/auto.ept" "-tomato" ADD_TEST(test_option_tomato_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-tomato") ADD_TEST(test_option_tomato_autohiera "scripts/test_option" "good/autohiera.ept" "-tomato") ADD_TEST(test_option_tomato_bad_updown "scripts/test_option" "good/bad_updown.ept" "-tomato") +ADD_TEST(test_option_tomato_ce "scripts/test_option" "good/ce.ept" "-tomato") ADD_TEST(test_option_tomato_ckannot "scripts/test_option" "good/ckannot.ept" "-tomato") ADD_TEST(test_option_tomato_clock_causality "scripts/test_option" "good/clock_causality.ept" "-tomato") ADD_TEST(test_option_tomato_clocks "scripts/test_option" "good/clocks.ept" "-tomato") +ADD_TEST(test_option_tomato_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-tomato") +ADD_TEST(test_option_tomato_contract "scripts/test_option" "good/contract.ept" "-tomato") +ADD_TEST(test_option_tomato_convolutions "scripts/test_option" "good/convolutions.ept" "-tomato") ADD_TEST(test_option_tomato_counter "scripts/test_option" "good/counter.ept" "-tomato") ADD_TEST(test_option_tomato_current "scripts/test_option" "good/current.ept" "-tomato") +ADD_TEST(test_option_tomato_downscale "scripts/test_option" "good/downscale.ept" "-tomato") ADD_TEST(test_option_tomato_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-tomato") +ADD_TEST(test_option_tomato_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-tomato") ADD_TEST(test_option_tomato_foldi "scripts/test_option" "good/foldi.ept" "-tomato") ADD_TEST(test_option_tomato_format "scripts/test_option" "good/format.ept" "-tomato") ADD_TEST(test_option_tomato_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-tomato") @@ -346,6 +397,7 @@ ADD_TEST(test_option_tomato_linear "scripts/test_option" "good/linear.ept" "-tom ADD_TEST(test_option_tomato_linear_init "scripts/test_option" "good/linear_init.ept" "-tomato") ADD_TEST(test_option_tomato_linear_split "scripts/test_option" "good/linear_split.ept" "-tomato") ADD_TEST(test_option_tomato_linear_vars "scripts/test_option" "good/linear_vars.ept" "-tomato") +ADD_TEST(test_option_tomato_mapnot "scripts/test_option" "good/mapnot.ept" "-tomato") ADD_TEST(test_option_tomato_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-tomato") ADD_TEST(test_option_tomato_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-tomato") ADD_TEST(test_option_tomato_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-tomato") @@ -353,7 +405,10 @@ ADD_TEST(test_option_tomato_name_clash "scripts/test_option" "good/name_clash.ep ADD_TEST(test_option_tomato_norm "scripts/test_option" "good/norm.ept" "-tomato") ADD_TEST(test_option_tomato_or_keep "scripts/test_option" "good/or_keep.ept" "-tomato") ADD_TEST(test_option_tomato_parametrize "scripts/test_option" "good/parametrize.ept" "-tomato") +ADD_TEST(test_option_tomato_pip "scripts/test_option" "good/pip.ept" "-tomato") +ADD_TEST(test_option_tomato_pip_slice "scripts/test_option" "good/pip_slice.ept" "-tomato") ADD_TEST(test_option_tomato_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-tomato") +ADD_TEST(test_option_tomato_quasi "scripts/test_option" "good/quasi.ept" "-tomato") ADD_TEST(test_option_tomato_reinit "scripts/test_option" "good/reinit.ept" "-tomato") ADD_TEST(test_option_tomato_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-tomato") ADD_TEST(test_option_tomato_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-tomato") @@ -390,6 +445,7 @@ ADD_TEST(test_option_tomato_tuple_args "scripts/test_option" "good/tuple_args.ep ADD_TEST(test_option_tomato_type_alias "scripts/test_option" "good/type_alias.ept" "-tomato") ADD_TEST(test_option_tomato_updown "scripts/test_option" "good/updown.ept" "-tomato") ADD_TEST(test_option_tomato_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-tomato") +ADD_TEST(test_option_flatten_ais "scripts/test_option" "good/ais.ept" "-flatten") ADD_TEST(test_option_flatten_alloc "scripts/test_option" "good/alloc.ept" "-flatten") ADD_TEST(test_option_flatten_array1 "scripts/test_option" "good/array1.ept" "-flatten") ADD_TEST(test_option_flatten_array2 "scripts/test_option" "good/array2.ept" "-flatten") @@ -402,12 +458,18 @@ ADD_TEST(test_option_flatten_auto "scripts/test_option" "good/auto.ept" "-flatte ADD_TEST(test_option_flatten_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-flatten") ADD_TEST(test_option_flatten_autohiera "scripts/test_option" "good/autohiera.ept" "-flatten") ADD_TEST(test_option_flatten_bad_updown "scripts/test_option" "good/bad_updown.ept" "-flatten") +ADD_TEST(test_option_flatten_ce "scripts/test_option" "good/ce.ept" "-flatten") ADD_TEST(test_option_flatten_ckannot "scripts/test_option" "good/ckannot.ept" "-flatten") ADD_TEST(test_option_flatten_clock_causality "scripts/test_option" "good/clock_causality.ept" "-flatten") ADD_TEST(test_option_flatten_clocks "scripts/test_option" "good/clocks.ept" "-flatten") +ADD_TEST(test_option_flatten_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-flatten") +ADD_TEST(test_option_flatten_contract "scripts/test_option" "good/contract.ept" "-flatten") +ADD_TEST(test_option_flatten_convolutions "scripts/test_option" "good/convolutions.ept" "-flatten") ADD_TEST(test_option_flatten_counter "scripts/test_option" "good/counter.ept" "-flatten") ADD_TEST(test_option_flatten_current "scripts/test_option" "good/current.ept" "-flatten") +ADD_TEST(test_option_flatten_downscale "scripts/test_option" "good/downscale.ept" "-flatten") ADD_TEST(test_option_flatten_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-flatten") +ADD_TEST(test_option_flatten_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-flatten") ADD_TEST(test_option_flatten_foldi "scripts/test_option" "good/foldi.ept" "-flatten") ADD_TEST(test_option_flatten_format "scripts/test_option" "good/format.ept" "-flatten") ADD_TEST(test_option_flatten_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-flatten") @@ -418,6 +480,7 @@ ADD_TEST(test_option_flatten_linear "scripts/test_option" "good/linear.ept" "-fl ADD_TEST(test_option_flatten_linear_init "scripts/test_option" "good/linear_init.ept" "-flatten") ADD_TEST(test_option_flatten_linear_split "scripts/test_option" "good/linear_split.ept" "-flatten") ADD_TEST(test_option_flatten_linear_vars "scripts/test_option" "good/linear_vars.ept" "-flatten") +ADD_TEST(test_option_flatten_mapnot "scripts/test_option" "good/mapnot.ept" "-flatten") ADD_TEST(test_option_flatten_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-flatten") ADD_TEST(test_option_flatten_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-flatten") ADD_TEST(test_option_flatten_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-flatten") @@ -425,7 +488,10 @@ ADD_TEST(test_option_flatten_name_clash "scripts/test_option" "good/name_clash.e ADD_TEST(test_option_flatten_norm "scripts/test_option" "good/norm.ept" "-flatten") ADD_TEST(test_option_flatten_or_keep "scripts/test_option" "good/or_keep.ept" "-flatten") ADD_TEST(test_option_flatten_parametrize "scripts/test_option" "good/parametrize.ept" "-flatten") +ADD_TEST(test_option_flatten_pip "scripts/test_option" "good/pip.ept" "-flatten") +ADD_TEST(test_option_flatten_pip_slice "scripts/test_option" "good/pip_slice.ept" "-flatten") ADD_TEST(test_option_flatten_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-flatten") +ADD_TEST(test_option_flatten_quasi "scripts/test_option" "good/quasi.ept" "-flatten") ADD_TEST(test_option_flatten_reinit "scripts/test_option" "good/reinit.ept" "-flatten") ADD_TEST(test_option_flatten_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-flatten") ADD_TEST(test_option_flatten_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-flatten") @@ -462,6 +528,7 @@ ADD_TEST(test_option_flatten_tuple_args "scripts/test_option" "good/tuple_args.e ADD_TEST(test_option_flatten_type_alias "scripts/test_option" "good/type_alias.ept" "-flatten") ADD_TEST(test_option_flatten_updown "scripts/test_option" "good/updown.ept" "-flatten") ADD_TEST(test_option_flatten_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-flatten") +ADD_TEST(test_option_itfusion_ais "scripts/test_option" "good/ais.ept" "-itfusion") ADD_TEST(test_option_itfusion_alloc "scripts/test_option" "good/alloc.ept" "-itfusion") ADD_TEST(test_option_itfusion_array1 "scripts/test_option" "good/array1.ept" "-itfusion") ADD_TEST(test_option_itfusion_array2 "scripts/test_option" "good/array2.ept" "-itfusion") @@ -474,12 +541,18 @@ ADD_TEST(test_option_itfusion_auto "scripts/test_option" "good/auto.ept" "-itfus ADD_TEST(test_option_itfusion_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-itfusion") ADD_TEST(test_option_itfusion_autohiera "scripts/test_option" "good/autohiera.ept" "-itfusion") ADD_TEST(test_option_itfusion_bad_updown "scripts/test_option" "good/bad_updown.ept" "-itfusion") +ADD_TEST(test_option_itfusion_ce "scripts/test_option" "good/ce.ept" "-itfusion") ADD_TEST(test_option_itfusion_ckannot "scripts/test_option" "good/ckannot.ept" "-itfusion") ADD_TEST(test_option_itfusion_clock_causality "scripts/test_option" "good/clock_causality.ept" "-itfusion") ADD_TEST(test_option_itfusion_clocks "scripts/test_option" "good/clocks.ept" "-itfusion") +ADD_TEST(test_option_itfusion_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-itfusion") +ADD_TEST(test_option_itfusion_contract "scripts/test_option" "good/contract.ept" "-itfusion") +ADD_TEST(test_option_itfusion_convolutions "scripts/test_option" "good/convolutions.ept" "-itfusion") ADD_TEST(test_option_itfusion_counter "scripts/test_option" "good/counter.ept" "-itfusion") ADD_TEST(test_option_itfusion_current "scripts/test_option" "good/current.ept" "-itfusion") +ADD_TEST(test_option_itfusion_downscale "scripts/test_option" "good/downscale.ept" "-itfusion") ADD_TEST(test_option_itfusion_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-itfusion") +ADD_TEST(test_option_itfusion_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-itfusion") ADD_TEST(test_option_itfusion_foldi "scripts/test_option" "good/foldi.ept" "-itfusion") ADD_TEST(test_option_itfusion_format "scripts/test_option" "good/format.ept" "-itfusion") ADD_TEST(test_option_itfusion_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-itfusion") @@ -490,6 +563,7 @@ ADD_TEST(test_option_itfusion_linear "scripts/test_option" "good/linear.ept" "-i ADD_TEST(test_option_itfusion_linear_init "scripts/test_option" "good/linear_init.ept" "-itfusion") ADD_TEST(test_option_itfusion_linear_split "scripts/test_option" "good/linear_split.ept" "-itfusion") ADD_TEST(test_option_itfusion_linear_vars "scripts/test_option" "good/linear_vars.ept" "-itfusion") +ADD_TEST(test_option_itfusion_mapnot "scripts/test_option" "good/mapnot.ept" "-itfusion") ADD_TEST(test_option_itfusion_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-itfusion") ADD_TEST(test_option_itfusion_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-itfusion") ADD_TEST(test_option_itfusion_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-itfusion") @@ -497,7 +571,10 @@ ADD_TEST(test_option_itfusion_name_clash "scripts/test_option" "good/name_clash. ADD_TEST(test_option_itfusion_norm "scripts/test_option" "good/norm.ept" "-itfusion") ADD_TEST(test_option_itfusion_or_keep "scripts/test_option" "good/or_keep.ept" "-itfusion") ADD_TEST(test_option_itfusion_parametrize "scripts/test_option" "good/parametrize.ept" "-itfusion") +ADD_TEST(test_option_itfusion_pip "scripts/test_option" "good/pip.ept" "-itfusion") +ADD_TEST(test_option_itfusion_pip_slice "scripts/test_option" "good/pip_slice.ept" "-itfusion") ADD_TEST(test_option_itfusion_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-itfusion") +ADD_TEST(test_option_itfusion_quasi "scripts/test_option" "good/quasi.ept" "-itfusion") ADD_TEST(test_option_itfusion_reinit "scripts/test_option" "good/reinit.ept" "-itfusion") ADD_TEST(test_option_itfusion_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-itfusion") ADD_TEST(test_option_itfusion_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-itfusion") @@ -534,6 +611,7 @@ ADD_TEST(test_option_itfusion_tuple_args "scripts/test_option" "good/tuple_args. ADD_TEST(test_option_itfusion_type_alias "scripts/test_option" "good/type_alias.ept" "-itfusion") ADD_TEST(test_option_itfusion_updown "scripts/test_option" "good/updown.ept" "-itfusion") ADD_TEST(test_option_itfusion_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-itfusion") +ADD_TEST(test_option_memalloc_ais "scripts/test_option" "good/ais.ept" "-memalloc") ADD_TEST(test_option_memalloc_alloc "scripts/test_option" "good/alloc.ept" "-memalloc") ADD_TEST(test_option_memalloc_array1 "scripts/test_option" "good/array1.ept" "-memalloc") ADD_TEST(test_option_memalloc_array2 "scripts/test_option" "good/array2.ept" "-memalloc") @@ -546,12 +624,18 @@ ADD_TEST(test_option_memalloc_auto "scripts/test_option" "good/auto.ept" "-memal ADD_TEST(test_option_memalloc_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-memalloc") ADD_TEST(test_option_memalloc_autohiera "scripts/test_option" "good/autohiera.ept" "-memalloc") ADD_TEST(test_option_memalloc_bad_updown "scripts/test_option" "good/bad_updown.ept" "-memalloc") +ADD_TEST(test_option_memalloc_ce "scripts/test_option" "good/ce.ept" "-memalloc") ADD_TEST(test_option_memalloc_ckannot "scripts/test_option" "good/ckannot.ept" "-memalloc") ADD_TEST(test_option_memalloc_clock_causality "scripts/test_option" "good/clock_causality.ept" "-memalloc") ADD_TEST(test_option_memalloc_clocks "scripts/test_option" "good/clocks.ept" "-memalloc") +ADD_TEST(test_option_memalloc_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-memalloc") +ADD_TEST(test_option_memalloc_contract "scripts/test_option" "good/contract.ept" "-memalloc") +ADD_TEST(test_option_memalloc_convolutions "scripts/test_option" "good/convolutions.ept" "-memalloc") ADD_TEST(test_option_memalloc_counter "scripts/test_option" "good/counter.ept" "-memalloc") ADD_TEST(test_option_memalloc_current "scripts/test_option" "good/current.ept" "-memalloc") +ADD_TEST(test_option_memalloc_downscale "scripts/test_option" "good/downscale.ept" "-memalloc") ADD_TEST(test_option_memalloc_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-memalloc") +ADD_TEST(test_option_memalloc_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-memalloc") ADD_TEST(test_option_memalloc_foldi "scripts/test_option" "good/foldi.ept" "-memalloc") ADD_TEST(test_option_memalloc_format "scripts/test_option" "good/format.ept" "-memalloc") ADD_TEST(test_option_memalloc_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-memalloc") @@ -562,6 +646,7 @@ ADD_TEST(test_option_memalloc_linear "scripts/test_option" "good/linear.ept" "-m ADD_TEST(test_option_memalloc_linear_init "scripts/test_option" "good/linear_init.ept" "-memalloc") ADD_TEST(test_option_memalloc_linear_split "scripts/test_option" "good/linear_split.ept" "-memalloc") ADD_TEST(test_option_memalloc_linear_vars "scripts/test_option" "good/linear_vars.ept" "-memalloc") +ADD_TEST(test_option_memalloc_mapnot "scripts/test_option" "good/mapnot.ept" "-memalloc") ADD_TEST(test_option_memalloc_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-memalloc") ADD_TEST(test_option_memalloc_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-memalloc") ADD_TEST(test_option_memalloc_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-memalloc") @@ -569,7 +654,10 @@ ADD_TEST(test_option_memalloc_name_clash "scripts/test_option" "good/name_clash. ADD_TEST(test_option_memalloc_norm "scripts/test_option" "good/norm.ept" "-memalloc") ADD_TEST(test_option_memalloc_or_keep "scripts/test_option" "good/or_keep.ept" "-memalloc") ADD_TEST(test_option_memalloc_parametrize "scripts/test_option" "good/parametrize.ept" "-memalloc") +ADD_TEST(test_option_memalloc_pip "scripts/test_option" "good/pip.ept" "-memalloc") +ADD_TEST(test_option_memalloc_pip_slice "scripts/test_option" "good/pip_slice.ept" "-memalloc") ADD_TEST(test_option_memalloc_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-memalloc") +ADD_TEST(test_option_memalloc_quasi "scripts/test_option" "good/quasi.ept" "-memalloc") ADD_TEST(test_option_memalloc_reinit "scripts/test_option" "good/reinit.ept" "-memalloc") ADD_TEST(test_option_memalloc_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-memalloc") ADD_TEST(test_option_memalloc_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-memalloc") @@ -606,6 +694,7 @@ ADD_TEST(test_option_memalloc_tuple_args "scripts/test_option" "good/tuple_args. ADD_TEST(test_option_memalloc_type_alias "scripts/test_option" "good/type_alias.ept" "-memalloc") ADD_TEST(test_option_memalloc_updown "scripts/test_option" "good/updown.ept" "-memalloc") ADD_TEST(test_option_memalloc_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-memalloc") +ADD_TEST(test_option_unroll_ais "scripts/test_option" "good/ais.ept" "-unroll") ADD_TEST(test_option_unroll_alloc "scripts/test_option" "good/alloc.ept" "-unroll") ADD_TEST(test_option_unroll_array1 "scripts/test_option" "good/array1.ept" "-unroll") ADD_TEST(test_option_unroll_array2 "scripts/test_option" "good/array2.ept" "-unroll") @@ -618,12 +707,18 @@ ADD_TEST(test_option_unroll_auto "scripts/test_option" "good/auto.ept" "-unroll" ADD_TEST(test_option_unroll_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-unroll") ADD_TEST(test_option_unroll_autohiera "scripts/test_option" "good/autohiera.ept" "-unroll") ADD_TEST(test_option_unroll_bad_updown "scripts/test_option" "good/bad_updown.ept" "-unroll") +ADD_TEST(test_option_unroll_ce "scripts/test_option" "good/ce.ept" "-unroll") ADD_TEST(test_option_unroll_ckannot "scripts/test_option" "good/ckannot.ept" "-unroll") ADD_TEST(test_option_unroll_clock_causality "scripts/test_option" "good/clock_causality.ept" "-unroll") ADD_TEST(test_option_unroll_clocks "scripts/test_option" "good/clocks.ept" "-unroll") +ADD_TEST(test_option_unroll_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-unroll") +ADD_TEST(test_option_unroll_contract "scripts/test_option" "good/contract.ept" "-unroll") +ADD_TEST(test_option_unroll_convolutions "scripts/test_option" "good/convolutions.ept" "-unroll") ADD_TEST(test_option_unroll_counter "scripts/test_option" "good/counter.ept" "-unroll") ADD_TEST(test_option_unroll_current "scripts/test_option" "good/current.ept" "-unroll") +ADD_TEST(test_option_unroll_downscale "scripts/test_option" "good/downscale.ept" "-unroll") ADD_TEST(test_option_unroll_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-unroll") +ADD_TEST(test_option_unroll_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-unroll") ADD_TEST(test_option_unroll_foldi "scripts/test_option" "good/foldi.ept" "-unroll") ADD_TEST(test_option_unroll_format "scripts/test_option" "good/format.ept" "-unroll") ADD_TEST(test_option_unroll_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-unroll") @@ -634,6 +729,7 @@ ADD_TEST(test_option_unroll_linear "scripts/test_option" "good/linear.ept" "-unr ADD_TEST(test_option_unroll_linear_init "scripts/test_option" "good/linear_init.ept" "-unroll") ADD_TEST(test_option_unroll_linear_split "scripts/test_option" "good/linear_split.ept" "-unroll") ADD_TEST(test_option_unroll_linear_vars "scripts/test_option" "good/linear_vars.ept" "-unroll") +ADD_TEST(test_option_unroll_mapnot "scripts/test_option" "good/mapnot.ept" "-unroll") ADD_TEST(test_option_unroll_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-unroll") ADD_TEST(test_option_unroll_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-unroll") ADD_TEST(test_option_unroll_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-unroll") @@ -641,7 +737,10 @@ ADD_TEST(test_option_unroll_name_clash "scripts/test_option" "good/name_clash.ep ADD_TEST(test_option_unroll_norm "scripts/test_option" "good/norm.ept" "-unroll") ADD_TEST(test_option_unroll_or_keep "scripts/test_option" "good/or_keep.ept" "-unroll") ADD_TEST(test_option_unroll_parametrize "scripts/test_option" "good/parametrize.ept" "-unroll") +ADD_TEST(test_option_unroll_pip "scripts/test_option" "good/pip.ept" "-unroll") +ADD_TEST(test_option_unroll_pip_slice "scripts/test_option" "good/pip_slice.ept" "-unroll") ADD_TEST(test_option_unroll_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-unroll") +ADD_TEST(test_option_unroll_quasi "scripts/test_option" "good/quasi.ept" "-unroll") ADD_TEST(test_option_unroll_reinit "scripts/test_option" "good/reinit.ept" "-unroll") ADD_TEST(test_option_unroll_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-unroll") ADD_TEST(test_option_unroll_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-unroll") @@ -678,6 +777,7 @@ ADD_TEST(test_option_unroll_tuple_args "scripts/test_option" "good/tuple_args.ep ADD_TEST(test_option_unroll_type_alias "scripts/test_option" "good/type_alias.ept" "-unroll") ADD_TEST(test_option_unroll_updown "scripts/test_option" "good/updown.ept" "-unroll") ADD_TEST(test_option_unroll_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-unroll") +ADD_TEST(test_option_O_ais "scripts/test_option" "good/ais.ept" "-O") ADD_TEST(test_option_O_alloc "scripts/test_option" "good/alloc.ept" "-O") ADD_TEST(test_option_O_array1 "scripts/test_option" "good/array1.ept" "-O") ADD_TEST(test_option_O_array2 "scripts/test_option" "good/array2.ept" "-O") @@ -690,12 +790,18 @@ ADD_TEST(test_option_O_auto "scripts/test_option" "good/auto.ept" "-O") ADD_TEST(test_option_O_autohiera2 "scripts/test_option" "good/autohiera2.ept" "-O") ADD_TEST(test_option_O_autohiera "scripts/test_option" "good/autohiera.ept" "-O") ADD_TEST(test_option_O_bad_updown "scripts/test_option" "good/bad_updown.ept" "-O") +ADD_TEST(test_option_O_ce "scripts/test_option" "good/ce.ept" "-O") ADD_TEST(test_option_O_ckannot "scripts/test_option" "good/ckannot.ept" "-O") ADD_TEST(test_option_O_clock_causality "scripts/test_option" "good/clock_causality.ept" "-O") ADD_TEST(test_option_O_clocks "scripts/test_option" "good/clocks.ept" "-O") +ADD_TEST(test_option_O_contract_automaton "scripts/test_option" "good/contract_automaton.ept" "-O") +ADD_TEST(test_option_O_contract "scripts/test_option" "good/contract.ept" "-O") +ADD_TEST(test_option_O_convolutions "scripts/test_option" "good/convolutions.ept" "-O") ADD_TEST(test_option_O_counter "scripts/test_option" "good/counter.ept" "-O") ADD_TEST(test_option_O_current "scripts/test_option" "good/current.ept" "-O") +ADD_TEST(test_option_O_downscale "scripts/test_option" "good/downscale.ept" "-O") ADD_TEST(test_option_O_fbyfby2 "scripts/test_option" "good/fbyfby2.ept" "-O") +ADD_TEST(test_option_O_foldi_arrays "scripts/test_option" "good/foldi_arrays.ept" "-O") ADD_TEST(test_option_O_foldi "scripts/test_option" "good/foldi.ept" "-O") ADD_TEST(test_option_O_format "scripts/test_option" "good/format.ept" "-O") ADD_TEST(test_option_O_grosauto_clock "scripts/test_option" "good/grosauto_clock.ept" "-O") @@ -706,6 +812,7 @@ ADD_TEST(test_option_O_linear "scripts/test_option" "good/linear.ept" "-O") ADD_TEST(test_option_O_linear_init "scripts/test_option" "good/linear_init.ept" "-O") ADD_TEST(test_option_O_linear_split "scripts/test_option" "good/linear_split.ept" "-O") ADD_TEST(test_option_O_linear_vars "scripts/test_option" "good/linear_vars.ept" "-O") +ADD_TEST(test_option_O_mapnot "scripts/test_option" "good/mapnot.ept" "-O") ADD_TEST(test_option_O_memalloc_clocks "scripts/test_option" "good/memalloc_clocks.ept" "-O") ADD_TEST(test_option_O_memalloc_record "scripts/test_option" "good/memalloc_record.ept" "-O") ADD_TEST(test_option_O_memalloc_simple "scripts/test_option" "good/memalloc_simple.ept" "-O") @@ -713,7 +820,10 @@ ADD_TEST(test_option_O_name_clash "scripts/test_option" "good/name_clash.ept" "- ADD_TEST(test_option_O_norm "scripts/test_option" "good/norm.ept" "-O") ADD_TEST(test_option_O_or_keep "scripts/test_option" "good/or_keep.ept" "-O") ADD_TEST(test_option_O_parametrize "scripts/test_option" "good/parametrize.ept" "-O") +ADD_TEST(test_option_O_pip "scripts/test_option" "good/pip.ept" "-O") +ADD_TEST(test_option_O_pip_slice "scripts/test_option" "good/pip_slice.ept" "-O") ADD_TEST(test_option_O_pre_tuple "scripts/test_option" "good/pre_tuple.ept" "-O") +ADD_TEST(test_option_O_quasi "scripts/test_option" "good/quasi.ept" "-O") ADD_TEST(test_option_O_reinit "scripts/test_option" "good/reinit.ept" "-O") ADD_TEST(test_option_O_sampling_stateful_output2 "scripts/test_option" "good/sampling_stateful_output2.ept" "-O") ADD_TEST(test_option_O_sampling_stateful_output "scripts/test_option" "good/sampling_stateful_output.ept" "-O") @@ -750,6 +860,7 @@ ADD_TEST(test_option_O_tuple_args "scripts/test_option" "good/tuple_args.ept" "- ADD_TEST(test_option_O_type_alias "scripts/test_option" "good/type_alias.ept" "-O") ADD_TEST(test_option_O_updown "scripts/test_option" "good/updown.ept" "-O") ADD_TEST(test_option_O_when_merge1 "scripts/test_option" "good/when_merge1.ept" "-O") +ADD_TEST(compile_javac_run_ais "scripts/compile_javac_run" "good/ais.ept") ADD_TEST(compile_javac_run_alloc "scripts/compile_javac_run" "good/alloc.ept") ADD_TEST(compile_javac_run_array1 "scripts/compile_javac_run" "good/array1.ept") ADD_TEST(compile_javac_run_array2 "scripts/compile_javac_run" "good/array2.ept") @@ -762,12 +873,18 @@ ADD_TEST(compile_javac_run_auto "scripts/compile_javac_run" "good/auto.ept") ADD_TEST(compile_javac_run_autohiera2 "scripts/compile_javac_run" "good/autohiera2.ept") ADD_TEST(compile_javac_run_autohiera "scripts/compile_javac_run" "good/autohiera.ept") ADD_TEST(compile_javac_run_bad_updown "scripts/compile_javac_run" "good/bad_updown.ept") +ADD_TEST(compile_javac_run_ce "scripts/compile_javac_run" "good/ce.ept") ADD_TEST(compile_javac_run_ckannot "scripts/compile_javac_run" "good/ckannot.ept") ADD_TEST(compile_javac_run_clock_causality "scripts/compile_javac_run" "good/clock_causality.ept") ADD_TEST(compile_javac_run_clocks "scripts/compile_javac_run" "good/clocks.ept") +ADD_TEST(compile_javac_run_contract_automaton "scripts/compile_javac_run" "good/contract_automaton.ept") +ADD_TEST(compile_javac_run_contract "scripts/compile_javac_run" "good/contract.ept") +ADD_TEST(compile_javac_run_convolutions "scripts/compile_javac_run" "good/convolutions.ept") ADD_TEST(compile_javac_run_counter "scripts/compile_javac_run" "good/counter.ept") ADD_TEST(compile_javac_run_current "scripts/compile_javac_run" "good/current.ept") +ADD_TEST(compile_javac_run_downscale "scripts/compile_javac_run" "good/downscale.ept") ADD_TEST(compile_javac_run_fbyfby2 "scripts/compile_javac_run" "good/fbyfby2.ept") +ADD_TEST(compile_javac_run_foldi_arrays "scripts/compile_javac_run" "good/foldi_arrays.ept") ADD_TEST(compile_javac_run_foldi "scripts/compile_javac_run" "good/foldi.ept") ADD_TEST(compile_javac_run_format "scripts/compile_javac_run" "good/format.ept") ADD_TEST(compile_javac_run_grosauto_clock "scripts/compile_javac_run" "good/grosauto_clock.ept") @@ -778,6 +895,7 @@ ADD_TEST(compile_javac_run_linear "scripts/compile_javac_run" "good/linear.ept") ADD_TEST(compile_javac_run_linear_init "scripts/compile_javac_run" "good/linear_init.ept") ADD_TEST(compile_javac_run_linear_split "scripts/compile_javac_run" "good/linear_split.ept") ADD_TEST(compile_javac_run_linear_vars "scripts/compile_javac_run" "good/linear_vars.ept") +ADD_TEST(compile_javac_run_mapnot "scripts/compile_javac_run" "good/mapnot.ept") ADD_TEST(compile_javac_run_memalloc_clocks "scripts/compile_javac_run" "good/memalloc_clocks.ept") ADD_TEST(compile_javac_run_memalloc_record "scripts/compile_javac_run" "good/memalloc_record.ept") ADD_TEST(compile_javac_run_memalloc_simple "scripts/compile_javac_run" "good/memalloc_simple.ept") @@ -785,7 +903,10 @@ ADD_TEST(compile_javac_run_name_clash "scripts/compile_javac_run" "good/name_cla ADD_TEST(compile_javac_run_norm "scripts/compile_javac_run" "good/norm.ept") ADD_TEST(compile_javac_run_or_keep "scripts/compile_javac_run" "good/or_keep.ept") ADD_TEST(compile_javac_run_parametrize "scripts/compile_javac_run" "good/parametrize.ept") +ADD_TEST(compile_javac_run_pip "scripts/compile_javac_run" "good/pip.ept") +ADD_TEST(compile_javac_run_pip_slice "scripts/compile_javac_run" "good/pip_slice.ept") ADD_TEST(compile_javac_run_pre_tuple "scripts/compile_javac_run" "good/pre_tuple.ept") +ADD_TEST(compile_javac_run_quasi "scripts/compile_javac_run" "good/quasi.ept") ADD_TEST(compile_javac_run_reinit "scripts/compile_javac_run" "good/reinit.ept") ADD_TEST(compile_javac_run_sampling_stateful_output2 "scripts/compile_javac_run" "good/sampling_stateful_output2.ept") ADD_TEST(compile_javac_run_sampling_stateful_output "scripts/compile_javac_run" "good/sampling_stateful_output.ept") diff --git a/test/good/ais.ept b/test/good/ais.ept new file mode 100644 index 0000000..d31dc9d --- /dev/null +++ b/test/good/ais.ept @@ -0,0 +1,8 @@ +type int_array = int^8 +type s = { t : int_array } + +node f(x : int_array) returns (r : s) +let + r = { t = x }; +tel + diff --git a/test/good/ce.ept b/test/good/ce.ept new file mode 100644 index 0000000..9b57b06 --- /dev/null +++ b/test/good/ce.ept @@ -0,0 +1,3 @@ +const c1 : int = 0 +const c2 : int = c1 + diff --git a/test/good/contract.ept b/test/good/contract.ept new file mode 100644 index 0000000..f0e3112 --- /dev/null +++ b/test/good/contract.ept @@ -0,0 +1,41 @@ +node f(x : bool) returns (y : bool) + +contract +var c, cx : bool; +let + c = not y; + cx = not (x & false fby x); +tel +assume cx +enforce c + +let + automaton + state A do y = x unless x then B + state B do y = false fby x until x then A + end +tel + +node g(x : bool) returns (y : bool) + +contract +var ok : bool; +let + automaton + state No_x do ok = true until x then One_x + state One_x do ok = not x + until x then Error + | not x then One_no_x + state One_no_x do ok = not x + until x then Error + | not x then No_x + state Error do ok = false + end +tel +assume ok +enforce not y + +let + y = f(x); +tel + diff --git a/test/good/contract_automaton.ept b/test/good/contract_automaton.ept new file mode 100644 index 0000000..1fe5fbb --- /dev/null +++ b/test/good/contract_automaton.ept @@ -0,0 +1,50 @@ +node f(x : bool) returns (y : bool) + +contract +var c, cx : bool; +let + c = not y; + cx = not (x & false fby x); +tel +assume cx +enforce c + +let + automaton + state A do y = x unless x then B + state B do y = false fby x until x then A + end +tel + +node g(x : bool) returns (last y : bool) + +contract +var ok : bool; +let + automaton + state No_x do ok = true until x then One_x + state One_x do ok = not x + until x then Error + | not x then One_no_x + state One_no_x do ok = not x + until x then Error + | not x then No_x + state Error do ok = false + end +tel +assume ok +enforce not y + +let + automaton + state Idle do y = false -> last y + until x then Active + state Active + var c : int; + do + y = f(x); + c = 1 fby c + 1; + until c = 20 then Idle + end +tel + diff --git a/test/good/tuple_args.ept b/test/good/tuple_args.ept old mode 100755 new mode 100644 From 8650ac5695a4bb8681067f90146bc8b4f031c743 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Fri, 21 Feb 2014 18:12:07 +0100 Subject: [PATCH 7/8] Version 1.00.06 --- CHANGES | 5 +++++ Makefile-distrib | 2 +- compiler/utilities/global/compiler_options.ml | 2 +- 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index d39f7f5..c680626 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,8 @@ +Heptagon 1.00.06 (21/02/2014) +----------------------------- + + - allowed abstractions (non-inlined subnodes calls) in contracts + Heptagon 1.00.05 (28/01/2014) ----------------------------- diff --git a/Makefile-distrib b/Makefile-distrib index b6bef16..bb0b9f6 100644 --- a/Makefile-distrib +++ b/Makefile-distrib @@ -2,7 +2,7 @@ include config #version = $(shell date +"%d%m%y") -version = 1.00.05 +version = 1.00.06 osname=$(shell uname -s) hardware=$(shell uname -m) heptdir = heptagon-$(version) diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index be3f969..dbd5536 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -32,7 +32,7 @@ open Names (* version of the compiler *) -let version = "1.00.05" +let version = "1.00.06" let date = "DATE" (* standard module *) From 478e621ac5360661a2aea95e261b99451f084da9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Sat, 22 Feb 2014 23:53:49 +0100 Subject: [PATCH 8/8] Handling of contracts in Mls2obc Handling of contracts when the "z3z" target is off. Equations of contracts are put into the node in the Mls2obc pass (done by the "z3z" code generation). --- compiler/main/mls2obc.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 6a9d68f..933933c 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -697,7 +697,7 @@ let remove m d_list = let translate_contract map mem_var_tys = function - | None -> ([], [], [], []) + | None -> ([], [], [], [], []) | Some { Minils.c_eq = eq_list; @@ -705,9 +705,9 @@ let translate_contract map mem_var_tys = } -> let (v, si, j, s_list) = translate_eq_list map empty_call_context eq_list in let d_list = translate_var_dec (v @ d_list) in - let d_list = List.filter - (fun vd -> not (List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys)) d_list in - (si, j, s_list, d_list) + let m, d_list = List.partition + (fun vd -> List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys) d_list in + (m, si, j, s_list, d_list) (** Returns a map, mapping variables names to the variables where they will be stored. *) @@ -734,7 +734,7 @@ let translate_node | Some c -> c.Minils.c_controllables, c.Minils.c_local in let subst_map = subst_map i_list o_list c_list c_locals d_list mem_var_tys in let (v, si, j, s_list) = translate_eq_list subst_map empty_call_context eq_list in - let (si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in + let (m_c, si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in let i_list = translate_var_dec i_list in let o_list = translate_var_dec o_list in let d_list = translate_var_dec (v @ d_list) in @@ -751,7 +751,7 @@ let translate_node in let resetm = { m_name = Mreset; m_inputs = []; m_outputs = []; m_body = mk_block si } in if stateful - then { cd_name = f; cd_stateful = true; cd_mems = m' @ m; cd_params = params; + then { cd_name = f; cd_stateful = true; cd_mems = m' @ m @ m_c; cd_params = params; cd_objs = j; cd_methods = [stepm; resetm]; cd_loc = loc; cd_mem_alloc = mem_alloc } else ( (* Functions won't have [Mreset] or memories,