diff options
Diffstat (limited to 'test/monniaux')
101 files changed, 3306 insertions, 488 deletions
diff --git a/test/monniaux/benches.list b/test/monniaux/benches.list deleted file mode 100644 index ff62dd4e..00000000 --- a/test/monniaux/benches.list +++ /dev/null @@ -1,2 +0,0 @@ - binary_search bitslicedaes bitslicedtea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha2 taclebenchlift taclebenchpowerwindow ternary too_slow - diff --git a/test/monniaux/benches.sh b/test/monniaux/benches.sh new file mode 100644 index 00000000..9bca6b42 --- /dev/null +++ b/test/monniaux/benches.sh @@ -0,0 +1 @@ +benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow ternary too_slow" diff --git a/test/monniaux/binary_search/make.proto b/test/monniaux/binary_search/make.proto index 19501e78..337751bb 100644 --- a/test/monniaux/binary_search/make.proto +++ b/test/monniaux/binary_search/make.proto @@ -1 +1,2 @@ -binary_search +target: binary_search +measures: ["random fill", search1] diff --git a/test/monniaux/bitsliced-aes/Makefile b/test/monniaux/bitsliced-aes/Makefile deleted file mode 100644 index 6a0367e0..00000000 --- a/test/monniaux/bitsliced-aes/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -src = $(wildcard *.c) tests/tests.c - -include ../rules.mk - -all: test.gcc.k1c.out test.gcc.o1.k1c.out test.ccomp.k1c.out test.gcc.host.out test.ccomp.host.out - -test.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ - -test.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ - -test.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ - -test.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o - $(CC) $(CFLAGS) -o $@ $+ - -test.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) -o $@ $+ - -clean: - rm -f *.o *.k1c *.host */*.o *.s */*.s *.out diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c index 083a8fc5..3132e1d9 100644 --- a/test/monniaux/bitsliced-aes/bs.c +++ b/test/monniaux/bitsliced-aes/bs.c @@ -3,7 +3,11 @@ #include "bs.h" #include "../ternary.h" +/* TEMPORARY */ +#define TERNARY(x, v0, v1) ((x) ? (v0) : (v1)) +/* #define TERNARY(x, v0, v1) TERNARY64(x, v1, v0) +*/ #if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\ defined(__amd64__) || defined(__amd32__)|| defined(__amd16__) diff --git a/test/monniaux/bitsliced-aes/make.proto b/test/monniaux/bitsliced-aes/make.proto new file mode 100644 index 00000000..8a9a1bff --- /dev/null +++ b/test/monniaux/bitsliced-aes/make.proto @@ -0,0 +1,4 @@ +sources: "$(wildcard *.c) tests/tests.c" +target: test +measures: [cycles] +name: bitsliced-aes diff --git a/test/monniaux/bitsliced-tea/Makefile b/test/monniaux/bitsliced-tea/Makefile deleted file mode 100644 index 3d5fd540..00000000 --- a/test/monniaux/bitsliced-tea/Makefile +++ /dev/null @@ -1,27 +0,0 @@ -include ../rules.mk - -PRODUCTS=bstea.gcc.host.out bstea.ccomp.host.out bstea.gcc.o1.k1c.out bstea.gcc.k1c.out bstea.ccomp.k1c.out bstea.ccomp.k1c.s bstea.gcc.k1c.s bstea.gcc.k1c bstea.ccomp.k1c bstea.gcc.host bstea.ccomp.host - -all: $(PRODUCTS) - -bstea.gcc.host: bstea.c bstea_run.c bstea.h ../clock.o - $(CC) $(CFLAGS) bstea.c bstea_run.c ../clock.o -o $@ - -bstea.ccomp.host: bstea.c bstea_run.c bstea.h ../clock.o - $(CCOMP) $(CCOMPFLAGS) bstea.c bstea_run.c ../clock.o -o $@ - -bstea.gcc.k1c.s bstea.ccomp.k1c.s bstea_run.gcc.k1c.s: bstea.h - -bstea.gcc.k1c: bstea.gcc.k1c.o bstea_run.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -bstea.gcc.o1.k1c: bstea.gcc.o1.k1c.o bstea_run.gcc.o1.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -bstea.ccomp.k1c: bstea.ccomp.k1c.o bstea_run.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f *.k1c *.host *.out *.o *.s - -.PHONY: clean diff --git a/test/monniaux/bitsliced-tea/make.proto b/test/monniaux/bitsliced-tea/make.proto new file mode 100644 index 00000000..6cdc0814 --- /dev/null +++ b/test/monniaux/bitsliced-tea/make.proto @@ -0,0 +1,4 @@ +objdeps: [{name: bstea_run, compiler: gcc}] +target: bstea +name: bitsliced-tea +measures: [cycles] diff --git a/test/monniaux/build_benches.sh b/test/monniaux/build_benches.sh new file mode 100755 index 00000000..02123665 --- /dev/null +++ b/test/monniaux/build_benches.sh @@ -0,0 +1,9 @@ + +source benches.sh + +rm -f commands.txt +for bench in $benches; do + echo "(cd $bench && make -j5 $1)" >> commands.txt +done + +cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}' diff --git a/test/monniaux/clean_benches.sh b/test/monniaux/clean_benches.sh new file mode 100755 index 00000000..c0a87ff9 --- /dev/null +++ b/test/monniaux/clean_benches.sh @@ -0,0 +1,8 @@ + +source benches.sh + +rm -f commands.txt +for bench in $benches; do + (cd $bench && make clean) +done +rm -f *.o diff --git a/test/monniaux/clean_csv.sh b/test/monniaux/clean_csv.sh new file mode 100755 index 00000000..e480aa5a --- /dev/null +++ b/test/monniaux/clean_csv.sh @@ -0,0 +1,9 @@ + +source benches.sh + +rm -f commands.txt +for bench in $benches; do + (cd $bench && rm *.csv) +done + +rm measures.csv diff --git a/test/monniaux/complex/Makefile b/test/monniaux/complex/Makefile deleted file mode 100644 index ca3d441b..00000000 --- a/test/monniaux/complex/Makefile +++ /dev/null @@ -1,29 +0,0 @@ -include ../rules.mk - -PRODUCTS=complex_mat.gcc.host.out complex_mat.ccomp.host.out \ - complex_mat.gcc.k1c.out complex_mat.gcc.o1.k1c.out complex_mat.ccomp.k1c.out \ - complex_mat.gcc.k1c.s complex_mat.ccomp.k1c.s - -all: $(PRODUCTS) - -complex_mat.gcc.host.s complex_mat.ccomp.host.s complex_mat.gcc.k1c.s complex_mat.ccomp.k1c.s : ../clock.h - -complex_mat.ccomp.host: complex_mat.ccomp.host.o ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -o $@ - -complex_mat.gcc.host: complex_mat.gcc.host.o ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ -o $@ - -complex_mat.gcc.k1c: complex_mat.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -complex_mat.gcc.o1.k1c: complex_mat.gcc.o1.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -complex_mat.ccomp.k1c: complex_mat.ccomp.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - -rm -f *.o *.s *.k1c - -.PHONY: clean diff --git a/test/monniaux/complex/complex_mat.c b/test/monniaux/complex/complex_mat.c index 6c7dae1d..b7103f60 100644 --- a/test/monniaux/complex/complex_mat.c +++ b/test/monniaux/complex/complex_mat.c @@ -227,9 +227,9 @@ int main() { printf("c1==c8: %s\n" "c1==c9: %s\n" - "c1_time = %" PRIu64 "\n" - "c8_time = %" PRIu64 "\n" - "c9_time = %" PRIu64 "\n", + "c1_time : %" PRIu64 "\n" + "c8_time : %" PRIu64 "\n" + "c9_time : %" PRIu64 "\n", COMPLEX_mat_equal(m, n, c1, p, c8, p)?"true":"false", COMPLEX_mat_equal(m, n, c1, p, c9, p)?"true":"false", diff --git a/test/monniaux/complex/make.proto b/test/monniaux/complex/make.proto new file mode 100644 index 00000000..8870f311 --- /dev/null +++ b/test/monniaux/complex/make.proto @@ -0,0 +1,2 @@ +target: complex_mat +measures: [[c1_time, c1]] diff --git a/test/monniaux/division/sum_div.c b/test/monniaux/division/sum_div.c new file mode 100644 index 00000000..87256922 --- /dev/null +++ b/test/monniaux/division/sum_div.c @@ -0,0 +1,18 @@ +#include <stdio.h> +#include <stdlib.h> +#include "../clock.h" + +int main(int argc, char **argv) { + unsigned modulus = argc < 2 ? 3371 : atoi(argv[1]); + clock_prepare(); + clock_start(); + unsigned total=0, total_mod=0; + for(int i=0; i<1000; i++) { + total += i; + total_mod = (total_mod + i)%modulus; + } + clock_stop(); + print_total_clock(); + printf("%u %u %d\n", total, total_mod, total%modulus == total_mod); + return 0; +} diff --git a/test/monniaux/dm_random.c b/test/monniaux/dm_random.c new file mode 100644 index 00000000..6643b79f --- /dev/null +++ b/test/monniaux/dm_random.c @@ -0,0 +1,7 @@ +#include <stdint.h> + +static uint32_t dm_random_uint32(void) { + static uint32_t current=UINT32_C(0xDEADBEEF); + current = ((uint64_t) current << 6) % UINT32_C(4294967291); + return current; +} diff --git a/test/monniaux/float_mat/Makefile b/test/monniaux/float_mat/Makefile deleted file mode 100644 index 0d3d68d6..00000000 --- a/test/monniaux/float_mat/Makefile +++ /dev/null @@ -1,24 +0,0 @@ -include ../rules.mk - -PRODUCTS=float_mat.host float_mat.gcc.o1.k1c.out float_mat.gcc.k1c.out float_mat.ccomp.k1c.out float_mat.ccomp.k1c.s float_mat.gcc.k1c.s float_mat.gcc.k1c float_mat.ccomp.k1c - -all: $(PRODUCTS) - -float_mat.host: float_mat.c float_mat_run.c float_mat.h - $(CC) $(CFLAGS) float_mat.c float_mat_run.c -o $@ - -float_mat.gcc.k1c.s float_mat.ccomp.k1c.s float_mat_run.gcc.k1c.s: float_mat.h - -float_mat.gcc.k1c: float_mat.gcc.k1c.o float_mat_run.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -float_mat.gcc.o1.k1c: float_mat.gcc.o1.k1c.o float_mat_run.gcc.o1.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -float_mat.ccomp.k1c: float_mat.ccomp.k1c.o float_mat_run.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f *.k1c *.host *.o *.s - -.PHONY: clean diff --git a/test/monniaux/float_mat/float_mat_run.c b/test/monniaux/float_mat/float_mat_run.c index 5d34bb70..329648c2 100644 --- a/test/monniaux/float_mat/float_mat_run.c +++ b/test/monniaux/float_mat/float_mat_run.c @@ -93,14 +93,14 @@ int main() { "c1==c6: %s\n" "c1==c7: %s\n" "c1==c8: %s\n" - "c1_time = %" PRIu64 "\n" - "c2_time = %" PRIu64 "\n" - "c3_time = %" PRIu64 "\n" - "c4_time = %" PRIu64 "\n" - "c5_time = %" PRIu64 "\n" - "c6_time = %" PRIu64 "\n" - "c7_time = %" PRIu64 "\n" - "c8_time = %" PRIu64 "\n", + "c1_time : %" PRIu64 "\n" + "c2_time : %" PRIu64 "\n" + "c3_time : %" PRIu64 "\n" + "c4_time : %" PRIu64 "\n" + "c5_time : %" PRIu64 "\n" + "c6_time : %" PRIu64 "\n" + "c7_time : %" PRIu64 "\n" + "c8_time : %" PRIu64 "\n", REAL_mat_equal(m, n, c1, p, c2, p)?"true":"false", REAL_mat_equal(m, n, c1, p, c3, p)?"true":"false", diff --git a/test/monniaux/float_mat/make.proto b/test/monniaux/float_mat/make.proto new file mode 100644 index 00000000..ebdd8930 --- /dev/null +++ b/test/monniaux/float_mat/make.proto @@ -0,0 +1,3 @@ +objdeps: [{name: float_mat_run, compiler: gcc}] +target: float_mat +measures: [[c2_time, c2]] diff --git a/test/monniaux/generate_makefiles.sh b/test/monniaux/generate_makefiles.sh index ed8270b5..ecbbdf4d 100755 --- a/test/monniaux/generate_makefiles.sh +++ b/test/monniaux/generate_makefiles.sh @@ -1,5 +1,8 @@ -#!/usr/bin/bash +#!/usr/bin/env bash -for bench in binary_search; do - ./genmake.py $(cat $bench/make.proto) > $bench/Makefile +source benches.sh + +for bench in $benches; do + ./genmake.py $bench/make.proto > $bench/Makefile done + diff --git a/test/monniaux/gengraphs.py b/test/monniaux/gengraphs.py new file mode 100755 index 00000000..3ffe6f3d --- /dev/null +++ b/test/monniaux/gengraphs.py @@ -0,0 +1,94 @@ +#!/usr/bin/python3.6 + +import numpy as np # type: ignore +import matplotlib.pyplot as plt # type: ignore +import pandas as pd # type: ignore +import sys +from typing import * + +## +# Reading data +## + +if len(sys.argv) != 2: + raise Exception("Only 1 argument should be given to this script: the make.proto file") +csv_file = sys.argv[1] + +with open(csv_file, "r") as f: + df = pd.read_csv(csv_file) + +benches = df["benches"] + +host_measures_cols = [col for col in df if "host" in col] +k1c_measures_cols = [col for col in df if "k1c" in col] + +colors = ["forestgreen", "darkorange", "cornflowerblue", "darkorchid", "darksalmon", "dodgerblue", "navy", "gray", "springgreen", "crimson"] + +## +# Generating PDF +## + +def extract_compiler(env: str) -> str: + words = env.split()[:-1] + return " ".join(words) + +def extract_compilers(envs: List[str]) -> List[str]: + compilers: List[str] = [] + for env in envs: + compiler = extract_compiler(env) + if compiler not in compilers: + compilers.append(compiler) + return compilers + +def subdivide_interv(inf: Any, sup: float, n: int) -> List[float]: + return [inf + k*(sup-inf)/n for k in range(n)] + + +# df associates the environment string (e.g. "gcc host") to the cycles +# envs is the list of environments to compare +# The returned value will be a dictionnary associating the compiler (e.g. "gcc") to his relative comparison on the best result +def make_relative_heights(data: Any, envs: List[str]) -> Dict[str, List[float]]: + n_benches: int = len((data.values)) # type: ignore + cols: Dict[str, List[int]] = {extract_compiler(env):data[env] for env in envs} + + ret: Dict[str, List[float]] = {} + for compiler in cols: + ret[compiler] = [] + + for i in range(n_benches): + max_time: int = max([cols[compiler][i] for compiler in cols]) + for compiler in cols: + ret[compiler].append(cols[compiler][i] / float(max_time)) + + return ret + + +def generate_file(f: str, cols: List[str]) -> None: + ind = np.arange(len(df[cols[0]])) + + width = 0.25 # the width of the bars + + compilers = extract_compilers(cols) + start_inds = subdivide_interv(ind, ind+2*width, len(compilers)) + heights: Dict[str, List[float]] = make_relative_heights(df, cols) + + fig, ax = plt.subplots() + rects = [] + for i, compiler in enumerate(compilers): + rects.append(ax.bar(start_inds[i], heights[compiler], width, color=colors[i], label=compiler)) + + # Add some text for labels, title and custom x-axis tick labels, etc. + ax.set_ylabel('Cycles (%)') + ax.set_yticklabels(['{:,.0%}'.format(x) for x in ax.get_yticks()]) + ax.set_title('TITLE') + ax.set_xticks(ind) + ax.set_xticklabels(benches) + ax.legend() + + plt.setp(ax.get_xticklabels(), rotation=30, horizontalalignment='right') + plt.xticks(size=5) + + plt.savefig(f) + +generate_file("measures-host.pdf", host_measures_cols) +generate_file("measures-k1c.pdf", k1c_measures_cols) diff --git a/test/monniaux/genmake.py b/test/monniaux/genmake.py index 8503b1ee..62b97836 100755 --- a/test/monniaux/genmake.py +++ b/test/monniaux/genmake.py @@ -1,4 +1,4 @@ -#!/usr/bin/python3.4 +#!/usr/bin/env python3 """ Custom Makefile generator @@ -8,7 +8,9 @@ See the source for more info. """ from collections import namedtuple +from typing import * import sys +import yaml Optim = namedtuple("Optim", ["short", "full"]) Env = namedtuple("Env", ["compiler", "optimizations", "target"]) @@ -25,51 +27,110 @@ gcc_k1c = Env(compiler = Compiler("gcc", "$(K1C_CC)"), optimizations = [Optim("" ccomp_x86 = Env(compiler = Compiler("ccomp", "$(CCOMP)"), optimizations = [Optim("", "$(CCOMPFLAGS)")], target = "host") ccomp_k1c = Env(compiler = Compiler("ccomp", "$(K1C_CCOMP)"), optimizations = [Optim("", "$(K1C_CCOMPFLAGS)")], target = "k1c") -environments = [gcc_x86, gcc_k1c, ccomp_x86, ccomp_k1c] +environments = [gcc_x86, ccomp_x86, gcc_k1c, ccomp_k1c] ## # Argument parsing ## if len(sys.argv) != 2: - raise Exception("Only 1 argument should be given to this script") -basename = sys.argv[1] + raise Exception("Only 1 argument should be given to this script: the make.proto file") +yaml_file = sys.argv[1] + +with open(yaml_file, "r") as f: + settings = yaml.load(f.read(), Loader=yaml.SafeLoader) + +basename = settings["target"] +objdeps = settings["objdeps"] if "objdeps" in settings else [] +intro = settings["intro"] if "intro" in settings else "" +sources = settings["sources"] if "sources" in settings else None +measures = settings["measures"] if "measures" in settings else [] +name = settings["name"] if "name" in settings else None + +if sources: + intro += "\nsrc=" + sources + +for objdep in objdeps: + if objdep["compiler"] not in ("gcc", "ccomp", "both"): + raise Exception('Invalid compiler specified in make.proto:objdeps, should be either "gcc" or "ccomp" or "both"') ## # Printing the rules ## -def make_product(env, optim): +def make_product(env: Env, optim: Optim) -> str: return basename + "." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target -def make_clock(env, optim): +def make_obj(name: str, env: Env, compiler_short: str) -> str: + return name + "." + compiler_short + "." + env.target + ".o" + +def make_clock(env: Env, optim: Optim) -> str: return "clock.gcc." + env.target -def print_rule(env, optim): - print("{product}: {product}.o ../{clock}.o" - .format(product = make_product(env, optim), clock = make_clock(env, optim))) +def make_sources(env: Env, optim: Optim) -> str: + if sources: + return "$(src:.c=." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target + ".o)" + else: + return "{product}.o".format(product = make_product(env, optim)) + +def print_rule(env: Env, optim: Optim) -> None: + print("{product}: {sources} ../{clock}.o " + .format(product = make_product(env, optim), + sources = make_sources(env, optim), clock = make_clock(env, optim)) + + " ".join([make_obj(objdep["name"], env, (objdep["compiler"] if objdep["compiler"] != "both" else env.compiler.short)) for objdep in objdeps])) print(" {compiler} {flags} $+ -o $@" .format(compiler = env.compiler.full, flags = optim.full)) +def make_env_list(envs: List[Env]) -> str: + return ",".join([(env.compiler.short + ((" " + optim.short) if optim.short != "" else "") + " " + env.target) + for env in environments + for optim in env.optimizations]) + +def print_measure_rule(environments: List[Env], measures: List[Union[List[str], str]]) -> None: + print("measures.csv: $(PRODUCTS_OUT)") + print(' echo "benches, {}" > $@'.format(make_env_list(environments))) + for measure in measures: + display_measure_name = (len(measures) > 1) + if isinstance(measure, list): + measure_name, measure_short = measure + display_measure_name = True + else: + measure_name = measure_short = measure + print(' echo "{name} {measure}"'.format(name=basename if not name else name, measure=measure_short if display_measure_name else ""), end="") + for env in environments: + for optim in env.optimizations: + print(", $$(grep '{measure}' {outfile} | cut -d':' -f2)".format( + measure=measure_name, outfile=make_product(env, optim) + ".out"), end="") + print('>> $@') + products = [] for env in environments: for optim in env.optimizations: - products.append(make_product(env, optim) + ".out") + products.append(make_product(env, optim)) print(""" include ../rules.mk -PRODUCTS?={} +{intro} + +PRODUCTS?={prod} +PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS)) all: $(PRODUCTS) -""".format(" ".join(products))) + +.PHONY: +run: measures.csv + +""".format(intro=intro, prod=" ".join(products))) for env in environments: for optim in env.optimizations: print_rule(env, optim) +print_measure_rule(environments, measures) + + print(""" +.PHONY: clean: - -rm -f *.o *.s *.k1c - -.PHONY: clean + rm -f *.o *.s *.k1c *.csv """) diff --git a/test/monniaux/glibc_qsort/Makefile b/test/monniaux/glibc_qsort/Makefile deleted file mode 100644 index 62902903..00000000 --- a/test/monniaux/glibc_qsort/Makefile +++ /dev/null @@ -1,27 +0,0 @@ -include ../rules.mk - -PRODUCTS=glibc_qsort.gcc.host.out glibc_qsort.ccomp.host.out glibc_qsort.gcc.k1c.out glibc_qsort.gcc.o1.k1c.out glibc_qsort.ccomp.k1c.out glibc_qsort.ccomp.k1c.s glibc_qsort.gcc.k1c.s glibc_qsort.gcc.k1c glibc_qsort.ccomp.k1c - -all: $(PRODUCTS) - -glibc_qsort.gcc.host: glibc_qsort.c glibc_qsort_run.gcc.host.o glibc_qsort.h - $(CC) $(CFLAGS) glibc_qsort.c glibc_qsort_run.gcc.host.o -o $@ - -glibc_qsort.ccomp.host: glibc_qsort.c glibc_qsort_run.gcc.host.o glibc_qsort.h - $(CCOMP) $(CCOMPFLAGS) glibc_qsort.c glibc_qsort_run.gcc.host.o -o $@ - -glibc_qsort.gcc.k1c.s glibc_qsort.ccomp.k1c.s glibc_qsort_run.gcc.k1c.s: glibc_qsort.h - -glibc_qsort.gcc.k1c: glibc_qsort.gcc.k1c.o glibc_qsort_run.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -glibc_qsort.gcc.o1.k1c: glibc_qsort.gcc.o1.k1c.o glibc_qsort_run.gcc.o1.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -glibc_qsort.ccomp.k1c: glibc_qsort.ccomp.k1c.o glibc_qsort_run.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f $(PRODUCTS) glibc_qsort.gcc.k1c.o glibc_qsort.ccomp.k1c.o glibc_qsort_run.gcc.k1c.o glibc_qsort_run.gcc.k1c.s - -.PHONY: clean diff --git a/test/monniaux/glibc_qsort/glibc_qsort_run.c b/test/monniaux/glibc_qsort/glibc_qsort_run.c index 92bfba4e..7fcb8130 100644 --- a/test/monniaux/glibc_qsort/glibc_qsort_run.c +++ b/test/monniaux/glibc_qsort/glibc_qsort_run.c @@ -41,7 +41,7 @@ int main (void) { quicksort(vec, len, sizeof(data), data_compare, NULL); quicksort_time = get_cycle() - quicksort_time; printf("sorted=%s\n" - "quicksort_time=%" PRIu64 "\n", + "quicksort_time:%" PRIu64 "\n", data_vec_is_sorted(vec, len)?"true":"false", quicksort_time); free(vec); diff --git a/test/monniaux/glibc_qsort/make.proto b/test/monniaux/glibc_qsort/make.proto new file mode 100644 index 00000000..763e77f5 --- /dev/null +++ b/test/monniaux/glibc_qsort/make.proto @@ -0,0 +1,3 @@ +objdeps: [{name: glibc_qsort_run, compiler: gcc}] +target: glibc_qsort +measures: [quicksort_time] diff --git a/test/monniaux/heapsort/Makefile b/test/monniaux/heapsort/Makefile deleted file mode 100644 index 74eb1dea..00000000 --- a/test/monniaux/heapsort/Makefile +++ /dev/null @@ -1,30 +0,0 @@ -include ../rules.mk - -PRODUCTS=heapsort.gcc.host.out heapsort.ccomp.host.out heapsort.gcc.o1.k1c.out heapsort.gcc.k1c.out heapsort.ccomp.k1c.out heapsort.ccomp.k1c.s heapsort.gcc.k1c.s heapsort.gcc.k1c heapsort.ccomp.k1c - -all: $(PRODUCTS) - -heapsort.gcc.host: heapsort.c heapsort_run.gcc.host.o heapsort.h - $(CC) $(CFLAGS) heapsort.c heapsort_run.gcc.host.o -o $@ - -heapsort.ccomp.host: heapsort.c heapsort_run.gcc.host.o heapsort.h - $(CCOMP) $(CCOMPFLAGS) heapsort.c heapsort_run.gcc.host.o -o $@ - -heapsort.gcc.k1c.s heapsort.ccomp.k1c.s heapsort_run.gcc.k1c.s: heapsort.h - -heapsort.gcc.o1.k1c: heapsort.gcc.o1.k1c.o heapsort_run.gcc.o1.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -heapsort.gcc.k1c: heapsort.gcc.k1c.o heapsort_run.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -heapsort.ccomp.k1c: heapsort.ccomp.k1c.o heapsort_run.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -%.k1c.out: %.k1c - k1-cluster --cycle-based -- $< | tee $@ - -clean: - $(RM) -f $(PRODUCTS) heapsort.gcc.k1c.o heapsort.ccomp.k1c.o heapsort_run.gcc.k1c.o heapsort_run.gcc.k1c.s - -.PHONY: clean diff --git a/test/monniaux/heapsort/heapsort_run.c b/test/monniaux/heapsort/heapsort_run.c index 76378067..053822a3 100644 --- a/test/monniaux/heapsort/heapsort_run.c +++ b/test/monniaux/heapsort/heapsort_run.c @@ -13,7 +13,7 @@ int main (void) { heapsort(vec, len); heapsort_time = get_cycle() - heapsort_time; printf("sorted=%s\n" - "heapsort_time=%" PRIu64 "\n", + "heapsort_time:%" PRIu64 "\n", data_vec_is_sorted(vec, len)?"true":"false", heapsort_time); free(vec); diff --git a/test/monniaux/heapsort/make.proto b/test/monniaux/heapsort/make.proto new file mode 100644 index 00000000..0b5972d6 --- /dev/null +++ b/test/monniaux/heapsort/make.proto @@ -0,0 +1,3 @@ +objdeps: [{name: heapsort_run, compiler: gcc}] +target: heapsort +measures: [heapsort_time] diff --git a/test/monniaux/heptagon_radio_transmitter/_main.c b/test/monniaux/heptagon_radio_transmitter/_main.c new file mode 100644 index 00000000..635d660f --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/_main.c @@ -0,0 +1,74 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include "_main.h" +#include "../clock.h" +#include "../dm_random.c" + +static inline int get_bool(void) { + return dm_random_uint32() & 1; +} + +Radiotrans__main_mem mem; +int main(int argc, char** argv) { + int step_c; + int step_max; + int enter_tx; + int enter_rx; + int exit_rx; + int calibrate; + int sleep; + int wake_up; + int irq_tx_done; + int irq_on_packet; + int irq_end_of_packet; + int irq_end_of_calibration; + int irq_fifo_threshold; + int adc_on; + int adc_off; + Radiotrans__main_out _res; + step_c = 0; + step_max = 1000; + if ((argc==2)) { + step_max = atoi(argv[1]); + }; + + clock_prepare(); + clock_start(); + Radiotrans__main_reset(&mem); + while ((!(step_max)||(step_c<step_max))) { + step_c = (step_c+1); + + enter_tx = get_bool(); + enter_rx = get_bool(); + exit_rx = get_bool(); + calibrate = get_bool(); + sleep = get_bool(); + wake_up = get_bool(); + irq_tx_done = get_bool(); + irq_on_packet = get_bool(); + irq_end_of_packet = get_bool(); + irq_end_of_calibration = get_bool(); + irq_fifo_threshold = get_bool(); + adc_on = get_bool(); + adc_off = get_bool(); + + Radiotrans__main_step(enter_tx, enter_rx, exit_rx, calibrate, sleep, + wake_up, irq_tx_done, irq_on_packet, + irq_end_of_packet, irq_end_of_calibration, + irq_fifo_threshold, adc_on, adc_off, &_res, &mem); +#if 0 + printf("%d\n", _res.a_on); + printf("%d\n", _res.red); + fflush(stdout); +#endif + }; + clock_stop(); + print_total_clock(); + return 0; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/_main.h b/test/monniaux/heptagon_radio_transmitter/_main.h new file mode 100644 index 00000000..65abec74 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/_main.h @@ -0,0 +1,9 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#ifndef _MAIN_H +#define _MAIN_H + +#include "radiotrans.h" +#endif // _MAIN_H diff --git a/test/monniaux/heptagon_radio_transmitter/pervasives.h b/test/monniaux/heptagon_radio_transmitter/pervasives.h new file mode 100644 index 00000000..f6d197e4 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/pervasives.h @@ -0,0 +1,45 @@ +/***********************************************************************/ +/* */ +/* Heptagon */ +/* */ +/* Gwenael Delaval, LIG/INRIA, UJF */ +/* Leonard Gerard, Parkas, ENS */ +/* Adrien Guatto, Parkas, ENS */ +/* Cedric Pasteur, Parkas, ENS */ +/* Marc Pouzet, Parkas, ENS */ +/* */ +/* Copyright 2012 ENS, INRIA, UJF */ +/* */ +/* This file is part of the Heptagon compiler. */ +/* */ +/* Heptagon is free software: you can redistribute it and/or modify it */ +/* under the terms of the GNU General Public License as published by */ +/* the Free Software Foundation, either version 3 of the License, or */ +/* (at your option) any later version. */ +/* */ +/* Heptagon is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU General Public License for more details. */ +/* */ +/* You should have received a copy of the GNU General Public License */ +/* along with Heptagon. If not, see <http://www.gnu.org/licenses/> */ +/* */ +/***********************************************************************/ + +/* Pervasives module for the Heptagon compiler */ + +#ifndef DECADES_PERVASIVES_H +#define DECADES_PERVASIVES_H + +typedef float real; + +/* between(i, n) returns idx between 0 and n-1. */ +static inline int between(int idx, int n) +{ + int o = (idx >= n) ? n-1 : (idx < 0 ? 0 : idx); + return o; +} + +#endif + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans.c b/test/monniaux/heptagon_radio_transmitter/radiotrans.c new file mode 100644 index 00000000..30d4f62d --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans.c @@ -0,0 +1,571 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include "radiotrans.h" + +void Radiotrans__transceiver_reset(Radiotrans__transceiver_mem* self) { + self->ck = Radiotrans__St_Idle; + self->pnr = false; +} + +void Radiotrans__transceiver_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, + int irq_end_of_calibration, + int irq_fifo_threshold, int ok, + Radiotrans__transceiver_out* _out, + Radiotrans__transceiver_mem* self) { + + int v_2; + Radiotrans__st v_1; + int v; + int v_3; + int v_13; + Radiotrans__st v_12; + int v_11; + Radiotrans__st v_10; + int v_9; + Radiotrans__st v_8; + int v_7; + int v_6; + int v_5; + int v_4; + int nr_St_Rx_Packet; + Radiotrans__st ns_St_Rx_Packet; + int red_St_Rx_Packet; + int nr_St_Rx; + Radiotrans__st ns_St_Rx; + int red_St_Rx; + int nr_St_Sleep; + Radiotrans__st ns_St_Sleep; + int red_St_Sleep; + int nr_St_Calibrate; + Radiotrans__st ns_St_Calibrate; + int red_St_Calibrate; + int nr_St_Tx; + Radiotrans__st ns_St_Tx; + int red_St_Tx; + int nr_St_Idle; + Radiotrans__st ns_St_Idle; + int red_St_Idle; + Radiotrans__st ns; + int r; + int nr; + r = self->pnr; + switch (self->ck) { + case Radiotrans__St_Rx_Packet: + if (irq_end_of_packet) { + ns_St_Rx_Packet = Radiotrans__St_Idle; + nr_St_Rx_Packet = true; + } else { + ns_St_Rx_Packet = Radiotrans__St_Rx_Packet; + nr_St_Rx_Packet = false; + }; + red_St_Rx_Packet = true; + ns = ns_St_Rx_Packet; + nr = nr_St_Rx_Packet; + _out->red = red_St_Rx_Packet; + break; + case Radiotrans__St_Rx: + v = (exit_rx&&ok); + if (v) { + v_1 = Radiotrans__St_Idle; + } else { + v_1 = Radiotrans__St_Rx; + }; + if (irq_on_packet) { + ns_St_Rx = Radiotrans__St_Rx_Packet; + } else { + ns_St_Rx = v_1; + }; + if (v) { + v_2 = true; + } else { + v_2 = false; + }; + if (irq_on_packet) { + nr_St_Rx = true; + } else { + nr_St_Rx = v_2; + }; + red_St_Rx = true; + ns = ns_St_Rx; + nr = nr_St_Rx; + _out->red = red_St_Rx; + break; + case Radiotrans__St_Sleep: + v_3 = (wake_up&&ok); + if (v_3) { + ns_St_Sleep = Radiotrans__St_Idle; + nr_St_Sleep = true; + } else { + ns_St_Sleep = Radiotrans__St_Sleep; + nr_St_Sleep = false; + }; + red_St_Sleep = false; + ns = ns_St_Sleep; + nr = nr_St_Sleep; + _out->red = red_St_Sleep; + break; + case Radiotrans__St_Calibrate: + if (irq_end_of_calibration) { + ns_St_Calibrate = Radiotrans__St_Idle; + nr_St_Calibrate = true; + } else { + ns_St_Calibrate = Radiotrans__St_Calibrate; + nr_St_Calibrate = false; + }; + red_St_Calibrate = false; + ns = ns_St_Calibrate; + nr = nr_St_Calibrate; + _out->red = red_St_Calibrate; + break; + case Radiotrans__St_Tx: + if (irq_tx_done) { + ns_St_Tx = Radiotrans__St_Idle; + nr_St_Tx = true; + } else { + ns_St_Tx = Radiotrans__St_Tx; + nr_St_Tx = false; + }; + red_St_Tx = true; + ns = ns_St_Tx; + nr = nr_St_Tx; + _out->red = red_St_Tx; + break; + case Radiotrans__St_Idle: + v_4 = (enter_tx&&ok); + v_5 = (calibrate&&ok); + v_6 = (sleep&&ok); + v_7 = (enter_rx&&ok); + if (v_7) { + v_8 = Radiotrans__St_Rx; + } else { + v_8 = Radiotrans__St_Idle; + }; + if (v_6) { + v_10 = Radiotrans__St_Sleep; + } else { + v_10 = v_8; + }; + if (v_5) { + v_12 = Radiotrans__St_Calibrate; + } else { + v_12 = v_10; + }; + if (v_4) { + ns_St_Idle = Radiotrans__St_Tx; + } else { + ns_St_Idle = v_12; + }; + ns = ns_St_Idle; + if (v_7) { + v_9 = true; + } else { + v_9 = false; + }; + if (v_6) { + v_11 = true; + } else { + v_11 = v_9; + }; + if (v_5) { + v_13 = true; + } else { + v_13 = v_11; + }; + if (v_4) { + nr_St_Idle = true; + } else { + nr_St_Idle = v_13; + }; + nr = nr_St_Idle; + red_St_Idle = false; + _out->red = red_St_Idle; + break; + default: + break; + }; + self->ck = ns; + self->pnr = nr;; +} + +void Radiotrans__adc_reset(Radiotrans__adc_mem* self) { + self->ck = Radiotrans__St_1_Off; + self->pnr = false; +} + +void Radiotrans__adc_step(int adc_on, int adc_off, int ok, + Radiotrans__adc_out* _out, + Radiotrans__adc_mem* self) { + + int v; + int v_14; + int nr_St_1_On; + Radiotrans__st_1 ns_St_1_On; + int o_St_1_On; + int nr_St_1_Off; + Radiotrans__st_1 ns_St_1_Off; + int o_St_1_Off; + Radiotrans__st_1 ns; + int r; + int nr; + r = self->pnr; + switch (self->ck) { + case Radiotrans__St_1_On: + v = (adc_off&&ok); + if (v) { + ns_St_1_On = Radiotrans__St_1_Off; + nr_St_1_On = true; + } else { + ns_St_1_On = Radiotrans__St_1_On; + nr_St_1_On = false; + }; + o_St_1_On = true; + ns = ns_St_1_On; + nr = nr_St_1_On; + _out->o = o_St_1_On; + break; + case Radiotrans__St_1_Off: + v_14 = (adc_on&&ok); + if (v_14) { + ns_St_1_Off = Radiotrans__St_1_On; + } else { + ns_St_1_Off = Radiotrans__St_1_Off; + }; + ns = ns_St_1_Off; + if (v_14) { + nr_St_1_Off = true; + } else { + nr_St_1_Off = false; + }; + nr = nr_St_1_Off; + o_St_1_Off = false; + _out->o = o_St_1_Off; + break; + default: + break; + }; + self->ck = ns; + self->pnr = nr;; +} + +void Radiotrans__main_reset(Radiotrans__main_mem* self) { + self->ck = Radiotrans__St_3_Idle; + self->pnr_1 = false; + self->ck_1 = Radiotrans__St_2_Off; + self->pnr = false; +} + +void Radiotrans__main_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, int irq_end_of_calibration, + int irq_fifo_threshold, int adc_on, int adc_off, + Radiotrans__main_out* _out, + Radiotrans__main_mem* self) { + Radiotrans_controller__main_ctrlr0_out Radiotrans_controller__main_ctrlr0_out_st; + + int v_15; + int v; + int ok_r; + int ok_a; + int v_18; + Radiotrans__st_3 v_17; + int v_16; + int v_19; + int v_29; + Radiotrans__st_3 v_28; + int v_27; + Radiotrans__st_3 v_26; + int v_25; + Radiotrans__st_3 v_24; + int v_23; + int v_22; + int v_21; + int v_20; + int nr_1_St_3_Rx_Packet; + Radiotrans__st_3 ns_1_St_3_Rx_Packet; + int red_1_St_3_Rx_Packet; + int nr_1_St_3_Rx; + Radiotrans__st_3 ns_1_St_3_Rx; + int red_1_St_3_Rx; + int nr_1_St_3_Sleep; + Radiotrans__st_3 ns_1_St_3_Sleep; + int red_1_St_3_Sleep; + int nr_1_St_3_Calibrate; + Radiotrans__st_3 ns_1_St_3_Calibrate; + int red_1_St_3_Calibrate; + int nr_1_St_3_Tx; + Radiotrans__st_3 ns_1_St_3_Tx; + int red_1_St_3_Tx; + int nr_1_St_3_Idle; + Radiotrans__st_3 ns_1_St_3_Idle; + int red_1_St_3_Idle; + int v_30; + int v_31; + int nr_St_2_On; + Radiotrans__st_2 ns_St_2_On; + int o_St_2_On; + int nr_St_2_Off; + Radiotrans__st_2 ns_St_2_Off; + int o_St_2_Off; + Radiotrans__st_3 ns_1; + int r_1; + int nr_1; + Radiotrans__st_2 ns; + int r; + int nr; + int adc_on_1; + int adc_off_1; + int ok_1; + int o; + int enter_tx_1; + int enter_rx_1; + int exit_rx_1; + int calibrate_1; + int sleep_1; + int wake_up_1; + int irq_tx_done_1; + int irq_on_packet_1; + int irq_end_of_packet_1; + int irq_end_of_calibration_1; + int irq_fifo_threshold_1; + int ok; + int red_1; + r_1 = self->pnr_1; + irq_fifo_threshold_1 = irq_fifo_threshold; + irq_end_of_calibration_1 = irq_end_of_calibration; + irq_end_of_packet_1 = irq_end_of_packet; + irq_on_packet_1 = irq_on_packet; + irq_tx_done_1 = irq_tx_done; + wake_up_1 = wake_up; + sleep_1 = sleep; + calibrate_1 = calibrate; + exit_rx_1 = exit_rx; + enter_rx_1 = enter_rx; + enter_tx_1 = enter_tx; + r = self->pnr; + adc_off_1 = adc_off; + adc_on_1 = adc_on; + switch (self->ck) { + case Radiotrans__St_3_Rx_Packet: + if (irq_end_of_packet_1) { + ns_1_St_3_Rx_Packet = Radiotrans__St_3_Idle; + nr_1_St_3_Rx_Packet = true; + } else { + ns_1_St_3_Rx_Packet = Radiotrans__St_3_Rx_Packet; + nr_1_St_3_Rx_Packet = false; + }; + red_1_St_3_Rx_Packet = true; + red_1 = red_1_St_3_Rx_Packet; + break; + case Radiotrans__St_3_Rx: + red_1_St_3_Rx = true; + red_1 = red_1_St_3_Rx; + break; + case Radiotrans__St_3_Sleep: + red_1_St_3_Sleep = false; + red_1 = red_1_St_3_Sleep; + break; + case Radiotrans__St_3_Calibrate: + if (irq_end_of_calibration_1) { + ns_1_St_3_Calibrate = Radiotrans__St_3_Idle; + nr_1_St_3_Calibrate = true; + } else { + ns_1_St_3_Calibrate = Radiotrans__St_3_Calibrate; + nr_1_St_3_Calibrate = false; + }; + red_1_St_3_Calibrate = false; + red_1 = red_1_St_3_Calibrate; + break; + case Radiotrans__St_3_Tx: + if (irq_tx_done_1) { + ns_1_St_3_Tx = Radiotrans__St_3_Idle; + nr_1_St_3_Tx = true; + } else { + ns_1_St_3_Tx = Radiotrans__St_3_Tx; + nr_1_St_3_Tx = false; + }; + red_1_St_3_Tx = true; + red_1 = red_1_St_3_Tx; + break; + case Radiotrans__St_3_Idle: + red_1_St_3_Idle = false; + red_1 = red_1_St_3_Idle; + break; + default: + break; + }; + _out->red = red_1; + switch (self->ck_1) { + case Radiotrans__St_2_On: + o_St_2_On = true; + o = o_St_2_On; + break; + case Radiotrans__St_2_Off: + o_St_2_Off = false; + o = o_St_2_Off; + break; + default: + break; + }; + _out->a_on = o; + Radiotrans_controller__main_ctrlr0_step(adc_off, adc_on, calibrate, + self->ck, self->ck_1, enter_rx, + enter_tx, exit_rx, + irq_end_of_calibration, + irq_end_of_packet, + irq_fifo_threshold, irq_on_packet, + irq_tx_done, self->pnr, + self->pnr_1, sleep, wake_up, + &Radiotrans_controller__main_ctrlr0_out_st); + ok_a = Radiotrans_controller__main_ctrlr0_out_st.ok_a; + ok_r = Radiotrans_controller__main_ctrlr0_out_st.ok_r; + ok = ok_r; + ok_1 = ok_a; + switch (self->ck) { + case Radiotrans__St_3_Rx: + v_16 = (exit_rx_1&&ok); + if (v_16) { + v_17 = Radiotrans__St_3_Idle; + } else { + v_17 = Radiotrans__St_3_Rx; + }; + if (irq_on_packet_1) { + ns_1_St_3_Rx = Radiotrans__St_3_Rx_Packet; + } else { + ns_1_St_3_Rx = v_17; + }; + if (v_16) { + v_18 = true; + } else { + v_18 = false; + }; + if (irq_on_packet_1) { + nr_1_St_3_Rx = true; + } else { + nr_1_St_3_Rx = v_18; + }; + ns_1 = ns_1_St_3_Rx; + nr_1 = nr_1_St_3_Rx; + break; + case Radiotrans__St_3_Sleep: + v_19 = (wake_up_1&&ok); + if (v_19) { + ns_1_St_3_Sleep = Radiotrans__St_3_Idle; + nr_1_St_3_Sleep = true; + } else { + ns_1_St_3_Sleep = Radiotrans__St_3_Sleep; + nr_1_St_3_Sleep = false; + }; + ns_1 = ns_1_St_3_Sleep; + nr_1 = nr_1_St_3_Sleep; + break; + case Radiotrans__St_3_Idle: + v_20 = (enter_tx_1&&ok); + v_21 = (calibrate_1&&ok); + v_22 = (sleep_1&&ok); + v_23 = (enter_rx_1&&ok); + if (v_23) { + v_24 = Radiotrans__St_3_Rx; + } else { + v_24 = Radiotrans__St_3_Idle; + }; + if (v_22) { + v_26 = Radiotrans__St_3_Sleep; + } else { + v_26 = v_24; + }; + if (v_21) { + v_28 = Radiotrans__St_3_Calibrate; + } else { + v_28 = v_26; + }; + if (v_20) { + ns_1_St_3_Idle = Radiotrans__St_3_Tx; + } else { + ns_1_St_3_Idle = v_28; + }; + ns_1 = ns_1_St_3_Idle; + if (v_23) { + v_25 = true; + } else { + v_25 = false; + }; + if (v_22) { + v_27 = true; + } else { + v_27 = v_25; + }; + if (v_21) { + v_29 = true; + } else { + v_29 = v_27; + }; + if (v_20) { + nr_1_St_3_Idle = true; + } else { + nr_1_St_3_Idle = v_29; + }; + nr_1 = nr_1_St_3_Idle; + break; + case Radiotrans__St_3_Rx_Packet: + ns_1 = ns_1_St_3_Rx_Packet; + nr_1 = nr_1_St_3_Rx_Packet; + break; + case Radiotrans__St_3_Calibrate: + ns_1 = ns_1_St_3_Calibrate; + nr_1 = nr_1_St_3_Calibrate; + break; + case Radiotrans__St_3_Tx: + ns_1 = ns_1_St_3_Tx; + nr_1 = nr_1_St_3_Tx; + break; + default: + break; + }; + switch (self->ck_1) { + case Radiotrans__St_2_On: + v_30 = (adc_off_1&&ok_1); + if (v_30) { + ns_St_2_On = Radiotrans__St_2_Off; + nr_St_2_On = true; + } else { + ns_St_2_On = Radiotrans__St_2_On; + nr_St_2_On = false; + }; + ns = ns_St_2_On; + nr = nr_St_2_On; + break; + case Radiotrans__St_2_Off: + v_31 = (adc_on_1&&ok_1); + if (v_31) { + ns_St_2_Off = Radiotrans__St_2_On; + } else { + ns_St_2_Off = Radiotrans__St_2_Off; + }; + ns = ns_St_2_Off; + if (v_31) { + nr_St_2_Off = true; + } else { + nr_St_2_Off = false; + }; + nr = nr_St_2_Off; + break; + default: + break; + }; + self->ck = ns_1; + self->pnr_1 = nr_1; + self->ck_1 = ns; + self->pnr = nr; + v = (_out->a_on&&_out->red); + v_15 = !(v);; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans.h b/test/monniaux/heptagon_radio_transmitter/radiotrans.h new file mode 100644 index 00000000..1d68ad5c --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans.h @@ -0,0 +1,67 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#ifndef RADIOTRANS_H +#define RADIOTRANS_H + +#include "radiotrans_types.h" +#include "radiotrans_controller.h" +typedef struct Radiotrans__transceiver_mem { + Radiotrans__st ck; + int pnr; +} Radiotrans__transceiver_mem; + +typedef struct Radiotrans__transceiver_out { + int red; +} Radiotrans__transceiver_out; + +void Radiotrans__transceiver_reset(Radiotrans__transceiver_mem* self); + +void Radiotrans__transceiver_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, + int irq_end_of_calibration, + int irq_fifo_threshold, int ok, + Radiotrans__transceiver_out* _out, + Radiotrans__transceiver_mem* self); + +typedef struct Radiotrans__adc_mem { + Radiotrans__st_1 ck; + int pnr; +} Radiotrans__adc_mem; + +typedef struct Radiotrans__adc_out { + int o; +} Radiotrans__adc_out; + +void Radiotrans__adc_reset(Radiotrans__adc_mem* self); + +void Radiotrans__adc_step(int adc_on, int adc_off, int ok, + Radiotrans__adc_out* _out, + Radiotrans__adc_mem* self); + +typedef struct Radiotrans__main_mem { + Radiotrans__st_3 ck; + Radiotrans__st_2 ck_1; + int pnr_1; + int pnr; +} Radiotrans__main_mem; + +typedef struct Radiotrans__main_out { + int a_on; + int red; +} Radiotrans__main_out; + +void Radiotrans__main_reset(Radiotrans__main_mem* self); + +void Radiotrans__main_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, int irq_end_of_calibration, + int irq_fifo_threshold, int adc_on, int adc_off, + Radiotrans__main_out* _out, + Radiotrans__main_mem* self); + +#endif // RADIOTRANS_H diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c new file mode 100644 index 00000000..8cc6d512 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c @@ -0,0 +1,160 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include "radiotrans_controller.h" + +void Radiotrans_controller__main_ctrlr0_step(int adc_off, int adc_on, + int calibrate, + Radiotrans__st_3 ck, + Radiotrans__st_2 ck_1, + int enter_rx, int enter_tx, + int exit_rx, + int irq_end_of_calibration, + int irq_end_of_packet, + int irq_fifo_threshold, + int irq_on_packet, + int irq_tx_done, int pnr, + int pnr_1, int sleep, + int wake_up, + Radiotrans_controller__main_ctrlr0_out* _out) { + + int v_22; + int v_21; + int v_20; + int v_19; + int v_18; + int v_17; + int v_16; + int v_15; + int v_14; + int v_13; + int v_12; + int v_11; + int v_10; + int v_9; + int v_8; + int v_7; + int v_6; + int v_5; + int v_4; + int v_3; + int v_2; + int v_1; + int v; + int l52; + int l51; + int l50; + int l49; + int l48; + int l47; + int l46; + int l45; + int l44; + int l43; + int l42; + int l41; + int l40; + int l39; + int l38; + int l37; + int l36; + int l35; + int l34; + int l33; + int l32; + v_22 = (ck==Radiotrans__St_3_Rx_Packet); + v_21 = !(adc_on); + l51 = (v_21||irq_end_of_packet); + v_20 = (ck==Radiotrans__St_3_Tx); + v_19 = !(adc_on); + l49 = (v_19||irq_tx_done); + v_18 = (ck==Radiotrans__St_3_Rx); + v_17 = !(adc_on); + v_16 = !(adc_on); + v_15 = !(adc_on); + v_14 = !(irq_on_packet); + l45 = (v_14||v_15); + if (exit_rx) { + l46 = l45; + } else { + l46 = v_16; + }; + v_12 = (ck==Radiotrans__St_3_Idle); + v_13 = !(v_12); + v_11 = (ck_1==Radiotrans__St_2_On); + v_9 = !(adc_on); + v_8 = !(adc_on); + v_7 = !(enter_tx); + l38 = (v_7||v_8); + if (sleep) { + l39 = l38; + } else { + l39 = v_9; + }; + if (enter_rx) { + l40 = l39; + } else { + l40 = l38; + }; + if (calibrate) { + l41 = l38; + } else { + l41 = l40; + }; + v_5 = (ck==Radiotrans__St_3_Rx); + v_3 = (ck==Radiotrans__St_3_Calibrate); + v_2 = (ck==Radiotrans__St_3_Sleep); + v_4 = (v_2||v_3); + v_6 = (v_4||v_5); + v_1 = (ck_1==Radiotrans__St_2_Off); + v = !(enter_tx); + l32 = (v||adc_off); + if (sleep) { + l33 = l32; + } else { + l33 = adc_off; + }; + if (enter_rx) { + l34 = l33; + } else { + l34 = l32; + }; + if (calibrate) { + l35 = l32; + } else { + l35 = l34; + }; + l36 = (v_1||l35); + l37 = (v_6||l36); + _out->ok_r = l37; + if (_out->ok_r) { + l47 = l46; + } else { + l47 = v_17; + }; + v_10 = !(_out->ok_r); + l42 = (v_10||l41); + l43 = (v_11||l42); + l44 = (v_13||l43); + if (v_18) { + l48 = l47; + } else { + l48 = l44; + }; + if (v_20) { + l50 = l49; + } else { + l50 = l48; + }; + if (v_22) { + l52 = l51; + } else { + l52 = l50; + }; + _out->ok_a = l52;; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h new file mode 100644 index 00000000..45681ada --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h @@ -0,0 +1,30 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#ifndef RADIOTRANS_CONTROLLER_H +#define RADIOTRANS_CONTROLLER_H + +#include "radiotrans_controller_types.h" +#include "radiotrans.h" +typedef struct Radiotrans_controller__main_ctrlr0_out { + int ok_a; + int ok_r; +} Radiotrans_controller__main_ctrlr0_out; + +void Radiotrans_controller__main_ctrlr0_step(int adc_off, int adc_on, + int calibrate, + Radiotrans__st_3 ck, + Radiotrans__st_2 ck_1, + int enter_rx, int enter_tx, + int exit_rx, + int irq_end_of_calibration, + int irq_end_of_packet, + int irq_fifo_threshold, + int irq_on_packet, + int irq_tx_done, int pnr, + int pnr_1, int sleep, + int wake_up, + Radiotrans_controller__main_ctrlr0_out* _out); + +#endif // RADIOTRANS_CONTROLLER_H diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c new file mode 100644 index 00000000..a3c3972f --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c @@ -0,0 +1,9 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include "radiotrans_controller_types.h" + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h new file mode 100644 index 00000000..9a081213 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h @@ -0,0 +1,12 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#ifndef RADIOTRANS_CONTROLLER_TYPES_H +#define RADIOTRANS_CONTROLLER_TYPES_H + +#include "stdbool.h" +#include "assert.h" +#include "pervasives.h" +#include "radiotrans_types.h" +#endif // RADIOTRANS_CONTROLLER_TYPES_H diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_types.c b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.c new file mode 100644 index 00000000..cc62575d --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.c @@ -0,0 +1,149 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include "radiotrans_types.h" + +Radiotrans__st_3 Radiotrans__st_3_of_string(char* s) { + if ((strcmp(s, "St_3_Tx")==0)) { + return Radiotrans__St_3_Tx; + }; + if ((strcmp(s, "St_3_Sleep")==0)) { + return Radiotrans__St_3_Sleep; + }; + if ((strcmp(s, "St_3_Rx_Packet")==0)) { + return Radiotrans__St_3_Rx_Packet; + }; + if ((strcmp(s, "St_3_Rx")==0)) { + return Radiotrans__St_3_Rx; + }; + if ((strcmp(s, "St_3_Idle")==0)) { + return Radiotrans__St_3_Idle; + }; + if ((strcmp(s, "St_3_Calibrate")==0)) { + return Radiotrans__St_3_Calibrate; + }; +} + +char* string_of_Radiotrans__st_3(Radiotrans__st_3 x, char* buf) { + switch (x) { + case Radiotrans__St_3_Tx: + strcpy(buf, "St_3_Tx"); + break; + case Radiotrans__St_3_Sleep: + strcpy(buf, "St_3_Sleep"); + break; + case Radiotrans__St_3_Rx_Packet: + strcpy(buf, "St_3_Rx_Packet"); + break; + case Radiotrans__St_3_Rx: + strcpy(buf, "St_3_Rx"); + break; + case Radiotrans__St_3_Idle: + strcpy(buf, "St_3_Idle"); + break; + case Radiotrans__St_3_Calibrate: + strcpy(buf, "St_3_Calibrate"); + break; + default: + break; + }; + return buf; +} + +Radiotrans__st_2 Radiotrans__st_2_of_string(char* s) { + if ((strcmp(s, "St_2_On")==0)) { + return Radiotrans__St_2_On; + }; + if ((strcmp(s, "St_2_Off")==0)) { + return Radiotrans__St_2_Off; + }; +} + +char* string_of_Radiotrans__st_2(Radiotrans__st_2 x, char* buf) { + switch (x) { + case Radiotrans__St_2_On: + strcpy(buf, "St_2_On"); + break; + case Radiotrans__St_2_Off: + strcpy(buf, "St_2_Off"); + break; + default: + break; + }; + return buf; +} + +Radiotrans__st_1 Radiotrans__st_1_of_string(char* s) { + if ((strcmp(s, "St_1_On")==0)) { + return Radiotrans__St_1_On; + }; + if ((strcmp(s, "St_1_Off")==0)) { + return Radiotrans__St_1_Off; + }; +} + +char* string_of_Radiotrans__st_1(Radiotrans__st_1 x, char* buf) { + switch (x) { + case Radiotrans__St_1_On: + strcpy(buf, "St_1_On"); + break; + case Radiotrans__St_1_Off: + strcpy(buf, "St_1_Off"); + break; + default: + break; + }; + return buf; +} + +Radiotrans__st Radiotrans__st_of_string(char* s) { + if ((strcmp(s, "St_Tx")==0)) { + return Radiotrans__St_Tx; + }; + if ((strcmp(s, "St_Sleep")==0)) { + return Radiotrans__St_Sleep; + }; + if ((strcmp(s, "St_Rx_Packet")==0)) { + return Radiotrans__St_Rx_Packet; + }; + if ((strcmp(s, "St_Rx")==0)) { + return Radiotrans__St_Rx; + }; + if ((strcmp(s, "St_Idle")==0)) { + return Radiotrans__St_Idle; + }; + if ((strcmp(s, "St_Calibrate")==0)) { + return Radiotrans__St_Calibrate; + }; +} + +char* string_of_Radiotrans__st(Radiotrans__st x, char* buf) { + switch (x) { + case Radiotrans__St_Tx: + strcpy(buf, "St_Tx"); + break; + case Radiotrans__St_Sleep: + strcpy(buf, "St_Sleep"); + break; + case Radiotrans__St_Rx_Packet: + strcpy(buf, "St_Rx_Packet"); + break; + case Radiotrans__St_Rx: + strcpy(buf, "St_Rx"); + break; + case Radiotrans__St_Idle: + strcpy(buf, "St_Idle"); + break; + case Radiotrans__St_Calibrate: + strcpy(buf, "St_Calibrate"); + break; + default: + break; + }; + return buf; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_types.h b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.h new file mode 100644 index 00000000..826ed65c --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.h @@ -0,0 +1,56 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#ifndef RADIOTRANS_TYPES_H +#define RADIOTRANS_TYPES_H + +#include "stdbool.h" +#include "assert.h" +#include "pervasives.h" +#include "radiotrans_controller_types.h" +typedef enum { + Radiotrans__St_3_Tx, + Radiotrans__St_3_Sleep, + Radiotrans__St_3_Rx_Packet, + Radiotrans__St_3_Rx, + Radiotrans__St_3_Idle, + Radiotrans__St_3_Calibrate +} Radiotrans__st_3; + +Radiotrans__st_3 Radiotrans__st_3_of_string(char* s); + +char* string_of_Radiotrans__st_3(Radiotrans__st_3 x, char* buf); + +typedef enum { + Radiotrans__St_2_On, + Radiotrans__St_2_Off +} Radiotrans__st_2; + +Radiotrans__st_2 Radiotrans__st_2_of_string(char* s); + +char* string_of_Radiotrans__st_2(Radiotrans__st_2 x, char* buf); + +typedef enum { + Radiotrans__St_1_On, + Radiotrans__St_1_Off +} Radiotrans__st_1; + +Radiotrans__st_1 Radiotrans__st_1_of_string(char* s); + +char* string_of_Radiotrans__st_1(Radiotrans__st_1 x, char* buf); + +typedef enum { + Radiotrans__St_Tx, + Radiotrans__St_Sleep, + Radiotrans__St_Rx_Packet, + Radiotrans__St_Rx, + Radiotrans__St_Idle, + Radiotrans__St_Calibrate +} Radiotrans__st; + +Radiotrans__st Radiotrans__st_of_string(char* s); + +char* string_of_Radiotrans__st(Radiotrans__st x, char* buf); + +#endif // RADIOTRANS_TYPES_H diff --git a/test/monniaux/idea/Makefile b/test/monniaux/idea/Makefile deleted file mode 100644 index c638f22f..00000000 --- a/test/monniaux/idea/Makefile +++ /dev/null @@ -1,27 +0,0 @@ -include ../rules.mk - -PRODUCTS=idea.gcc.host.out idea.ccomp.host.out idea.gcc.o1.k1c.out idea.gcc.k1c.out idea.ccomp.k1c.out idea.ccomp.k1c.s idea.gcc.k1c.s idea.gcc.k1c idea.ccomp.k1c - -all: $(PRODUCTS) - -idea.gcc.host: idea.c idea.h ../clock.gcc.host.o - $(CC) $(CFLAGS) idea.c ../clock.gcc.host.o -o $@ - -idea.ccomp.host: idea.c idea.h ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) idea.c ../clock.gcc.host.o -o $@ - -idea.gcc.k1c.s idea.ccomp.k1c.s idea_run.gcc.k1c.s: idea.h - -idea.gcc.k1c: idea.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -idea.gcc.o1.k1c: idea.gcc.o1.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -idea.ccomp.k1c: idea.ccomp.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f $(PRODUCTS) idea.gcc.k1c.o idea.ccomp.k1c.o - -.PHONY: clean diff --git a/test/monniaux/idea/make.proto b/test/monniaux/idea/make.proto new file mode 100644 index 00000000..0e147514 --- /dev/null +++ b/test/monniaux/idea/make.proto @@ -0,0 +1,2 @@ +target: idea +measures: [cycles] diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c new file mode 100644 index 00000000..6025cd13 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c @@ -0,0 +1,342 @@ +#include <assert.h> +#include "heater_control.h" + +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +/* Import dependencies */ + +/* Global constants (definitions) */ +double FAILURE = -999.0; +double TMIN = 6.0; +double TMAX = 9.0; +double DELTA = 0.5; + +/* Struct definitions */ +struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2; + } _reg; + struct _arrow_mem *ni_0; + }; +struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16; + } _reg; + struct _arrow_mem *ni_1; + }; +struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2; + } _reg; + struct _arrow_mem *ni_2; + }; + + +void not_a_sauna2_reset (struct not_a_sauna2_mem *self) { + + _arrow_reset(self->ni_0); + return; +} + +void not_a_sauna2_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna2_mem *self) { + _Bool __not_a_sauna2_1; + + + _arrow_step (1, 0, &__not_a_sauna2_1, self->ni_0); + if (__not_a_sauna2_1) { + *ok = 1; + } else { + *ok = (self->_reg.__not_a_sauna2_2 < (9.0 - 6.0)); + } + self->_reg.__not_a_sauna2_2 = T; + + return; +} + +void heater_control_reset (struct heater_control_mem *self) { + + _arrow_reset(self->ni_1); + return; +} + +void heater_control_step (double T, double T1, double T2, double T3, + _Bool (*Heat_on), + struct heater_control_mem *self) { + double Median_42_max2_150_m; + double Median_42_max2_152_m; + double Median_42_min2_141_m; + double Median_42_min2_143_m; + double Median_52_max2_150_m; + double Median_52_max2_152_m; + double Median_52_min2_141_m; + double Median_52_min2_143_m; + double Tguess; + _Bool V12; + _Bool V13; + _Bool V23; + _Bool __heater_control_12; + double abs_15_a; + double abs_15_v; + double abs_23_a; + double abs_23_v; + double abs_7_a; + double abs_7_v; + + + + + + + + + + + + + + + + + + + + + abs_7_v = (T1 - T2); + if ((abs_7_v >= 0.0)) { + abs_7_a = abs_7_v; + } else { + abs_7_a = (- abs_7_v); + } + abs_23_v = (T2 - T3); + if ((abs_23_v >= 0.0)) { + abs_23_a = abs_23_v; + } else { + abs_23_a = (- abs_23_v); + } + abs_15_v = (T1 - T3); + if ((abs_15_v >= 0.0)) { + abs_15_a = abs_15_v; + } else { + abs_15_a = (- abs_15_v); + } + V23 = (abs_23_a < 0.5); + V13 = (abs_15_a < 0.5); + V12 = (abs_7_a < 0.5); + if ((T2 < T3)) { + Median_52_min2_141_m = T2; + } else { + Median_52_min2_141_m = T3; + } + if ((T2 > T3)) { + Median_42_max2_150_m = T2; + } else { + Median_42_max2_150_m = T3; + } + if ((T2 < T3)) { + Median_42_min2_141_m = T2; + } else { + Median_42_min2_141_m = T3; + } + if ((T2 > T3)) { + Median_52_max2_150_m = T2; + } else { + Median_52_max2_150_m = T3; + } + if ((T1 < Median_52_min2_141_m)) { + Median_52_min2_143_m = T1; + } else { + Median_52_min2_143_m = Median_52_min2_141_m; + } + if ((T1 > Median_52_max2_150_m)) { + Median_52_max2_152_m = T1; + } else { + Median_52_max2_152_m = Median_52_max2_150_m; + } + if ((T1 < Median_42_min2_141_m)) { + Median_42_min2_143_m = T1; + } else { + Median_42_min2_143_m = Median_42_min2_141_m; + } + if ((T1 > Median_42_max2_150_m)) { + Median_42_max2_152_m = T1; + } else { + Median_42_max2_152_m = Median_42_max2_150_m; + } + if ((((!V12) && (!V13)) && (!V23))) { + Tguess = -999.0; + } else { + if (((((V12 && (!V13)) && (!V23)) || ((V13 && (!V12)) && (!V23))) || ((V23 && (!V12)) && (!V13)))) { + Tguess = ((((T1 + T2) + T3) - Median_42_min2_143_m) - Median_42_max2_152_m); + } else { + if (((V12 && V13) && V23)) { + Tguess = ((((T1 + T2) + T3) - Median_52_min2_143_m) - Median_52_max2_152_m); + } else { + if (V12) { + Tguess = ((T1 + T2) / 2.0); + } else { + if (V13) { + Tguess = ((T1 + T3) / 2.0); + } else { + Tguess = ((T2 + T3) / 2.0); + } + } + } + } + } + _arrow_step (1, 0, &__heater_control_12, self->ni_1); + if (__heater_control_12) { + *Heat_on = 1; + } else { + if ((Tguess == -999.0)) { + *Heat_on = 0; + } else { + if ((Tguess < 6.0)) { + *Heat_on = 1; + } else { + if ((Tguess > 9.0)) { + *Heat_on = 0; + } else { + *Heat_on = self->_reg.__heater_control_16; + } + } + } + } + self->_reg.__heater_control_16 = *Heat_on; + + + + + + + + + + + + + + + + + + + + return; +} + +void not_a_sauna_reset (struct not_a_sauna_mem *self) { + + _arrow_reset(self->ni_2); + return; +} + +void not_a_sauna_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna_mem *self) { + _Bool __not_a_sauna_1; + + + _arrow_step (1, 0, &__not_a_sauna_1, self->ni_2); + if (__not_a_sauna_1) { + *ok = 1; + } else { + *ok = (self->_reg.__not_a_sauna_2 < (9.0 + 1.0)); + } + self->_reg.__not_a_sauna_2 = T; + + return; +} + +void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ) { + + *r = ((((f1 && (!f2)) && (!f3)) || ((f2 && (!f1)) && (!f3))) || ((f3 && (!f1)) && (!f2))); + return; +} + +void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ) { + + *r = (((!f1) && (!f2)) && (!f3)); + return; +} + +void alloftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ) { + + *r = ((f1 && f2) && f3); + return; +} + +void abs_step (double v, + double (*a) + ) { + + if ((v >= 0.0)) { + *a = v; + } else { + *a = (- v); + } + return; +} + +void Median_step (double a, double b, double c, + double (*z) + ) { + double __Median_1; + double __Median_2; + double __Median_3; + double __Median_4; + + + + + + min2_step (b, c, &__Median_3); + min2_step (a, __Median_3, &__Median_4); + max2_step (b, c, &__Median_1); + max2_step (a, __Median_1, &__Median_2); + *z = ((((a + b) + c) - __Median_4) - __Median_2); + + + + + return; +} + +void Average_step (double a, double b, + double (*z) + ) { + + *z = ((a + b) / 2.0); + return; +} + +void min2_step (double one, double two, + double (*m) + ) { + + if ((one < two)) { + *m = one; + } else { + *m = two; + } + return; +} + +void max2_step (double one, double two, + double (*m) + ) { + + if ((one > two)) { + *m = one; + } else { + *m = two; + } + return; +} + diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h new file mode 100644 index 00000000..d25a7d52 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h @@ -0,0 +1,96 @@ +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +#ifndef _HEATER_CONTROL +#define _HEATER_CONTROL + +/* Imports standard library */ +#include <stdint.h> +#include "/opt/lustrec/1.6/include/lustrec/arrow.h" + + +/* Import dependencies */ + +/* Types definitions */ + +/* Global constant (declarations, definitions are in C file) */ +extern double FAILURE; +extern double TMIN; +extern double TMAX; +extern double DELTA; + +/* Structs declarations */ +struct not_a_sauna2_mem; +struct heater_control_mem; +struct not_a_sauna_mem; + +/* Nodes declarations */ +extern void not_a_sauna2_reset (struct not_a_sauna2_mem *self); + +extern void not_a_sauna2_init (struct not_a_sauna2_mem *self); + +extern void not_a_sauna2_clear (struct not_a_sauna2_mem *self); + +extern void not_a_sauna2_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna2_mem *self); + +extern void heater_control_reset (struct heater_control_mem *self); + +extern void heater_control_init (struct heater_control_mem *self); + +extern void heater_control_clear (struct heater_control_mem *self); + +extern void heater_control_step (double T, double T1, double T2, double T3, + _Bool (*Heat_on), + struct heater_control_mem *self); + +extern void not_a_sauna_reset (struct not_a_sauna_mem *self); + +extern void not_a_sauna_init (struct not_a_sauna_mem *self); + +extern void not_a_sauna_clear (struct not_a_sauna_mem *self); + +extern void not_a_sauna_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna_mem *self); + +extern void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ); + +extern void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ); + +extern void alloftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ); + +extern void abs_step (double v, + double (*a) + ); + +extern void Median_step (double a, double b, double c, + double (*z) + ); + +extern void Average_step (double a, double b, + double (*z) + ); + +extern void min2_step (double one, double two, + double (*m) + ); + +extern void max2_step (double one, double two, + double (*m) + ); + + +#endif + diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus new file mode 100644 index 00000000..9a668a47 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus @@ -0,0 +1,126 @@ +-- +-- A fault-tolerant heater controller with 3 sensors. +-- +-- To guess the temperature (T), +-- +-- (1) It compares the value of the 3 sensors 2 by 2 to determine +-- which ones seem are broken -- we consider then broken if they +-- differ too much. +-- +-- (2) then, it performs a vote: +-- o If the tree sensors are broken, it does not heat; +-- o If the temperature is bigger than TMAX, it does not heat; +-- o If the temperature is smaller than TMIN, it heats; +-- o Otherwise, it keeps its previous state. + + +const FAILURE = -999.0; -- a fake temperature given when all sensors are broken +const TMIN = 6.0; +const TMAX = 9.0; + + +const DELTA = 0.5; +-- const DELTA : real; + +----------------------------------------------------------------------- +----------------------------------------------------------------------- +node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool); +-- T is supposed to be the real temperature and is not +-- used in the controller; we add it here in oder to test the +-- controller to be able to write a sensible oracle. + + +var + V12, V13, V23 : bool; + Tguess : real; + +let + V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid? + V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid? + V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid? + + Tguess = + if noneoftree(V12, V13, V23) then FAILURE else + if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else + if alloftree(V12, V13, V23) then Median(T1, T2, T3) else + -- 2 among V1, V2, V3 are false + if V12 then Average(T1, T2) else + if V13 then Average(T1, T3) else + -- V23 is necessarily true, hence T1 is wrong + Average(T2, T3) ; + + Heat_on = true -> + if Tguess = FAILURE then false else + if Tguess < TMIN then true else + if Tguess > TMAX then false else + pre Heat_on; +tel + + +----------------------------------------------------------------------- +----------------------------------------------------------------------- +node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); + +let + ok = true -> pre T < TMAX + 1.0 ; +tel + +node not_a_sauna2(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); + +let + ok = true -> pre T < TMAX - 6.0 ; +tel + + + +----------------------------------------------------------------------- +----------------------------------------------------------------------- + +-- returns the absolute value of 2 reals +function abs (v : real) returns (a : real) ; +let + a = if v >= 0.0 then v else -v ; +tel + +-- returns the average values of 2 reals +function Average(a, b: real) returns (z : real); +let + z = (a+b)/2.0 ; +tel + +-- returns the median values of 3 reals +function Median(a, b, c : real) returns (z : real); +let + z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ; +tel + + +-- returns the maximum values of 2 reals +function max2 (one, two : real) returns (m : real) ; +let + m = if one > two then one else two ; +tel + +-- returns the minimum values of 2 reals +function min2 (one, two : real) returns (m : real) ; +let + m = if one < two then one else two ; +tel + + +function noneoftree (f1, f2, f3 : bool) returns (r : bool) +let + r = not f1 and not f2 and not f3 ; +tel + +function alloftree (f1, f2, f3 : bool) returns (r : bool) +let + r = f1 and f2 and f3 ; +tel + +function oneoftree (f1, f2, f3 : bool) returns (r : bool) +let + r = f1 and not f2 and not f3 or + f2 and not f1 and not f3 or + f3 and not f1 and not f2 ; +tel diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h new file mode 100644 index 00000000..270ed4a3 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h @@ -0,0 +1,73 @@ +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +#ifndef _HEATER_CONTROL_alloc +#define _HEATER_CONTROL_alloc + +/* Import header from heater_control */ +#include "heater_control.h" + +/* Import dependencies */ + +/* Struct definitions */ +struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2; + } _reg; + struct _arrow_mem *ni_0; + }; +struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16; + } _reg; + struct _arrow_mem *ni_1; + }; +struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2; + } _reg; + struct _arrow_mem *ni_2; + }; + +/* Node allocation function/macro prototypes */ +#define not_a_sauna2_DECLARE(attr, inst)\ + attr struct not_a_sauna2_mem inst;\ + _arrow_DECLARE(attr, inst ## _ni_0); + +#define not_a_sauna2_LINK(inst) do {\ + _arrow_LINK(inst ## _ni_0);\ + inst.ni_0 = &inst ## _ni_0;\ +} while (0) + +#define not_a_sauna2_ALLOC(attr, inst)\ + not_a_sauna2_DECLARE(attr, inst);\ + not_a_sauna2_LINK(inst); + + +#define heater_control_DECLARE(attr, inst)\ + attr struct heater_control_mem inst;\ + _arrow_DECLARE(attr, inst ## _ni_1); + +#define heater_control_LINK(inst) do {\ + _arrow_LINK(inst ## _ni_1);\ + inst.ni_1 = &inst ## _ni_1;\ +} while (0) + +#define heater_control_ALLOC(attr, inst)\ + heater_control_DECLARE(attr, inst);\ + heater_control_LINK(inst); + + +#define not_a_sauna_DECLARE(attr, inst)\ + attr struct not_a_sauna_mem inst;\ + _arrow_DECLARE(attr, inst ## _ni_2); + +#define not_a_sauna_LINK(inst) do {\ + _arrow_LINK(inst ## _ni_2);\ + inst.ni_2 = &inst ## _ni_2;\ +} while (0) + +#define not_a_sauna_ALLOC(attr, inst)\ + not_a_sauna_DECLARE(attr, inst);\ + not_a_sauna_LINK(inst); + + + +#endif + diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c new file mode 100644 index 00000000..d0298840 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c @@ -0,0 +1,48 @@ +#include <stdio.h> +#include <unistd.h> +#include <stdlib.h> +#include <assert.h> +#include "heater_control_alloc.h" +#include "../clock.h" +#include "../dm_random.c" + +static double _get_double(void) { + return (dm_random_uint32()%70000U) * 1E-3 -20.0; +} + +static void _put_bool(const char *name, _Bool b) { + printf("%s: %d\n", name, b); +} + +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +int main (int argc, char *argv[]) { + + /* Main memory allocation */ + heater_control_ALLOC(static,main_mem); + + clock_prepare(); + clock_start(); + + /* Initialize the main memory */ + heater_control_reset(&main_mem); + + /* Infinite loop */ + for(int loop_count=0; loop_count<1000; loop_count++){ + double T = _get_double(); + double T1 = _get_double(); + double T2 = _get_double(); + double T3 = _get_double(); + _Bool Heat_on; + heater_control_step (T, T1, T2, T3, &Heat_on, &main_mem); + // _put_bool("Heat_on", Heat_on); + } + + clock_stop(); + print_total_clock(); + + return 1; +} diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control.c b/test/monniaux/lustrev4_lv4_heater_control/heater_control.c new file mode 100644 index 00000000..4a2b8174 --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control.c @@ -0,0 +1,275 @@ +/******** +* ec2c version 0.67 +* c file generated for node : heater_control +* context method = HEAP +* ext call method = PROCEDURES +********/ +#include <stdlib.h> +#include <string.h> +#define _heater_control_EC2C_SRC_FILE +#include "heater_control.h" +/*-------- +Internal structure for the call +--------*/ +typedef struct { + void* client_data; + //INPUTS + _real _T; + _real _T1; + _real _T2; + _real _T3; + //OUTPUTS + _boolean _Heat_on; + //REGISTERS + _boolean M73; + _boolean M73_nil; + _boolean M5; +} heater_control_ctx; +/*-------- +Output procedures must be defined, +Input procedures must be used: +--------*/ +void heater_control_I_T(heater_control_ctx* ctx, _real V){ + ctx->_T = V; +} +void heater_control_I_T1(heater_control_ctx* ctx, _real V){ + ctx->_T1 = V; +} +void heater_control_I_T2(heater_control_ctx* ctx, _real V){ + ctx->_T2 = V; +} +void heater_control_I_T3(heater_control_ctx* ctx, _real V){ + ctx->_T3 = V; +} +extern void heater_control_O_Heat_on(void* cdata, _boolean); +#ifdef CKCHECK +extern void heater_control_BOT_Heat_on(void* cdata); +#endif +/*-------- +Internal reset input procedure +--------*/ +static void heater_control_reset_input(heater_control_ctx* ctx){ + //NOTHING FOR THIS VERSION... +} +/*-------- +Reset procedure +--------*/ +void heater_control_reset(heater_control_ctx* ctx){ + ctx->M73_nil = _true; + ctx->M5 = _true; + heater_control_reset_input(ctx); +} +/*-------- +Copy the value of an internal structure +--------*/ +void heater_control_copy_ctx(heater_control_ctx* dest, heater_control_ctx +* src){ + memcpy((void*)dest, (void*)src, sizeof(heater_control_ctx)); +} +/*-------- +Dynamic allocation of an internal structure +--------*/ +heater_control_ctx* heater_control_new_ctx(void* cdata){ + heater_control_ctx* ctx = (heater_control_ctx*)calloc(1, sizeof( +heater_control_ctx)); + ctx->client_data = cdata; + heater_control_reset(ctx); + return ctx; +} +/*-------- +Step procedure +--------*/ +void heater_control_step(heater_control_ctx* ctx){ +//LOCAL VARIABLES + _real L16; + _boolean L15; + _real L18; + _real L14; + _boolean L13; + _boolean L12; + _real L24; + _boolean L23; + _real L25; + _real L22; + _boolean L21; + _boolean L20; + _boolean L11; + _real L30; + _boolean L29; + _real L31; + _real L28; + _boolean L27; + _boolean L26; + _boolean L10; + _real L32; + _boolean L38; + _boolean L37; + _boolean L40; + _boolean L39; + _boolean L36; + _boolean L42; + _boolean L41; + _boolean L35; + _real L46; + _real L45; + _boolean L50; + _real L49; + _boolean L48; + _real L47; + _real L44; + _boolean L54; + _real L53; + _boolean L52; + _real L51; + _real L43; + _boolean L57; + _boolean L56; + _real L59; + _real L63; + _real L62; + _real L65; + _real L64; + _real L61; + _real L58; + _real L55; + _real L34; + _real L9; + _boolean L8; + _boolean L68; + _boolean L71; + _boolean L70; + _boolean L67; + _boolean L7; + _boolean L4; + _boolean T73; +//CODE + L16 = (ctx->_T1 - ctx->_T2); + L15 = (L16 >= 0.000000); + L18 = (- L16); + if (L15) { + L14 = L16; + } else { + L14 = L18; + } + L13 = (L14 < 0.500000); + L12 = (! L13); + L24 = (ctx->_T1 - ctx->_T3); + L23 = (L24 >= 0.000000); + L25 = (- L24); + if (L23) { + L22 = L24; + } else { + L22 = L25; + } + L21 = (L22 < 0.500000); + L20 = (! L21); + L11 = (L12 && L20); + L30 = (ctx->_T2 - ctx->_T3); + L29 = (L30 >= 0.000000); + L31 = (- L30); + if (L29) { + L28 = L30; + } else { + L28 = L31; + } + L27 = (L28 < 0.500000); + L26 = (! L27); + L10 = (L11 && L26); + L32 = (- 999.000000); + L38 = (L13 && L20); + L37 = (L38 && L26); + L40 = (L21 && L12); + L39 = (L40 && L26); + L36 = (L37 || L39); + L42 = (L27 && L12); + L41 = (L42 && L20); + L35 = (L36 || L41); + L46 = (ctx->_T1 + ctx->_T2); + L45 = (L46 + ctx->_T3); + L50 = (ctx->_T2 < ctx->_T3); + if (L50) { + L49 = ctx->_T2; + } else { + L49 = ctx->_T3; + } + L48 = (ctx->_T1 < L49); + if (L48) { + L47 = ctx->_T1; + } else { + L47 = L49; + } + L44 = (L45 - L47); + L54 = (ctx->_T2 > ctx->_T3); + if (L54) { + L53 = ctx->_T2; + } else { + L53 = ctx->_T3; + } + L52 = (ctx->_T1 > L53); + if (L52) { + L51 = ctx->_T1; + } else { + L51 = L53; + } + L43 = (L44 - L51); + L57 = (L13 && L21); + L56 = (L57 && L27); + L59 = (L46 / 2.000000); + L63 = (ctx->_T1 + ctx->_T3); + L62 = (L63 / 2.000000); + L65 = (ctx->_T2 + ctx->_T3); + L64 = (L65 / 2.000000); + if (L21) { + L61 = L62; + } else { + L61 = L64; + } + if (L13) { + L58 = L59; + } else { + L58 = L61; + } + if (L56) { + L55 = L43; + } else { + L55 = L58; + } + if (L35) { + L34 = L43; + } else { + L34 = L55; + } + if (L10) { + L9 = L32; + } else { + L9 = L34; + } + L8 = (L9 == L32); + L68 = (L9 < 6.000000); + L71 = (L9 > 9.000000); + if (L71) { + L70 = _false; + } else { + L70 = ctx->M73; + } + if (L68) { + L67 = _true; + } else { + L67 = L70; + } + if (L8) { + L7 = _false; + } else { + L7 = L67; + } + if (ctx->M5) { + L4 = _true; + } else { + L4 = L7; + } + heater_control_O_Heat_on(ctx->client_data, L4); + T73 = L4; + ctx->M73 = T73; + ctx->M73_nil = _false; + ctx->M5 = ctx->M5 && !(_true); +} diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control.h b/test/monniaux/lustrev4_lv4_heater_control/heater_control.h new file mode 100644 index 00000000..64be774b --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control.h @@ -0,0 +1,47 @@ +/******** +* ec2c version 0.67 +* context method = HEAP +* ext call method = PROCEDURES +* c header file generated for node : heater_control +* to be used with : heater_control.c +********/ +#ifndef _heater_control_EC2C_H_FILE +#define _heater_control_EC2C_H_FILE +/*-------- Predefined types ---------*/ +#ifndef _EC2C_PREDEF_TYPES +#define _EC2C_PREDEF_TYPES +typedef int _boolean; +typedef int _integer; +typedef char* _string; +typedef double _real; +typedef double _double; +typedef float _float; +#define _false 0 +#define _true 1 +#endif +/*--------- Pragmas ----------------*/ +//MODULE: heater_control 4 1 +//IN: _real T +//IN: _real T1 +//IN: _real T2 +//IN: _real T3 +//OUT: _boolean Heat_on +#ifndef _heater_control_EC2C_SRC_FILE +/*--------Context type -------------*/ +struct heater_control_ctx; +/*-------- Input procedures -------------*/ +extern void heater_control_I_T(struct heater_control_ctx* ctx, _real); +extern void heater_control_I_T1(struct heater_control_ctx* ctx, _real); +extern void heater_control_I_T2(struct heater_control_ctx* ctx, _real); +extern void heater_control_I_T3(struct heater_control_ctx* ctx, _real); +/*-------- Reset procedure -----------*/ +extern void heater_control_reset(struct heater_control_ctx* ctx); +/*--------Context copy -------------*/ +extern void heater_control_copy_ctx(struct heater_control_ctx* dest, struct +heater_control_ctx* src); +/*--------Context allocation --------*/ +extern struct heater_control_ctx* heater_control_new_ctx(void* client_data); +/*-------- Step procedure -----------*/ +extern void heater_control_step(struct heater_control_ctx* ctx); +#endif +#endif diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control.lus b/test/monniaux/lustrev4_lv4_heater_control/heater_control.lus new file mode 100644 index 00000000..5d0db95f --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control.lus @@ -0,0 +1,126 @@ +-- +-- A fault-tolerant heater controller with 3 sensors. +-- +-- To guess the temperature (T), +-- +-- (1) It compares the value of the 3 sensors 2 by 2 to determine +-- which ones seem are broken -- we consider then broken if they +-- differ too much. +-- +-- (2) then, it performs a vote: +-- o If the tree sensors are broken, it does not heat; +-- o If the temperature is bigger than TMAX, it does not heat; +-- o If the temperature is smaller than TMIN, it heats; +-- o Otherwise, it keeps its previous state. + + +const FAILURE = -999.0; -- a fake temperature given when all sensors are broken +const TMIN = 6.0; +const TMAX = 9.0; + + +const DELTA = 0.5; +-- const DELTA : real; + +----------------------------------------------------------------------- +----------------------------------------------------------------------- +node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool); +-- T is supposed to be the real temperature and is not +-- used in the controller; we add it here in oder to test the +-- controller to be able to write a sensible oracle. + + +var + V12, V13, V23 : bool; + Tguess : real; + +let + V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid? + V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid? + V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid? + + Tguess = + if noneoftree(V12, V13, V23) then FAILURE else + if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else + if alloftree(V12, V13, V23) then Median(T1, T2, T3) else + -- 2 among V1, V2, V3 are false + if V12 then Average(T1, T2) else + if V13 then Average(T1, T3) else + -- V23 is necessarily true, hence T1 is wrong + Average(T2, T3) ; + + Heat_on = true -> + if Tguess = FAILURE then false else + if Tguess < TMIN then true else + if Tguess > TMAX then false else + pre Heat_on; +tel + + +----------------------------------------------------------------------- +----------------------------------------------------------------------- +node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); + +let + ok = true -> pre T < TMAX + 1.0 ; +tel + +node not_a_sauna2(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); + +let + ok = true -> pre T < TMAX - 6.0 ; +tel + + + +----------------------------------------------------------------------- +----------------------------------------------------------------------- + +-- returns the absolute value of 2 reals +node abs (v : real) returns (a : real) ; +let + a = if v >= 0.0 then v else -v ; +tel + +-- returns the average values of 2 reals +node Average(a, b: real) returns (z : real); +let + z = (a+b)/2.0 ; +tel + +-- returns the median values of 3 reals +node Median(a, b, c : real) returns (z : real); +let + z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ; +tel + + +-- returns the maximum values of 2 reals +node max2 (one, two : real) returns (m : real) ; +let + m = if one > two then one else two ; +tel + +-- returns the minimum values of 2 reals +node min2 (one, two : real) returns (m : real) ; +let + m = if one < two then one else two ; +tel + + +node noneoftree (f1, f2, f3 : bool) returns (r : bool) +let + r = not f1 and not f2 and not f3 ; +tel + +node alloftree (f1, f2, f3 : bool) returns (r : bool) +let + r = f1 and f2 and f3 ; +tel + +node oneoftree (f1, f2, f3 : bool) returns (r : bool) +let + r = f1 and not f2 and not f3 or + f2 and not f1 and not f3 or + f3 and not f1 and not f2 ; +tel diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c b/test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c new file mode 100644 index 00000000..06bad418 --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c @@ -0,0 +1,64 @@ +/******** +* ec2c version 0.67 +* c main file generated for node : heater_control +* to be used with : heater_control.c +* and : heater_control.h +* context method = HEAP +* ext call method = PROCEDURES +********/ +#include <stdlib.h> +#include <stdio.h> +#include <unistd.h> +#include "../clock.h" +#include "../dm_random.c" +#include "heater_control.h" + +/* Print a promt ? ************************/ +static int ISATTY; +/* MACROS DEFINITIONS ****************/ +#ifndef TT +#define TT "true" +#endif +#ifndef FF +#define FF "false" +#endif +#ifndef BB +#define BB "bottom" +#endif +#ifdef CKCHECK +/* set this macro for testing output clocks */ +#endif + +/* Standard Input procedures **************/ +_real _get_real(char* n){ + return (dm_random_uint32()%70000U) * 1E-3 -20.0; +} +/* Standard Output procedures **************/ +void _put_bool(char* n, _boolean b){ + printf("%s: %d\n", n, b); +} +/* Output procedures **********************/ +void heater_control_O_Heat_on(void* cdata, _boolean _V) { + // _put_bool("Heat_on", _V); +} +/* Main procedure *************************/ +int main(){ + + /* Context allocation */ + struct heater_control_ctx* ctx = heater_control_new_ctx(NULL); + /* Main loop */ + clock_prepare(); + clock_start(); + heater_control_reset(ctx); + for(int count=0; count<1000; count++){ + heater_control_I_T(ctx, _get_real("T")); + heater_control_I_T1(ctx, _get_real("T1")); + heater_control_I_T2(ctx, _get_real("T2")); + heater_control_I_T3(ctx, _get_real("T3")); + heater_control_step(ctx); + + } + clock_stop(); + print_total_clock(); + return 0; +} diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus new file mode 100644 index 00000000..9a668a47 --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus @@ -0,0 +1,126 @@ +-- +-- A fault-tolerant heater controller with 3 sensors. +-- +-- To guess the temperature (T), +-- +-- (1) It compares the value of the 3 sensors 2 by 2 to determine +-- which ones seem are broken -- we consider then broken if they +-- differ too much. +-- +-- (2) then, it performs a vote: +-- o If the tree sensors are broken, it does not heat; +-- o If the temperature is bigger than TMAX, it does not heat; +-- o If the temperature is smaller than TMIN, it heats; +-- o Otherwise, it keeps its previous state. + + +const FAILURE = -999.0; -- a fake temperature given when all sensors are broken +const TMIN = 6.0; +const TMAX = 9.0; + + +const DELTA = 0.5; +-- const DELTA : real; + +----------------------------------------------------------------------- +----------------------------------------------------------------------- +node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool); +-- T is supposed to be the real temperature and is not +-- used in the controller; we add it here in oder to test the +-- controller to be able to write a sensible oracle. + + +var + V12, V13, V23 : bool; + Tguess : real; + +let + V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid? + V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid? + V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid? + + Tguess = + if noneoftree(V12, V13, V23) then FAILURE else + if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else + if alloftree(V12, V13, V23) then Median(T1, T2, T3) else + -- 2 among V1, V2, V3 are false + if V12 then Average(T1, T2) else + if V13 then Average(T1, T3) else + -- V23 is necessarily true, hence T1 is wrong + Average(T2, T3) ; + + Heat_on = true -> + if Tguess = FAILURE then false else + if Tguess < TMIN then true else + if Tguess > TMAX then false else + pre Heat_on; +tel + + +----------------------------------------------------------------------- +----------------------------------------------------------------------- +node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); + +let + ok = true -> pre T < TMAX + 1.0 ; +tel + +node not_a_sauna2(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); + +let + ok = true -> pre T < TMAX - 6.0 ; +tel + + + +----------------------------------------------------------------------- +----------------------------------------------------------------------- + +-- returns the absolute value of 2 reals +function abs (v : real) returns (a : real) ; +let + a = if v >= 0.0 then v else -v ; +tel + +-- returns the average values of 2 reals +function Average(a, b: real) returns (z : real); +let + z = (a+b)/2.0 ; +tel + +-- returns the median values of 3 reals +function Median(a, b, c : real) returns (z : real); +let + z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ; +tel + + +-- returns the maximum values of 2 reals +function max2 (one, two : real) returns (m : real) ; +let + m = if one > two then one else two ; +tel + +-- returns the minimum values of 2 reals +function min2 (one, two : real) returns (m : real) ; +let + m = if one < two then one else two ; +tel + + +function noneoftree (f1, f2, f3 : bool) returns (r : bool) +let + r = not f1 and not f2 and not f3 ; +tel + +function alloftree (f1, f2, f3 : bool) returns (r : bool) +let + r = f1 and f2 and f3 ; +tel + +function oneoftree (f1, f2, f3 : bool) returns (r : bool) +let + r = f1 and not f2 and not f3 or + f2 and not f1 and not f3 or + f3 and not f1 and not f2 ; +tel diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c new file mode 100644 index 00000000..b3995c61 --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c @@ -0,0 +1,309 @@ +/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */ +/* lv6 -en -2cgc heater_control.lus -n heater_control */ +/* on vanoise the 15/05/2019 at 13:20:10 */ +#include "heater_control_heater_control.h" +//// Defining step functions +// Memory initialisation for Lustre_arrow_ctx +#define DM_INLINE inline + +DM_INLINE void Lustre_arrow_ctx_reset(Lustre_arrow_ctx_type* ctx){ + int _i; + ctx->_memory = _true; +} + +// Initialisation of the internal structure of Lustre_arrow_ctx +DM_INLINE void Lustre_arrow_ctx_init(Lustre_arrow_ctx_type* ctx){ + // ctx->client_data = cdata; + Lustre_arrow_ctx_reset(ctx); + } +// Step function(s) for Lustre_arrow_ctx +DM_INLINE void Lustre_arrow_step(_boolean i1,_boolean i2,_boolean *out,Lustre_arrow_ctx_type* ctx){ *out = ((ctx->_memory)? i1 : i2); + ctx->_memory = _false; + +} // End of Lustre_arrow_step + +// Memory initialisation for Lustre_pre_ctx +DM_INLINE void Lustre_pre_ctx_reset(Lustre_pre_ctx_type* ctx){ + int _i; + +} + +// Initialisation of the internal structure of Lustre_pre_ctx +DM_INLINE void Lustre_pre_ctx_init(Lustre_pre_ctx_type* ctx){ + // ctx->client_data = cdata; + Lustre_pre_ctx_reset(ctx); + } +// Step function(s) for Lustre_pre_ctx +DM_INLINE void Lustre_pre_get(_boolean *out,Lustre_pre_ctx_type* ctx){ + *out = ctx->_memory; + +} // End of Lustre_pre_get + +DM_INLINE void Lustre_pre_set(_boolean i1,Lustre_pre_ctx_type* ctx){ + ctx->_memory = i1; + +} // End of Lustre_pre_set + +// Step function(s) for Lustre_slash_ctx +#if 0 +DM_INLINE void Lustre_slash_step(_real i1,_real i2,_real *out){ + *out = (i1 / i2); + +} +#else +#define Lustre_slash_step(x, y, out) *out = x/y +#endif +// End of Lustre_slash_step + +// Memory initialisation for heater_control_heater_control_ctx +DM_INLINE void heater_control_heater_control_ctx_reset(heater_control_heater_control_ctx_type* ctx){ + int _i; + + Lustre_pre_ctx_reset(&ctx->Lustre_pre_ctx_tab[0]); + Lustre_arrow_ctx_reset(&ctx->Lustre_arrow_ctx_tab[0]); +} + +// Initialisation of the internal structure of heater_control_heater_control_ctx +void heater_control_heater_control_ctx_init(heater_control_heater_control_ctx_type* ctx){ + // ctx->client_data = cdata; + heater_control_heater_control_ctx_reset(ctx); + } +// Step function(s) for heater_control_heater_control_ctx +void heater_control_heater_control_step(_real T,_real T1,_real T2,_real T3,_boolean *Heat_on,heater_control_heater_control_ctx_type* ctx){ _boolean __split_9_3; + _real __split_10_3; + _boolean __split_9_2; + _real __split_10_2; + _boolean __split_9_1; + _real __split_10_1; + _real __split_1_3; + _real __split_1_2; + _real __split_1_1; + _real __split_2_2; + _real __split_3_2; + _real __split_4_2; + _real __split_5_2; + _real __split_6_2; + _real __split_7_2; + _real __split_8_2; + _boolean ___split_38_1_2; + _boolean ___split_38_2_2; + _boolean ___split_37_1_2; + _boolean ___split_37_2_2; + _boolean __split_11_1; + _real __split_2_1; + _real __split_3_1; + _real __split_4_1; + _real __split_5_1; + _real __split_6_1; + _real __split_7_1; + _real __split_8_1; + _boolean ___split_38_1_1; + _boolean ___split_38_2_1; + _boolean ___split_37_1_1; + _boolean ___split_37_2_1; + _boolean __split_43_1; + _boolean __split_44_1; + _boolean __split_45_1; + _boolean __split_46_1; + _boolean __split_47_1; + _boolean __split_48_1; + _boolean __split_49_1; + _boolean __split_50_1; + _boolean __split_51_1; + _boolean __split_52_1; + _boolean __split_53_1; + _boolean __split_54_1; + _boolean __split_55_1; + _boolean __split_39_1; + _boolean __split_40_1; + _boolean __split_41_1; + _boolean __split_42_1; + _boolean _split_36; + _boolean _split_35; + _boolean _split_34; + _boolean _split_33; + _boolean _split_32; + _boolean _split_31; + _boolean _split_30; + _real _split_29; + _real _split_28; + _real _split_27; + _real _split_26; + _real _split_25; + _real _split_24; + _real _split_23; + _real _split_22; + _boolean _split_21; + _real _split_20; + _boolean _split_19; + _boolean _split_18; + _real _split_17; + _real _split_16; + _real _split_15; + _real _split_14; + _real _split_13; + _real _split_12; + _boolean V12; + _boolean V13; + _boolean V23; + _real Tguess; + + _split_16 = T2 - T3; + __split_10_1 = - _split_16; + __split_9_1 = _split_16 >= 0.0; + if (__split_9_1 == _true) { + _split_17 = _split_16; + } else { + _split_17 = __split_10_1; + } + V23 = _split_17 < 0.5; + __split_42_1 = ! V23; + _split_12 = T1 - T2; + __split_10_3 = - _split_12; + __split_9_3 = _split_12 >= 0.0; + if (__split_9_3 == _true) { + _split_13 = _split_12; + } else { + _split_13 = __split_10_3; + } + V12 = _split_13 < 0.5; + __split_39_1 = ! V12; + _split_14 = T1 - T3; + __split_10_2 = - _split_14; + __split_9_2 = _split_14 >= 0.0; + if (__split_9_2 == _true) { + _split_15 = _split_14; + } else { + _split_15 = __split_10_2; + } + V13 = _split_15 < 0.5; + __split_40_1 = ! V13; + __split_41_1 = __split_39_1 & __split_40_1; + _split_18 = __split_41_1 & __split_42_1; + __split_43_1 = ! V13; + __split_44_1 = V12 & __split_43_1; + __split_45_1 = ! V23; + __split_46_1 = __split_44_1 & __split_45_1; + __split_47_1 = ! V12; + __split_48_1 = V13 & __split_47_1; + __split_49_1 = ! V23; + __split_50_1 = __split_48_1 & __split_49_1; + __split_51_1 = __split_46_1 | __split_50_1; + __split_54_1 = ! V13; + __split_52_1 = ! V12; + __split_53_1 = V23 & __split_52_1; + __split_55_1 = __split_53_1 & __split_54_1; + _split_19 = __split_51_1 | __split_55_1; + ___split_37_1_1 = T2 > T3; + if (___split_37_1_1 == _true) { + __split_7_1 = T2; + } else { + __split_7_1 = T3; + } + ___split_37_2_1 = T1 > __split_7_1; + if (___split_37_2_1 == _true) { + __split_8_1 = T1; + } else { + __split_8_1 = __split_7_1; + } + ___split_38_1_1 = T2 < T3; + if (___split_38_1_1 == _true) { + __split_4_1 = T2; + } else { + __split_4_1 = T3; + } + ___split_38_2_1 = T1 < __split_4_1; + if (___split_38_2_1 == _true) { + __split_5_1 = T1; + } else { + __split_5_1 = __split_4_1; + } + __split_2_1 = T1 + T2; + __split_3_1 = __split_2_1 + T3; + __split_6_1 = __split_3_1 - __split_5_1; + _split_20 = __split_6_1 - __split_8_1; + __split_1_2 = T1 + T3; + Lustre_slash_step(__split_1_2,2.0,&_split_24); + __split_1_3 = T2 + T3; + Lustre_slash_step(__split_1_3,2.0,&_split_25); + if (V13 == _true) { + _split_26 = _split_24; + } else { + _split_26 = _split_25; + } + __split_1_1 = T1 + T2; + Lustre_slash_step(__split_1_1,2.0,&_split_23); + if (V12 == _true) { + _split_27 = _split_23; + } else { + _split_27 = _split_26; + } + __split_11_1 = V12 & V13; + _split_21 = __split_11_1 & V23; + ___split_37_1_2 = T2 > T3; + if (___split_37_1_2 == _true) { + __split_7_2 = T2; + } else { + __split_7_2 = T3; + } + ___split_37_2_2 = T1 > __split_7_2; + if (___split_37_2_2 == _true) { + __split_8_2 = T1; + } else { + __split_8_2 = __split_7_2; + } + ___split_38_1_2 = T2 < T3; + if (___split_38_1_2 == _true) { + __split_4_2 = T2; + } else { + __split_4_2 = T3; + } + ___split_38_2_2 = T1 < __split_4_2; + if (___split_38_2_2 == _true) { + __split_5_2 = T1; + } else { + __split_5_2 = __split_4_2; + } + __split_2_2 = T1 + T2; + __split_3_2 = __split_2_2 + T3; + __split_6_2 = __split_3_2 - __split_5_2; + _split_22 = __split_6_2 - __split_8_2; + if (_split_21 == _true) { + _split_28 = _split_22; + } else { + _split_28 = _split_27; + } + if (_split_19 == _true) { + _split_29 = _split_20; + } else { + _split_29 = _split_28; + } + if (_split_18 == _true) { + Tguess = -999.0; + } else { + Tguess = _split_29; + } + _split_30 = Tguess == -999.0; + _split_31 = Tguess < 6.0; + Lustre_pre_get(&_split_33,&ctx->Lustre_pre_ctx_tab[0]); + _split_32 = Tguess > 9.0; + if (_split_32 == _true) { + _split_34 = _false; + } else { + _split_34 = _split_33; + } + if (_split_31 == _true) { + _split_35 = _true; + } else { + _split_35 = _split_34; + } + if (_split_30 == _true) { + _split_36 = _false; + } else { + _split_36 = _split_35; + } + Lustre_arrow_step(_true,_split_36,Heat_on,&ctx->Lustre_arrow_ctx_tab[0]); + Lustre_pre_set(*Heat_on,&ctx->Lustre_pre_ctx_tab[0]); + +} // End of heater_control_heater_control_step + diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h new file mode 100644 index 00000000..bfe8df20 --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h @@ -0,0 +1,30 @@ +/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */ +/* lv6 -en -2cgc heater_control.lus -n heater_control */ +/* on vanoise the 15/05/2019 at 13:20:10 */ + +#include <stdlib.h> +#include <string.h> + +#include "lustre_types.h" +#include "lustre_consts.h" + +#ifndef _heater_control_heater_control_H_FILE +#define _heater_control_heater_control_H_FILE +void Lustre_arrow_ctx_reset(Lustre_arrow_ctx_type* ctx); +void Lustre_arrow_ctx_init(Lustre_arrow_ctx_type* ctx); +void Lustre_arrow_step(_boolean ,_boolean ,_boolean *,Lustre_arrow_ctx_type*); + +void Lustre_pre_ctx_reset(Lustre_pre_ctx_type* ctx); +void Lustre_pre_ctx_init(Lustre_pre_ctx_type* ctx); +void Lustre_pre_get(_boolean *,Lustre_pre_ctx_type*); + +void Lustre_pre_set(_boolean ,Lustre_pre_ctx_type*); + +void Lustre_slash_step(_real ,_real ,_real *); + +void heater_control_heater_control_ctx_reset(heater_control_heater_control_ctx_type* ctx); +void heater_control_heater_control_ctx_init(heater_control_heater_control_ctx_type* ctx); +void heater_control_heater_control_step(_real ,_real ,_real ,_real ,_boolean *,heater_control_heater_control_ctx_type*); + +///////////////////////////////////////////////// +#endif diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c new file mode 100644 index 00000000..d1a01268 --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c @@ -0,0 +1,63 @@ +/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */ +/* lv6 -en -2cgc heater_control.lus -n heater_control */ +/* on vanoise the 15/05/2019 at 13:20:10 */ + +#include <stdlib.h> +#include <stdio.h> +#include <unistd.h> +#include "../dm_random.c" +#include "../clock.h" +#include "heater_control_heater_control.h" + +/* MACROS DEFINITIONS ****************/ +#ifndef TT +#define TT "1" +#endif +#ifndef FF +#define FF "0" +#endif +#ifndef BB +#define BB "bottom" +#endif +#ifdef CKCHECK +/* set this macro for testing output clocks */ +#endif + +/* Standard Input procedures **************/ +_real _get_real(char* n){ + return (dm_random_uint32()%70000U) * 1E-3 -20.0; +} +/* Standard Output procedures **************/ +void _put_bool(char* n, _boolean b){ + printf("%s: %d\n", n, b); +} +/* Main procedure *************************/ +int main(){ + _real T; + _real T1; + _real T2; + _real T3; + _boolean Heat_on; + heater_control_heater_control_ctx_type ctx_struct; + heater_control_heater_control_ctx_type* ctx = &ctx_struct; + + clock_prepare(); + clock_start(); + + heater_control_heater_control_ctx_init(ctx); + + /* Main loop */ + for(int step=0; step<1000; step++){ + T = _get_real("T"); + T1 = _get_real("T1"); + T2 = _get_real("T2"); + T3 = _get_real("T3"); + heater_control_heater_control_step(T,T1,T2,T3,&Heat_on,ctx); + // _put_bool("Heat_on", Heat_on); + } + + clock_stop(); + print_total_clock(); + + return 1; +} diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c new file mode 100644 index 00000000..47bfb5f5 --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c @@ -0,0 +1,4 @@ +/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */ +/* lv6 -en -2cgc heater_control.lus -n heater_control */ +/* on vanoise the 15/05/2019 at 13:20:10 */ +#include "lustre_consts.h"
\ No newline at end of file diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h new file mode 100644 index 00000000..c2f70459 --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h @@ -0,0 +1,9 @@ +/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */ +/* lv6 -en -2cgc heater_control.lus -n heater_control */ +/* on vanoise the 15/05/2019 at 13:20:10 */ + +// Constant definitions +#define heater_control_DELTA 0.5 +#define heater_control_FAILURE -999.0 +#define heater_control_TMAX 9.0 +#define heater_control_TMIN 6.0 diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h new file mode 100644 index 00000000..7fdfa03e --- /dev/null +++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h @@ -0,0 +1,41 @@ +/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */ +/* lv6 -en -2cgc heater_control.lus -n heater_control */ +/* on vanoise the 15/05/2019 at 13:20:10 */ + +#ifndef _SOC2C_PREDEF_TYPES +#define _SOC2C_PREDEF_TYPES +typedef int _boolean; +typedef int _integer; +typedef char* _string; +typedef double _real; +typedef double _double; +typedef float _float; +#define _false 0 +#define _true 1 +#endif +// end of _SOC2C_PREDEF_TYPES +// User typedef +#ifndef _heater_control_heater_control_TYPES +#define _heater_control_heater_control_TYPES +#endif // enf of _heater_control_heater_control_TYPES +// Memoryless soc ctx typedef +// Memoryfull soc ctx typedef +/* Lustre_arrow_ctx */ +typedef struct { + /*Memory cell*/ + _boolean _memory ; +} Lustre_arrow_ctx_type; + +/* Lustre_pre_ctx */ +typedef struct { + /*Memory cell*/ + _boolean _memory ; +} Lustre_pre_ctx_type; + +/* heater_control_heater_control_ctx */ +typedef struct { + /*INSTANCES*/ + Lustre_pre_ctx_type Lustre_pre_ctx_tab[1]; + Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1]; +} heater_control_heater_control_ctx_type; + diff --git a/test/monniaux/lustre-carlightV2/carlightV2_carlight.c b/test/monniaux/lustrev6-carlightV2/carlightV2_carlight.c index 206f854a..206f854a 100644 --- a/test/monniaux/lustre-carlightV2/carlightV2_carlight.c +++ b/test/monniaux/lustrev6-carlightV2/carlightV2_carlight.c diff --git a/test/monniaux/lustre-carlightV2/carlightV2_carlight.h b/test/monniaux/lustrev6-carlightV2/carlightV2_carlight.h index c56c8fa1..c56c8fa1 100644 --- a/test/monniaux/lustre-carlightV2/carlightV2_carlight.h +++ b/test/monniaux/lustrev6-carlightV2/carlightV2_carlight.h diff --git a/test/monniaux/lustre-carlightV2/carlightV2_carlight_loop.c b/test/monniaux/lustrev6-carlightV2/carlightV2_carlight_loop.c index 2276d24b..a9b4417a 100644 --- a/test/monniaux/lustre-carlightV2/carlightV2_carlight_loop.c +++ b/test/monniaux/lustrev6-carlightV2/carlightV2_carlight_loop.c @@ -7,6 +7,7 @@ #include <unistd.h> #include "carlightV2_carlight.h" #include "../clock.h" +#include "../dm_random.c" /* MACROS DEFINITIONS ****************/ #ifndef TT @@ -22,12 +23,6 @@ /* set this macro for testing output clocks */ #endif -static uint32_t dm_random_uint32(void) { - static uint32_t current=UINT32_C(0xDEADBEEF); - current = ((uint64_t) current << 6) % UINT32_C(4294967291); - return current; -} - /* Standard Input procedures **************/ _boolean _get_bool(char* n){ return dm_random_uint32() & 1; diff --git a/test/monniaux/lustre-carlightV2/lustre_consts.c b/test/monniaux/lustrev6-carlightV2/lustre_consts.c index e1a77c9e..e1a77c9e 100644 --- a/test/monniaux/lustre-carlightV2/lustre_consts.c +++ b/test/monniaux/lustrev6-carlightV2/lustre_consts.c diff --git a/test/monniaux/lustre-carlightV2/lustre_consts.h b/test/monniaux/lustrev6-carlightV2/lustre_consts.h index 9d651d25..9d651d25 100644 --- a/test/monniaux/lustre-carlightV2/lustre_consts.h +++ b/test/monniaux/lustrev6-carlightV2/lustre_consts.h diff --git a/test/monniaux/lustre-carlightV2/lustre_types.h b/test/monniaux/lustrev6-carlightV2/lustre_types.h index e1cfb463..e1cfb463 100644 --- a/test/monniaux/lustre-carlightV2/lustre_types.h +++ b/test/monniaux/lustrev6-carlightV2/lustre_types.h diff --git a/test/monniaux/lustre-convertible-2cgc/convertible_main.c b/test/monniaux/lustrev6-convertible-2cgc/convertible_main.c index 285f8941..285f8941 100644 --- a/test/monniaux/lustre-convertible-2cgc/convertible_main.c +++ b/test/monniaux/lustrev6-convertible-2cgc/convertible_main.c diff --git a/test/monniaux/lustre-convertible-2cgc/convertible_main.h b/test/monniaux/lustrev6-convertible-2cgc/convertible_main.h index 63b4ea90..63b4ea90 100644 --- a/test/monniaux/lustre-convertible-2cgc/convertible_main.h +++ b/test/monniaux/lustrev6-convertible-2cgc/convertible_main.h diff --git a/test/monniaux/lustre-convertible-2cgc/convertible_main_loop.c b/test/monniaux/lustrev6-convertible-2cgc/convertible_main_loop.c index 9aa52cad..9646b39f 100644 --- a/test/monniaux/lustre-convertible-2cgc/convertible_main_loop.c +++ b/test/monniaux/lustrev6-convertible-2cgc/convertible_main_loop.c @@ -8,6 +8,7 @@ #include <stdint.h> #include "convertible_main.h" #include "../clock.h" +#include "../dm_random.c" /* MACROS DEFINITIONS ****************/ #ifndef TT @@ -23,12 +24,6 @@ /* set this macro for testing output clocks */ #endif -static uint32_t dm_random_uint32(void) { - static uint32_t current=UINT32_C(0xDEADBEEF); - current = ((uint64_t) current << 6) % UINT32_C(4294967291); - return current; -} - /* Standard Input procedures **************/ _boolean _get_bool(char* n){ return dm_random_uint32() & 1; diff --git a/test/monniaux/lustre-convertible-2cgc/lustre_consts.c b/test/monniaux/lustrev6-convertible-2cgc/lustre_consts.c index 925cbf0b..925cbf0b 100644 --- a/test/monniaux/lustre-convertible-2cgc/lustre_consts.c +++ b/test/monniaux/lustrev6-convertible-2cgc/lustre_consts.c diff --git a/test/monniaux/lustre-convertible-2cgc/lustre_consts.h b/test/monniaux/lustrev6-convertible-2cgc/lustre_consts.h index a9ba2005..a9ba2005 100644 --- a/test/monniaux/lustre-convertible-2cgc/lustre_consts.h +++ b/test/monniaux/lustrev6-convertible-2cgc/lustre_consts.h diff --git a/test/monniaux/lustre-convertible-2cgc/lustre_types.h b/test/monniaux/lustrev6-convertible-2cgc/lustre_types.h index 83a1c722..83a1c722 100644 --- a/test/monniaux/lustre-convertible-2cgc/lustre_types.h +++ b/test/monniaux/lustrev6-convertible-2cgc/lustre_types.h diff --git a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c b/test/monniaux/lustrev6-convertible-en-2cgc/convertible_main.c index 6a4db4c3..6a4db4c3 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c +++ b/test/monniaux/lustrev6-convertible-en-2cgc/convertible_main.c diff --git a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.h b/test/monniaux/lustrev6-convertible-en-2cgc/convertible_main.h index 4785db8a..4785db8a 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.h +++ b/test/monniaux/lustrev6-convertible-en-2cgc/convertible_main.h diff --git a/test/monniaux/lustre-convertible-en-2cgc/convertible_main_loop.c b/test/monniaux/lustrev6-convertible-en-2cgc/convertible_main_loop.c index 9aa52cad..9646b39f 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/convertible_main_loop.c +++ b/test/monniaux/lustrev6-convertible-en-2cgc/convertible_main_loop.c @@ -8,6 +8,7 @@ #include <stdint.h> #include "convertible_main.h" #include "../clock.h" +#include "../dm_random.c" /* MACROS DEFINITIONS ****************/ #ifndef TT @@ -23,12 +24,6 @@ /* set this macro for testing output clocks */ #endif -static uint32_t dm_random_uint32(void) { - static uint32_t current=UINT32_C(0xDEADBEEF); - current = ((uint64_t) current << 6) % UINT32_C(4294967291); - return current; -} - /* Standard Input procedures **************/ _boolean _get_bool(char* n){ return dm_random_uint32() & 1; diff --git a/test/monniaux/lustre-convertible-en-2cgc/lustre_consts.c b/test/monniaux/lustrev6-convertible-en-2cgc/lustre_consts.c index 18d80805..18d80805 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/lustre_consts.c +++ b/test/monniaux/lustrev6-convertible-en-2cgc/lustre_consts.c diff --git a/test/monniaux/lustre-convertible-en-2cgc/lustre_consts.h b/test/monniaux/lustrev6-convertible-en-2cgc/lustre_consts.h index eaa21a15..eaa21a15 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/lustre_consts.h +++ b/test/monniaux/lustrev6-convertible-en-2cgc/lustre_consts.h diff --git a/test/monniaux/lustre-convertible-en-2cgc/lustre_types.h b/test/monniaux/lustrev6-convertible-en-2cgc/lustre_types.h index 68127eb6..68127eb6 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/lustre_types.h +++ b/test/monniaux/lustrev6-convertible-en-2cgc/lustre_types.h diff --git a/test/monniaux/lustre-convertible/convertible_main.c b/test/monniaux/lustrev6-convertible/convertible_main.c index 19bc40b9..19bc40b9 100644 --- a/test/monniaux/lustre-convertible/convertible_main.c +++ b/test/monniaux/lustrev6-convertible/convertible_main.c diff --git a/test/monniaux/lustre-convertible/convertible_main.h b/test/monniaux/lustrev6-convertible/convertible_main.h index 6be30a78..6be30a78 100644 --- a/test/monniaux/lustre-convertible/convertible_main.h +++ b/test/monniaux/lustrev6-convertible/convertible_main.h diff --git a/test/monniaux/lustre-convertible/convertible_main_loop.c b/test/monniaux/lustrev6-convertible/convertible_main_loop.c index a53d3e5e..46e94cd1 100644 --- a/test/monniaux/lustre-convertible/convertible_main_loop.c +++ b/test/monniaux/lustrev6-convertible/convertible_main_loop.c @@ -8,6 +8,7 @@ #include <stdint.h> #include "convertible_main.h" #include "../clock.h" +#include "../dm_random.c" /* MACROS DEFINITIONS ****************/ #ifndef TT @@ -23,12 +24,6 @@ /* set this macro for testing output clocks */ #endif -static uint32_t dm_random_uint32(void) { - static uint32_t current=UINT32_C(0xDEADBEEF); - current = ((uint64_t) current << 6) % UINT32_C(4294967291); - return current; -} - /* Standard Input procedures **************/ _boolean _get_bool(char* n){ return dm_random_uint32() & 1; diff --git a/test/monniaux/lustre-convertible/lustre_consts.c b/test/monniaux/lustrev6-convertible/lustre_consts.c index 37bd763b..37bd763b 100644 --- a/test/monniaux/lustre-convertible/lustre_consts.c +++ b/test/monniaux/lustrev6-convertible/lustre_consts.c diff --git a/test/monniaux/lustre-convertible/lustre_consts.h b/test/monniaux/lustrev6-convertible/lustre_consts.h index 72ee469e..72ee469e 100644 --- a/test/monniaux/lustre-convertible/lustre_consts.h +++ b/test/monniaux/lustrev6-convertible/lustre_consts.h diff --git a/test/monniaux/lustre-convertible/lustre_types.h b/test/monniaux/lustrev6-convertible/lustre_types.h index e721c12a..e721c12a 100644 --- a/test/monniaux/lustre-convertible/lustre_types.h +++ b/test/monniaux/lustrev6-convertible/lustre_types.h diff --git a/test/monniaux/number_theoretic_transform/Makefile b/test/monniaux/number_theoretic_transform/Makefile deleted file mode 100644 index 701703e1..00000000 --- a/test/monniaux/number_theoretic_transform/Makefile +++ /dev/null @@ -1,25 +0,0 @@ -include ../rules.mk - -PRODUCTS=ntt.gcc.host.out ntt.ccomp.host.out ntt.gcc.o1.k1c.out ntt.gcc.k1c.out ntt.ccomp.k1c.out ntt.ccomp.k1c.s ntt.gcc.k1c.s ntt.gcc.k1c ntt.ccomp.k1c ntt.gcc.host ntt.ccomp.host - -all: $(PRODUCTS) - -ntt.gcc.host: ntt.c ../clock.o - $(CC) $(CFLAGS) ntt.c ../clock.o -o $@ - -ntt.ccomp.host: ntt.c ../clock.o - $(CCOMP) $(CCOMPFLAGS) ntt.c ../clock.o -o $@ - -ntt.gcc.k1c: ntt.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -ntt.gcc.o1.k1c: ntt.gcc.o1.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -ntt.ccomp.k1c: ntt.ccomp.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f *.k1c *.host *.out *.o *.s - -.PHONY: clean diff --git a/test/monniaux/number_theoretic_transform/make.proto b/test/monniaux/number_theoretic_transform/make.proto new file mode 100644 index 00000000..e1844226 --- /dev/null +++ b/test/monniaux/number_theoretic_transform/make.proto @@ -0,0 +1,2 @@ +target: ntt +measures: [cycles] diff --git a/test/monniaux/number_theoretic_transform/ntt.c b/test/monniaux/number_theoretic_transform/ntt.c index 9d8c8906..9c978218 100644 --- a/test/monniaux/number_theoretic_transform/ntt.c +++ b/test/monniaux/number_theoretic_transform/ntt.c @@ -14,8 +14,8 @@ FFT original code from Rosetta Code. #include <string.h> #include "../clock.h" -typedef uint64_t modint; -typedef int64_t smodint; +typedef uint32_t modint; +typedef int32_t smodint; static modint invm(modint a0, modint b0) { @@ -89,6 +89,12 @@ void fft(modint modulus, modint root_of_unit, modint buf[], unsigned n) free(out); } +static void negate(modint MODULUS, modint buf[restrict], unsigned n) { + for(unsigned i=0; i<n; i++) { + if (buf[i]) buf[i] = MODULUS-buf[i]; + } +} + static void mulvecm(modint modulus, modint buf[restrict], unsigned n, modint coef) { for(unsigned i=0; i<n; i++) { buf[i] = mulm(buf[i], coef, modulus); @@ -107,6 +113,7 @@ modint randm(modint modulus) { } int main() { +#if 0 modint root_of_unit = 1; for(modint i=1; i<MODULUS; i++) { if (powm_u(i, MUL_MODULUS/2, MODULUS) != 1) { @@ -114,8 +121,11 @@ int main() { break; } } +#else + modint root_of_unit = 3; +#endif assert(root_of_unit != 1); - printf("root of unit = %" PRIu64 "\n", root_of_unit); + //printf("root of unit = %" PRIu64 "\n", root_of_unit); modint *buf = malloc(LENGTH * sizeof(modint)), *save = malloc(LENGTH * sizeof(modint)); @@ -131,10 +141,13 @@ int main() { fft(MODULUS, invm(root_of_unit, MODULUS), buf, LENGTH); clock_stop(); print_total_clock(); - + +#if 0 /* can be replaced by x -> -x */ mulvecm(MODULUS, buf, LENGTH, invm(LENGTH, MODULUS)); - +#else + negate(MODULUS, buf, LENGTH); +#endif printf("compare = %d\n", memcmp(buf, save, LENGTH * sizeof(modint))); /* diff --git a/test/monniaux/quicksort/Makefile b/test/monniaux/quicksort/Makefile deleted file mode 100644 index f753d916..00000000 --- a/test/monniaux/quicksort/Makefile +++ /dev/null @@ -1,36 +0,0 @@ -include ../rules.mk - -PRODUCTS=quicksort.host quicksort.gcc.o1.k1c.out quicksort.gcc.k1c.out quicksort.ccomp.k1c.out quicksort.ccomp.k1c.s quicksort.gcc.k1c.s quicksort.gcc.k1c quicksort.ccomp.k1c - -all: $(PRODUCTS) - -%.gcc.k1c.s: %.c - $(K1C_CC) $(K1C_CFLAGS) -S $< -o $@ - -%.gcc.k1c.o: %.gcc.k1c.s - $(K1C_CC) $(K1C_CFLAGS) -c $< -o $@ - -%.ccomp.k1c.s: %.c - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -S $< -o $@ - -%.ccomp.k1c.o: %.ccomp.k1c.s - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -c $< -o $@ - -quicksort.host: quicksort.c quicksort_run.c quicksort.h - $(CC) $(CFLAGS) quicksort.c quicksort_run.c -o $@ - -quicksort.gcc.k1c.s quicksort.ccomp.k1c.s quicksort_run.gcc.k1c.s: quicksort.h - -quicksort.gcc.k1c: quicksort.gcc.k1c.o quicksort_run.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -quicksort.gcc.o1.k1c: quicksort.gcc.o1.k1c.o quicksort_run.gcc.o1.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -quicksort.ccomp.k1c: quicksort.ccomp.k1c.o quicksort_run.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f $(PRODUCTS) quicksort.gcc.k1c.o quicksort.ccomp.k1c.o quicksort_run.gcc.k1c.o quicksort_run.gcc.k1c.s - -.PHONY: clean diff --git a/test/monniaux/quicksort/make.proto b/test/monniaux/quicksort/make.proto new file mode 100644 index 00000000..fe2f906b --- /dev/null +++ b/test/monniaux/quicksort/make.proto @@ -0,0 +1,3 @@ +objdeps: [{name: quicksort_run, compiler: gcc}] +target: quicksort +measures: [quicksort_time] diff --git a/test/monniaux/quicksort/quicksort_run.c b/test/monniaux/quicksort/quicksort_run.c index f9e1b871..88747d17 100644 --- a/test/monniaux/quicksort/quicksort_run.c +++ b/test/monniaux/quicksort/quicksort_run.c @@ -13,7 +13,7 @@ int main (void) { quicksort(vec, len); quicksort_time = get_cycle() - quicksort_time; printf("sorted=%s\n" - "quicksort_time=%" PRIu64 "\n", + "quicksort_time:%" PRIu64 "\n", data_vec_is_sorted(vec, len)?"true":"false", quicksort_time); free(vec); diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index ffbdac96..d098d1b2 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -1,5 +1,5 @@ ALL_CCOMPFLAGS=-fno-unprototyped -CCOMP=ccomp +CCOMP=ccomp-x86 CCOMPFLAGS=-g -O3 -Wall $(ALL_CCOMPFLAGS) $(ALL_CFLAGS) CFLAGS=-g -std=c99 -O3 -Wall -Wextra -Werror=implicit $(ALL_CFLAGS) diff --git a/test/monniaux/run_benches.sh b/test/monniaux/run_benches.sh new file mode 100755 index 00000000..479d09eb --- /dev/null +++ b/test/monniaux/run_benches.sh @@ -0,0 +1,26 @@ + +source benches.sh + +rm -f commands.txt +for bench in $benches; do + echo "(cd $bench && make -j5 run)" >> commands.txt +done + +cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}' + +## +# Gather all the CSV files +## + +benches_csv="" +for bench in $benches; do + if [ -f $bench/measures.csv ]; then + benches_csv="$benches_csv $bench/measures.csv" + fi +done + +nawk 'FNR==1 && NR!=1{next;}{print}' $benches_csv > measures.csv +echo "measures.csv done" + +./gengraphs.py measures.csv +echo "Graphs done" diff --git a/test/monniaux/sha-2/Makefile b/test/monniaux/sha-2/Makefile deleted file mode 100644 index 8fba819b..00000000 --- a/test/monniaux/sha-2/Makefile +++ /dev/null @@ -1,24 +0,0 @@ -include ../rules.mk - -PRODUCTS=sha-256.host sha-256.gcc.o1.k1c.out sha-256.gcc.k1c.out sha-256.ccomp.k1c.out sha-256.ccomp.k1c.s sha-256.gcc.k1c.s sha-256.gcc.k1c sha-256.ccomp.k1c - -all: $(PRODUCTS) - -sha-256.host: sha-256.c sha-256_run.c sha-256.h - $(CC) $(CFLAGS) sha-256.c sha-256_run.c -o $@ - -sha-256.gcc.k1c.s sha-256.ccomp.k1c.s sha-256_run.gcc.k1c.s: sha-256.h - -sha-256.gcc.k1c: sha-256.gcc.k1c.o sha-256_run.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -sha-256.gcc.o1.k1c: sha-256.gcc.o1.k1c.o sha-256_run.gcc.o1.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -sha-256.ccomp.k1c: sha-256.ccomp.k1c.o sha-256_run.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - $(RM) -f $(PRODUCTS) sha-256.gcc.k1c.o sha-256.ccomp.k1c.o sha-256_run.gcc.k1c.o sha-256_run.gcc.k1c.s - -.PHONY: clean diff --git a/test/monniaux/sha-2/make.proto b/test/monniaux/sha-2/make.proto new file mode 100644 index 00000000..f776565e --- /dev/null +++ b/test/monniaux/sha-2/make.proto @@ -0,0 +1,3 @@ +objdeps: [{name: sha-256_run, compiler: gcc}] +target: sha-256 +measures: ["total cycles"] diff --git a/test/monniaux/sha-2/sha-256_run.c b/test/monniaux/sha-2/sha-256_run.c index c3865991..05a69d6b 100644 --- a/test/monniaux/sha-2/sha-256_run.c +++ b/test/monniaux/sha-2/sha-256_run.c @@ -280,6 +280,6 @@ int main(void) } } destruct_binary_messages(); - printf("total cycles = %" PRIu64 "\n", cycle_total); + printf("total cycles : %" PRIu64 "\n", cycle_total); return 0; } diff --git a/test/monniaux/tacle-bench-lift/Makefile b/test/monniaux/tacle-bench-lift/Makefile deleted file mode 100644 index ab930adb..00000000 --- a/test/monniaux/tacle-bench-lift/Makefile +++ /dev/null @@ -1,42 +0,0 @@ -ALL_CFLAGS = -include kill_pragma.h - -CFILES=lift.c liftlibcontrol.c liftlibio.c - -HFILES=liftlibcontrol.h liftlibio.h - -K1C_GCC_OFILES=$(CFILES:.c=.gcc.k1c.o) -K1C_GCC_OFILES_O1=$(CFILES:.c=.gcc.o1.k1c.o) -K1C_CCOMP_OFILES=$(CFILES:.c=.ccomp.k1c.o) -K1C_GCC_SFILES=$(CFILES:.c=.gcc.k1c.s) -K1C_CCOMP_SFILES=$(CFILES:.c=.ccomp.k1c.s) - -HOST_GCC_OFILES=$(CFILES:.c=.gcc.host.o) -HOST_CCOMP_OFILES=$(CFILES:.c=.ccomp.host.o) -HOST_GCC_SFILES=$(CFILES:.c=.gcc.host.s) -HOST_CCOMP_SFILES=$(CFILES:.c=.ccomp.host.s) - -all: lift.gcc.o1.k1c.out lift.gcc.k1c.out lift.ccomp.k1c.out $(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) - -include ../rules.mk - -$(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) $(HOST_GCC_SFILES) $(HOST_CCOMP_SFILES) : $(HFILES) - -lift.gcc.k1c: $(K1C_GCC_OFILES) - $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o - -lift.gcc.o1.k1c: $(K1C_GCC_OFILES_O1) - $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o - -lift.ccomp.k1c: $(K1C_CCOMP_OFILES) - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o - -lift.gcc.host: $(HOST_GCC_OFILES) - $(CC) $(CFLAGS) -o $@ $+ ../clock.gcc.host.o - -lift.ccomp.host: $(HOST_CCOMP_OFILES) - $(CCOMP) $(CCOMPFLAGS) -o $@ $+ ../clock.gcc.host.o - -.PHONY: clean - -clean: - rm -f *.s *.o *.k1c diff --git a/test/monniaux/tacle-bench-lift/make.proto b/test/monniaux/tacle-bench-lift/make.proto new file mode 100644 index 00000000..c4849bab --- /dev/null +++ b/test/monniaux/tacle-bench-lift/make.proto @@ -0,0 +1,4 @@ +intro: "ALL_CFLAGS = -include kill_pragma.h" +objdeps: [{name: liftlibcontrol, compiler: both}, {name: liftlibio, compiler: both}] +target: lift +measures: [cycles] diff --git a/test/monniaux/tacle-bench-powerwindow/Makefile b/test/monniaux/tacle-bench-powerwindow/Makefile deleted file mode 100644 index 560a0cf9..00000000 --- a/test/monniaux/tacle-bench-powerwindow/Makefile +++ /dev/null @@ -1,48 +0,0 @@ -ALL_CFLAGS = -include kill_pragma.h - -CFILES= powerwindow.c powerwindow_PW_Control_DRV.c \ - powerwindow_const_params.c powerwindow_PW_Control_PSG_BackL.c \ - powerwindow_controlexclusion.c powerwindow_PW_Control_PSG_BackR.c \ - powerwindow_debounce.c powerwindow_PW_Control_PSG_Front.c \ - powerwindow_inputs.c wcclib.c \ - powerwindow_powerwindow_control.c - -HFILES= kill_pragma.h wcclib.h \ - $(wildcard powerwindow_HeaderFiles/*.h) - -K1C_GCC_OFILES=$(CFILES:.c=.gcc.k1c.o) -K1C_GCC_OFILES_O1=$(CFILES:.c=.gcc.o1.k1c.o) -K1C_CCOMP_OFILES=$(CFILES:.c=.ccomp.k1c.o) -K1C_GCC_SFILES=$(CFILES:.c=.gcc.k1c.s) -K1C_CCOMP_SFILES=$(CFILES:.c=.ccomp.k1c.s) - -HOST_GCC_OFILES=$(CFILES:.c=.gcc.host.o) -HOST_CCOMP_OFILES=$(CFILES:.c=.ccomp.host.o) -HOST_GCC_SFILES=$(CFILES:.c=.gcc.host.s) -HOST_CCOMP_SFILES=$(CFILES:.c=.ccomp.host.s) - -all: powerwindow.gcc.o1.k1c.out powerwindow.gcc.k1c.out powerwindow.ccomp.k1c.out $(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) - -include ../rules.mk - -$(K1C_GCC_SFILES) $(K1C_CCOMP_SFILES) $(HOST_GCC_SFILES) $(HOST_CCOMP_SFILES) : $(HFILES) - -powerwindow.gcc.k1c: $(K1C_GCC_OFILES) - $(K1C_CC) $(K1C_CFLAGS) -o $@ $+ ../clock.gcc.k1c.o - -powerwindow.gcc.o1.k1c: $(K1C_GCC_OFILES_O1) - $(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+ ../clock.gcc.k1c.o - -powerwindow.ccomp.k1c: $(K1C_CCOMP_OFILES) - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+ ../clock.gcc.k1c.o - -powerwindow.gcc.host: $(HOST_GCC_OFILES) - $(CC) $(CFLAGS) -o $@ $+ ../clock.gcc.host.o - -powerwindow.ccomp.host: $(HOST_CCOMP_OFILES) - $(CCOMP) $(CCOMPFLAGS) -o $@ $+ ../clock.gcc.host.o - -.PHONY: clean - -clean: - rm -f *.s *.o *.k1c diff --git a/test/monniaux/tacle-bench-powerwindow/make.proto b/test/monniaux/tacle-bench-powerwindow/make.proto new file mode 100644 index 00000000..21e07941 --- /dev/null +++ b/test/monniaux/tacle-bench-powerwindow/make.proto @@ -0,0 +1,8 @@ +intro: "ALL_CFLAGS = -include kill_pragma.h" +objdeps: [{name: powerwindow_const_params, compiler: both}, {name: powerwindow_controlexclusion, compiler: both}, + {name: powerwindow_debounce, compiler: both}, {name: powerwindow_inputs, compiler: both}, + {name: powerwindow_powerwindow_control, compiler: both}, {name: powerwindow_PW_Control_DRV, compiler: both}, + {name: powerwindow_PW_Control_PSG_BackL, compiler: both}, {name: powerwindow_PW_Control_PSG_BackR, compiler: both}, + {name: powerwindow_PW_Control_PSG_Front, compiler: both}] +target: powerwindow +measures: [cycles] diff --git a/test/monniaux/ternary/Makefile b/test/monniaux/ternary/Makefile deleted file mode 100644 index 7b1fe155..00000000 --- a/test/monniaux/ternary/Makefile +++ /dev/null @@ -1,29 +0,0 @@ -include ../rules.mk - -PRODUCTS=ternary.gcc.host.out ternary.ccomp.host.out \ - ternary.gcc.o1.k1c.out ternary.gcc.k1c.out ternary.ccomp.k1c.out \ - ternary.gcc.k1c.s ternary.ccomp.k1c.s - -all: $(PRODUCTS) - -ternary.gcc.host.s ternary.ccomp.host.s ternary.gcc.k1c.s ternary.ccomp.k1c.s : ../clock.h - -ternary.ccomp.host: ternary.ccomp.host.o ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -o $@ - -ternary.gcc.host: ternary.gcc.host.o ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ -o $@ - -ternary.gcc.k1c: ternary.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -ternary.gcc.o1.k1c: ternary.gcc.o1.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -ternary.ccomp.k1c: ternary.ccomp.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - -rm -f *.o *.s *.k1c - -.PHONY: clean diff --git a/test/monniaux/ternary/make.proto b/test/monniaux/ternary/make.proto new file mode 100644 index 00000000..1568ed07 --- /dev/null +++ b/test/monniaux/ternary/make.proto @@ -0,0 +1,2 @@ +target: ternary +measures: [cycles] diff --git a/test/monniaux/ternary/ternary.c b/test/monniaux/ternary/ternary.c index ed7de156..e8813a5c 100644 --- a/test/monniaux/ternary/ternary.c +++ b/test/monniaux/ternary/ternary.c @@ -19,6 +19,6 @@ int main() { clock_start(); data result = silly_computation(); clock_stop(); - printf("result=%" PRIu32 "\ncycles=%" PRIu64 "\n", result, get_total_clock()); + printf("result=%" PRIu32 "\ncycles:%" PRIu64 "\n", result, get_total_clock()); return 0; } diff --git a/test/monniaux/too_slow/Makefile b/test/monniaux/too_slow/Makefile deleted file mode 100644 index fc612e2e..00000000 --- a/test/monniaux/too_slow/Makefile +++ /dev/null @@ -1,30 +0,0 @@ -include ../rules.mk - -PRODUCTS=memset_from_bitsliced-aes.gcc.host.out memset_from_bitsliced-aes.ccomp.host.out \ - memset_from_bitsliced-aes.gcc.o1.k1c.out memset_from_bitsliced-aes.gcc.k1c.out memset_from_bitsliced-aes.ccomp.k1c.out \ - memset_from_bitsliced-aes.gcc.k1c.s memset_from_bitsliced-aes.ccomp.k1c.s - -all: $(PRODUCTS) - -memset_from_bitsliced-aes.gcc.host.s memset_from_bitsliced-aes.ccomp.host.s memset_from_bitsliced-aes.gcc.k1c.s memset_from_bitsliced-aes.ccomp.k1c.s : ../clock.h - -memset_from_bitsliced-aes.ccomp.host: memset_from_bitsliced-aes.ccomp.host.o ../clock.gcc.host.o - $(CCOMP) $(CCOMPFLAGS) $+ -o $@ - -memset_from_bitsliced-aes.gcc.host: memset_from_bitsliced-aes.gcc.host.o ../clock.gcc.host.o - $(CC) $(CFLAGS) $+ -o $@ - -memset_from_bitsliced-aes.gcc.k1c: memset_from_bitsliced-aes.gcc.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS) $+ -o $@ - -memset_from_bitsliced-aes.gcc.o1.k1c: memset_from_bitsliced-aes.gcc.o1.k1c.o ../clock.gcc.k1c.o - $(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@ - -memset_from_bitsliced-aes.ccomp.k1c: memset_from_bitsliced-aes.ccomp.k1c.o ../clock.gcc.k1c.o - $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ - -clean: - -rm -f *.o *.s *.k1c - -.PHONY: clean - diff --git a/test/monniaux/too_slow/make.proto b/test/monniaux/too_slow/make.proto new file mode 100644 index 00000000..852971fc --- /dev/null +++ b/test/monniaux/too_slow/make.proto @@ -0,0 +1,3 @@ +target: memset_from_bitsliced-aes +measures: [cycles] +name: memset-aes |