From 207de4d6e740b010448af00d978c52d771c63b3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Tue, 14 Dec 2010 18:36:54 +0100 Subject: [PATCH] Added some tests. --- test/bad/bad_flatten.ept | 12 +++ test/bad/bad_merge1.ept | 6 ++ test/bad/bad_merge2.ept | 6 ++ test/bad/bad_merge3.ept | 6 ++ test/good/bad_updown.ept | 12 +++ test/good/flatten.ept | 17 ++++ test/good/statics2.ept | 32 +++++++ test/good/t3.ept | 3 +- test/good/when_merge1.ept | 184 ++++++++++++++++++++++++++++++++++++++ tools/old_debugger_script | 130 +++++++++++++++++++++++++++ 10 files changed, 407 insertions(+), 1 deletion(-) create mode 100644 test/bad/bad_flatten.ept create mode 100644 test/bad/bad_merge1.ept create mode 100644 test/bad/bad_merge2.ept create mode 100644 test/bad/bad_merge3.ept create mode 100644 test/good/bad_updown.ept create mode 100644 test/good/flatten.ept create mode 100644 test/good/statics2.ept create mode 100644 test/good/when_merge1.ept create mode 100644 tools/old_debugger_script diff --git a/test/bad/bad_flatten.ept b/test/bad/bad_flatten.ept new file mode 100644 index 0000000..a3cb584 --- /dev/null +++ b/test/bad/bad_flatten.ept @@ -0,0 +1,12 @@ + +node f(x,y : int; b : bool) returns (z : int) +var t : int; +let + do + var t2 : int; in + t = x + t2; + t2 = if b then 0 else 1; + done; + z = t2 +tel + diff --git a/test/bad/bad_merge1.ept b/test/bad/bad_merge1.ept new file mode 100644 index 0000000..3be86f2 --- /dev/null +++ b/test/bad/bad_merge1.ept @@ -0,0 +1,6 @@ +type t = A | B +type tt = C +node t2bool(x: t) returns (b: bool) + let + b = merge x (A-> true) (B-> true) (C-> false) + tel diff --git a/test/bad/bad_merge2.ept b/test/bad/bad_merge2.ept new file mode 100644 index 0000000..29e080d --- /dev/null +++ b/test/bad/bad_merge2.ept @@ -0,0 +1,6 @@ +type t = A | B + +node t2bool(x: t) returns (b: bool) + let + b = merge x (A-> true) (B-> true) (A-> false) + tel diff --git a/test/bad/bad_merge3.ept b/test/bad/bad_merge3.ept new file mode 100644 index 0000000..63955dc --- /dev/null +++ b/test/bad/bad_merge3.ept @@ -0,0 +1,6 @@ +type t = A | B | C | D + +node t2bool(x: t) returns (b: bool) + let + b = merge x (B-> true) (C-> true) + tel diff --git a/test/good/bad_updown.ept b/test/good/bad_updown.ept new file mode 100644 index 0000000..771ed38 --- /dev/null +++ b/test/good/bad_updown.ept @@ -0,0 +1,12 @@ +node updown(b : bool) returns (o : bool) +var o',on_off:bool; +let + on_off = true; + automaton + state Down + do o' = false until on_off then Up + state Up + do o' = true until on_off then Down + end; + o = merge b (true-> o') (false -> false) +tel diff --git a/test/good/flatten.ept b/test/good/flatten.ept new file mode 100644 index 0000000..e9c656f --- /dev/null +++ b/test/good/flatten.ept @@ -0,0 +1,17 @@ + +node f(x,y : int; b : bool) returns (z : int) +var t : int; +let + do + var t2,t2' : int; in + t2 = if b then 0 else t2'; + do + var t3 : int; in + t3 = y + t; + t2' = t3; + done; + t = x + t2; + done; + z = t; +tel + diff --git a/test/good/statics2.ept b/test/good/statics2.ept new file mode 100644 index 0000000..22b5768 --- /dev/null +++ b/test/good/statics2.ept @@ -0,0 +1,32 @@ +(* Check manually *) +(* This test should only create two instances of f. *) +const c2:int = 3 +const k2:int = 1 + +fun f<>() returns (y:int) +let + y = n + 3 + c2; +tel + +fun g<>() returns (y:int) +var x:int; +let + x = m + f<<2>>(); + y = f<>(); +tel + +fun i<>() returns (o : int) +var x, y, z: int; +let + x = f<<2>>(); + y = f<<1 + m>>(); + z = f<>(); + o = f<>(); +tel + +fun h() returns (y,y':int) +let + y = c2 + g<>() + i<>(); + y' = c2 + Statics.g<>() + Statics.i<>(); +tel + diff --git a/test/good/t3.ept b/test/good/t3.ept index 8418e65..a70c31f 100644 --- a/test/good/t3.ept +++ b/test/good/t3.ept @@ -2,8 +2,9 @@ set arguments -v test/good/t3.ept *) node f(x,z:int) returns (o:int) - var o1:int; + var o1:int;r:bool; let + r = false; automaton state Init do o = 1 + 2 diff --git a/test/good/when_merge1.ept b/test/good/when_merge1.ept new file mode 100644 index 0000000..eeedb0c --- /dev/null +++ b/test/good/when_merge1.ept @@ -0,0 +1,184 @@ +(* pour debugger ../../compiler/hec.byte -i -v -I ../../lib t1.ept *) +(* pour debugger + directory parsing global analysis dataflow sequential sigali simulation translation main + set arguments -v ../test/good/t1.ept *) + +type t = A | B + +node bool2int(b: bool) returns (o: int) + let + o = merge b (true -> 1) (false -> 0) + tel + +node t2bool(x: t) returns (b: bool) + let + b = merge x (A-> true) (B-> false) + tel + +(* +node mm(x: int) returns (o: int) + var last m: int = 0; + let + switch (x = 0) + | true do m = last m + 1; o = m + | false do m = 2; o = m + end + tel + +node mmm(x: int) returns (o': int) + var last m: int = 1; o: int; + let + automaton + state I + do m = 0; o = last m + 1 until (o = 1) then J + state J + do m = last m + 1; o = 0 + end; + o' = 1 -> pre o + tel + +node m(x: int) returns (o: int) + var last o' : int = 1; + let + automaton + state I + do o' = 1 + unless (last o' = 2) then J + state J + do o' = 3 + unless (last o' = 1) then I + end; + o = o'; + tel + +node h(z: int; x, y: int) returns (o2: int) + var o1, o: int; + let + (o1, o2) = if z<0 then (1, 2) else (3, 4); + o = 0 -> pre o + 2 + tel + +node i(x, y: int) returns (o: int) + var z, k: int; + let + reset + o = 0 + x + y; + reset + z = 1 + o + 3; + k = z + o + 2 + every (x = x) + every (x = y) + tel + +node j(x, y: int) returns (o: int) + let + automaton + state I + var z: int; + do o = 1; z = 2 + until (o = 2) then J + state J + do o = 2 + until (o = 1) then I + end + tel + +node (++)(up, down: int) returns (o: int) + var last cpt: int = 42; + let + o = last cpt; + automaton + state Init + var k : int; + do k = 0 -> pre k + 2; + cpt = 0 + until + (up = 1) then Up + state Up + do cpt = last cpt + 1 + until (down = 1) then Down + | (down = 0) then Up + state Down + do cpt = (last cpt) + 1 + until (up = 1) then Up + end; + tel + +node f(x: bool) returns (y: bool) + var z: bool; + let + y = x or x & x; + z = true -> if y then not (pre z) else pre z; + tel + +(* +let increasing(x) returns (o) + do true -> x >= pre(x) + 1 done + +modes(v0) = + last o = v0 + when up(x) returns (w) + assume (x >= 0) ensure (w >= 0) + do w = x + last o + 2; o = w + 4 done + when down(x) returns (w) + do w = x - last o + 2; o = w + 2 done + end + +val gain : int > + modes last o : int when up: int -> int when down: int -> int + end with { up # down } + +let node gain(v0)(up, down) returns (o) + assume (v0 >= 0) & (increasing up) + guaranty (deacreasing o) + last o = 0 in + automaton + state Await + do + unless down then Down(1) | up then Up(1) + state Down(d) + let rec cpt = 1 -> pre cpt + 1 in + do o = last o - d + until (cpt >= 5) then Down(d-5) + until up then Up(1) + state Up(d) + let rec cpt = 1 -> pre cpt + 1 in + do o = last o + d + until (cpt >= 5) then Up(d+5) + until down then Down(1) + state Unreachable + let rec c = 0 + 2 in + var m in + do o = m + 2; m = 3 + c done + end + +node g(x, y: int) returns (o: int) + let + o = x ++ y; + tel + +node dfby(x)(y) returns (o) + let + o = x fby (x fby y) + tel + +node f(x)(y) returns (o) + var last o = x; + let + o = last o + y + tel + +val f : int > (int => int) + +static x = e in ... + +(if c then (fun x -> x + 2) else (fun k -> k + 3))(x+2) + +let M(x1,..., xn) = + let y1 = ... in ... let yk = ... in + modes + mem m1 = ...; mem ml = ...; + step (...) returns (...) ... + reset = ... + end +*) *) diff --git a/tools/old_debugger_script b/tools/old_debugger_script new file mode 100644 index 0000000..5b50e38 --- /dev/null +++ b/tools/old_debugger_script @@ -0,0 +1,130 @@ +load_printer "/sw/lib/ocaml/menhirLib/menhirLib.cmo" +load_printer "/sw/lib/ocaml/str.cma" +load_printer "_build/global/names.d.cmo" +load_printer "_build/global/location.d.cmo" +load_printer "_build/utilities/misc.d.cmo" +load_printer "_build/global/types.d.cmo" +load_printer "_build/global/signature.d.cmo" +load_printer "_build/utilities/global/compiler_options.d.cmo" +load_printer "_build/utilities/global/errors.d.cmo" +load_printer "_build/utilities/global/compiler_utils.d.cmo" +load_printer "_build/global/modules.d.cmo" +load_printer "_build/global/initial.d.cmo" +load_printer "_build/global/idents.d.cmo" +load_printer "_build/global/clocks.d.cmo" +load_printer "_build/utilities/pp_tools.d.cmo" +load_printer "_build/global/global_printer.d.cmo" +load_printer "_build/global/static.d.cmo" +load_printer "_build/heptagon/heptagon.d.cmo" +load_printer "_build/heptagon/analysis/initialization.d.cmo" +load_printer "_build/global/global_mapfold.d.cmo" +load_printer "_build/heptagon/hept_mapfold.d.cmo" +load_printer "_build/heptagon/analysis/statefull.d.cmo" +load_printer "_build/heptagon/analysis/typing.d.cmo" +load_printer "_build/heptagon/hept_printer.d.cmo" +load_printer "_build/heptagon/parsing/hept_parsetree.d.cmo" +load_printer "_build/heptagon/parsing/hept_parser.d.cmo" +load_printer "_build/heptagon/parsing/hept_lexer.d.cmo" +load_printer "_build/heptagon/parsing/hept_scoping.d.cmo" +load_printer "_build/heptagon/transformations/automata.d.cmo" +load_printer "_build/heptagon/transformations/block.d.cmo" +load_printer "_build/heptagon/transformations/completion.d.cmo" +load_printer "_build/heptagon/transformations/reset.d.cmo" +load_printer "_build/heptagon/transformations/every.d.cmo" +load_printer "_build/heptagon/transformations/last.d.cmo" +load_printer "_build/heptagon/transformations/present.d.cmo" +load_printer "_build/heptagon/main/hept_compiler.d.cmo" +load_printer "_build/heptagon/parsing/hept_parsetree_mapfold.d.cmo" +load_printer "_build/heptagon/parsing/hept_static_scoping.d.cmo" +load_printer "_build/minils/minils.d.cmo" +load_printer "_build/minils/mls_mapfold.d.cmo" +load_printer "_build/minils/mls_printer.d.cmo" +load_printer "_build/utilities/graph.d.cmo" +load_printer "_build/utilities/global/dep.d.cmo" +load_printer "_build/minils/mls_utils.d.cmo" +load_printer "_build/main/hept2mls.d.cmo" +load_printer "_build/minils/transformations/itfusion.d.cmo" +load_printer "_build/obc/obc.d.cmo" +load_printer "_build/obc/control.d.cmo" +load_printer "_build/obc/obc_mapfold.d.cmo" +load_printer "_build/main/mls2obc.d.cmo" +load_printer "_build/minils/transformations/callgraph.d.cmo" +load_printer "_build/obc/c/c.d.cmo" +load_printer "_build/obc/c/csubst.d.cmo" +load_printer "_build/obc/obc_utils.d.cmo" +load_printer "_build/obc/c/cgen.d.cmo" +load_printer "_build/obc/c/cmain.d.cmo" +load_printer "_build/obc/obc_printer.d.cmo" +load_printer "_build/minils/main/mls2seq.d.cmo" +load_printer "_build/minils/analysis/clocking.d.cmo" +load_printer "_build/minils/transformations/normalize.d.cmo" +load_printer "_build/minils/transformations/schedule.d.cmo" +load_printer "_build/global/global_compare.d.cmo" +load_printer "_build/minils/mls_compare.d.cmo" +load_printer "_build/minils/transformations/checkpass.d.cmo" +load_printer "_build/minils/transformations/introvars.d.cmo" +load_printer "_build/minils/transformations/singletonvars.d.cmo" +load_printer "_build/minils/transformations/tomato.d.cmo" +load_printer "_build/minils/main/mls_compiler.d.cmo" +load_printer "_build/main/heptc.d.cmo" + + +install_printer Idents.IdentSet.fprint_t + +install_printer Global_printer.print_ck +install_printer Global_printer.print_clock +install_printer Global_printer.print_field +install_printer Global_printer.print_ident +install_printer Global_printer.print_interface +install_printer Global_printer.print_param +install_printer Global_printer.print_qualname +install_printer Global_printer.print_size_constraint +install_printer Global_printer.print_static_exp +install_printer Global_printer.print_static_exp_tuple +install_printer Global_printer.print_struct +install_printer Global_printer.print_type + + + +install_printer Names.print_name + +install_printer Hept_printer.print_iterator +install_printer Hept_printer.print_pat +install_printer Hept_printer.print_vd +install_printer Hept_printer.print_exps +install_printer Hept_printer.print_exp +install_printer Hept_printer.print_app +install_printer Hept_printer.print_eq +install_printer Hept_printer.print_eq_list +install_printer Hept_printer.print_state_handler_list +install_printer Hept_printer.print_switch_handler_list +install_printer Hept_printer.print_present_handler_list +install_printer Hept_printer.print_inblock +install_printer Hept_printer.print_type_def +install_printer Hept_printer.print_const_dec +install_printer Hept_printer.print_contract +install_printer Hept_printer.print_node_params +install_printer Hept_printer.print_node +install_printer Hept_printer.print_open_module + + +install_printer Mls_printer.print_pat +install_printer Mls_printer.print_ck +install_printer Mls_printer.print_vd +install_printer Mls_printer.print_vd_tuple +install_printer Mls_printer.print_local_vars +install_printer Mls_printer.print_const_dec +install_printer Mls_printer.print_params +install_printer Mls_printer.print_node_params +install_printer Mls_printer.print_exp_tuple +install_printer Mls_printer.print_vd_tuple +install_printer Mls_printer.print_index +install_printer Mls_printer.print_dyn_index +install_printer Mls_printer.print_every +install_printer Mls_printer.print_exp_desc +install_printer Mls_printer.print_eq +install_printer Mls_printer.print_eqs +install_printer Mls_printer.print_open_module +install_printer Mls_printer.print_type_dec +install_printer Mls_printer.print_contract +install_printer Mls_printer.print_node