Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

6 files changed, 518 insertions, 0 deletions

diff --git a/test/monniaux/lustrev4_lv4_heater_control/Makefile b/test/monniaux/lustrev4_lv4_heater_control/Makefile
new file mode 100644
index 00000000..cfd37921
--- /dev/null
+++ b/test/monniaux/lustrev4_lv4_heater_control/Makefile
@@ -0,0 +1,3 @@
+TARGET=lv4_heater_control
+
+include ../rules.mk
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_lv4_heater_control/make.proto b/test/monniaux/lustrev4_lv4_heater_control/make.proto
new file mode 100644
index 00000000..f19fec0f
--- /dev/null
+++ b/test/monniaux/lustrev4_lv4_heater_control/make.proto
@@ -0,0 +1,3 @@
+sources: "$(wildcard *.c)"
+target: lv4_heater_control
+measures: [cycles]