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

8 files changed, 584 insertions, 0 deletions

diff --git a/test/monniaux/tacle-bench-lift/Makefile b/test/monniaux/tacle-bench-lift/Makefile
new file mode 100644
index 00000000..2e1db080
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/Makefile
@@ -0,0 +1,4 @@
+ALL_CFLAGS:=-include kill_pragma.h
+TARGET=lift
+
+include ../rules.mk
diff --git a/test/monniaux/tacle-bench-lift/README.md b/test/monniaux/tacle-bench-lift/README.md
new file mode 100644
index 00000000..dc2b1967
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/README.md
@@ -0,0 +1 @@
+From tacle-bench/bench/app/lift
\ No newline at end of file
diff --git a/test/monniaux/tacle-bench-lift/kill_pragma.h b/test/monniaux/tacle-bench-lift/kill_pragma.h
new file mode 100644
index 00000000..a2fde5a9
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/kill_pragma.h
@@ -0,0 +1 @@
+#define _Pragma(x)
diff --git a/test/monniaux/tacle-bench-lift/lift.c b/test/monniaux/tacle-bench-lift/lift.c
new file mode 100644
index 00000000..5a810244
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/lift.c
@@ -0,0 +1,145 @@
+/* DM */
+#include "../clock.h"
+#include <stdio.h>
+
+/*
+
+  This program is part of the TACLeBench benchmark suite.
+  Version V 2.0
+
+  Name: lift
+
+  Author: Martin Schoeberl, Benedikt Huber
+
+  Function: Lift Controler
+
+  Source: C-Port from http://www.jopdesign.com/doc/jembench.pdf
+
+  Original name: run_lift.c
+
+  Changes: no major functional changes
+
+  License: GPL version 3 or later
+
+*/
+
+
+/*
+  Include section
+*/
+
+#include "liftlibio.h"
+#include "liftlibcontrol.h"
+
+
+/*
+  Forward declaration of functions
+*/
+
+void lift_controller();
+void lift_init();
+void lift_main();
+int lift_return();
+
+
+/*
+  Declaration of global variables
+*/
+
+int lift_checksum;/* Checksum */
+
+
+/*
+  Initialization- and return-value-related functions
+*/
+
+void lift_init()
+{
+  unsigned int i;
+  unsigned char *p;
+  volatile char bitmask = 0;
+
+  /*
+    Apply volatile XOR-bitmask to entire input array.
+  */
+  p = ( unsigned char * ) &lift_ctrl_io_in[ 0 ];
+  _Pragma( "loopbound min 40 max 40" )
+  for ( i = 0; i < sizeof( lift_ctrl_io_in ); ++i, ++p )
+    *p ^= bitmask;
+
+  p = ( unsigned char * ) &lift_ctrl_io_out[ 0 ];
+  _Pragma( "loopbound min 16 max 16" )
+  for ( i = 0; i < sizeof( lift_ctrl_io_out ); ++i, ++p )
+    *p ^= bitmask;
+
+  p = ( unsigned char * ) &lift_ctrl_io_analog[ 0 ];
+  _Pragma( "loopbound min 16 max 16" )
+  for ( i = 0; i < sizeof( lift_ctrl_io_analog ); ++i, ++p )
+    *p ^= bitmask;
+
+  p = ( unsigned char * ) &lift_ctrl_io_led[ 0 ];
+  _Pragma( "loopbound min 64 max 64" )
+  for ( i = 0; i < sizeof( lift_ctrl_io_led ); ++i, ++p )
+    *p ^= bitmask;
+
+  lift_checksum = 0;
+  lift_ctrl_init();
+}
+
+
+int lift_return()
+{
+  return ( lift_checksum - 4005888 != 0 );
+}
+
+
+/*
+  Algorithm core functions
+*/
+
+void lift_controller()
+{
+  lift_ctrl_get_vals();
+  lift_ctrl_loop();
+  lift_ctrl_set_vals();
+}
+
+
+/*
+  Main functions
+*/
+
+void  _Pragma( "entrypoint" ) lift_main()
+{
+  int i = 0;
+  _Pragma( "loopbound min 1001 max 1001" )
+  while ( 1 ) {
+    /* zero input stimulus */
+    lift_simio_in = 0;
+    lift_simio_adc1 = 0;
+    lift_simio_adc2 = 0;
+    lift_simio_adc3 = 0;
+    /* run lift_controller */
+    lift_controller();
+    if ( i++ >= 1000 )
+      break;
+  }
+}
+
+
+int main( void )
+{
+  clock_prepare();
+  clock_start();
+  
+  lift_init();
+  lift_main();
+
+  clock_stop();
+  
+  int ret = lift_return();
+
+  printf("check: %s\n", ret ? "FAIL" : "passed");
+  
+  print_total_clock();
+}
diff --git a/test/monniaux/tacle-bench-lift/liftlibcontrol.c b/test/monniaux/tacle-bench-lift/liftlibcontrol.c
new file mode 100644
index 00000000..5e491276
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/liftlibcontrol.c
@@ -0,0 +1,277 @@
+#include "liftlibio.h"
+#include "liftlibcontrol.h"
+
+/* Global variables */
+int lift_levelPos[16];
+int lift_one_level;
+
+/**
+   Is the counter valid for level positioning?
+*/
+int lift_cntValid;
+
+/**
+   Position absolute or relative<.
+*/
+int lift_cnt;
+
+/**
+   Last stoped level (1..13) if position is absolute else 0.
+*/
+int lift_level;
+
+/**
+   load position in level, 0 means we don't know
+*/
+int lift_loadLevel;
+
+/**
+   we're going TOP or BOTTOM, but stop at load position.
+*/
+int lift_loadPending;
+
+/**
+   we're waiting for the load sensor to go.
+*/
+int lift_loadSensor;
+
+/**
+   cmd keeps the value of the command until the command is finished.
+   It is only updated by the switches if it's current value is CMD_NONE.
+*/
+int lift_cmd;
+
+int lift_timMotor;
+
+int lift_timImp;
+
+/**
+   Remember last direction for impuls count after motor off;
+*/
+int lift_directionUp;
+
+/**
+   Last value of impuls sensor.
+*/
+int lift_lastImp;
+
+int lift_dbgCnt;
+
+/**
+   stop value for the counter.
+*/
+int lift_endCnt;
+
+
+void lift_ctrl_init()
+{
+  int i;
+  lift_checksum = 0;
+
+  lift_io_init();
+  lift_cntValid = 0;
+  lift_cnt = 0;
+  lift_cmd = lift_CMD_NONE;
+  lift_timMotor = 0;
+  lift_timImp = 0;
+  lift_directionUp = 1;
+  lift_lastImp = 0;
+  lift_loadLevel = 0;
+  lift_loadPending = 0;
+  lift_loadSensor = 0;
+  i = 0;
+  lift_levelPos[i++] = 0;
+  lift_levelPos[i++] = 58;
+  lift_levelPos[i++] = 115;
+  lift_levelPos[i++] = 173;
+  lift_levelPos[i++] = 230;
+  lift_levelPos[i++] = 288;
+  lift_levelPos[i++] = 346;
+  lift_levelPos[i++] = 403;
+  lift_levelPos[i++] = 461;
+  lift_levelPos[i++] = 518;
+  lift_levelPos[i++] = 576;
+  lift_levelPos[i++] = 634;
+  lift_levelPos[i++] = 691;
+  lift_levelPos[i++] = 749;
+  lift_levelPos[i++] = 806;
+  lift_levelPos[i++] = 864;
+  lift_one_level = lift_levelPos[1];
+}
+
+void lift_ctrl_loop()
+{
+  if ( lift_cmd == lift_CMD_NONE )
+    lift_check_cmd();
+  else {
+    lift_do_impulse( lift_ctrl_io_in[lift_SENS_IMPULS],
+                     lift_ctrl_io_out[lift_MOTOR_ON],
+                     lift_ctrl_io_in[lift_SENS_BOTTOM] );
+    lift_do_cmd();
+  }
+  lift_check_level();
+  lift_ctrl_io_led[13] = ( lift_dbgCnt & 0x80 ) != 0;
+  ++lift_dbgCnt;
+}
+
+
+void lift_check_level()
+{
+  int i;
+  int middle = lift_one_level >> 2;
+  if ( lift_cntValid ) {
+    _Pragma( "loopbound min 14 max 14" )
+    for ( lift_level = 1; lift_level < 14; ++lift_level ) {
+      if ( lift_cnt < lift_levelPos[lift_level] - middle )
+        break;
+    }
+  } else
+    lift_level = 0;
+  _Pragma( "loopbound min 14 max 14" )
+  for ( i = 0; i < 14; ++i )
+    lift_ctrl_io_led[i] = ( i == lift_level - 1 );
+}
+
+
+void lift_check_cmd()
+{
+  if ( lift_loadPending ) {
+    if ( lift_ctrl_io_in[lift_SENS_BOTTOM] )
+      lift_cmd = lift_CMD_TOP;
+  } else
+    if ( lift_ctrl_io_in[lift_GO_UP] ) {
+      if ( !lift_ctrl_io_in[lift_SENS_TOP] && lift_level != 14 )
+        lift_cmd = lift_CMD_UP;
+    } else
+      if ( lift_ctrl_io_in[lift_GO_DOWN] ) {
+        if ( !lift_ctrl_io_in[lift_SENS_BOTTOM] && lift_level != 1 )
+          lift_cmd = lift_CMD_DOWN;
+      } else
+        if ( lift_ctrl_io_in[lift_GO_LOAD] ) {
+          if ( lift_loadLevel != 0 && lift_level < lift_loadLevel )
+            lift_cmd = lift_CMD_TOP;
+          else
+            lift_cmd = lift_CMD_BOTTOM;
+          lift_loadPending = 1;
+          lift_loadSensor = 0;
+        } else
+          if ( lift_ctrl_io_in[lift_GO_TOP] ) {
+            if ( !lift_ctrl_io_in[lift_SENS_TOP] )
+              lift_cmd = lift_CMD_TOP;
+          } else
+            if ( lift_ctrl_io_in[lift_GO_BOTTOM] ) {
+              if ( !lift_ctrl_io_in[lift_SENS_BOTTOM] )
+                lift_cmd = lift_CMD_BOTTOM;
+            }
+  if ( lift_cmd != lift_CMD_NONE )
+    lift_timMotor = 50;
+}
+
+
+void lift_do_impulse( int val, int motor, int reset )
+{
+  if ( val && !lift_lastImp ) {
+    if ( motor || lift_timImp > 0 ) {
+      if ( lift_directionUp )
+        ++lift_cnt;
+      else
+        --lift_cnt;
+    }
+  }
+  if ( reset ) {
+    lift_cnt = 0;
+    lift_cntValid = 1;
+  }
+  lift_lastImp = val;
+  if ( lift_timImp > 0 ) {
+    --lift_timImp;
+    if ( lift_timImp == 0 && lift_cmd != lift_CMD_NONE )
+      lift_cmd = lift_CMD_NONE;
+  }
+}
+
+
+void lift_do_cmd()
+{
+  int run = 0;
+  if ( lift_timMotor > 0 )
+    lift_wait_for_motor_start();
+  else {
+    run = lift_check_run();
+    if ( lift_ctrl_io_out[lift_MOTOR_ON] && !run ) {
+      /* motor stopped: */
+      lift_cmd = 99;
+      lift_timImp = 50;
+    }
+    lift_ctrl_io_out[lift_MOTOR_ON] = run;
+  }
+}
+
+
+void lift_wait_for_motor_start()
+{
+  int newLevel = 0;
+  --lift_timMotor;
+  lift_directionUp = ( lift_cmd == lift_CMD_UP || lift_cmd == lift_CMD_TOP );
+  lift_ctrl_io_out[lift_MOTOR_UP] =  lift_directionUp;
+  if ( !lift_cntValid ) {
+    lift_cnt = 0;   /* use relative counter */
+    if ( lift_cmd == lift_CMD_UP )
+      lift_endCnt = lift_one_level;
+    else
+      lift_endCnt = -lift_one_level;
+  } else {
+    lift_endCnt = lift_cnt;
+    newLevel = -99;
+    if ( lift_cmd == lift_CMD_UP )
+      newLevel = lift_level + 1;
+    else
+      if ( lift_cmd == lift_CMD_DOWN )
+        newLevel = lift_level - 1;
+    --newLevel; /* lift_level is one based */
+    if ( newLevel >= 0 && newLevel < 14 )
+      lift_endCnt = lift_levelPos[newLevel];
+  }
+}
+
+
+int lift_check_run()
+{
+  if ( lift_cmd == lift_CMD_UP ) {
+    if ( lift_cnt < lift_endCnt - 1 && !lift_ctrl_io_in[lift_SENS_TOP] )
+      return 1;
+  } else
+    if ( lift_cmd == lift_CMD_DOWN ) {
+      if ( lift_cnt > lift_endCnt + 1 && !lift_ctrl_io_in[lift_SENS_BOTTOM] )
+        return 1;
+    } else
+      if ( lift_cmd == lift_CMD_TOP ) {
+        if ( lift_loadPending && lift_ctrl_io_in[lift_SENS_LOAD] ) {
+          /* we are at lift_load position */
+          lift_loadLevel = lift_level;
+          lift_loadPending = 0;
+          return 0;
+        }
+        if ( !lift_ctrl_io_in[lift_SENS_TOP] )
+          return 1;
+        /* safe fallback if lift_load sensor does not work */
+        lift_loadPending = 0;
+      } else
+        if ( lift_cmd == lift_CMD_BOTTOM ) {
+          if ( lift_loadPending ) {
+            if ( lift_loadSensor ) {
+              if ( !lift_ctrl_io_in[lift_SENS_LOAD] ) {
+                lift_loadSensor = 0;
+                /* we are at lift_load position */
+                lift_loadPending = 0;
+                lift_loadLevel = lift_level;
+                return 0;
+              }
+            }
+            lift_loadSensor = lift_ctrl_io_in[lift_SENS_LOAD];
+          }
+          if ( !lift_ctrl_io_in[lift_SENS_BOTTOM] )
+            return 1;
+        }
+  return 0;
+}
diff --git a/test/monniaux/tacle-bench-lift/liftlibcontrol.h b/test/monniaux/tacle-bench-lift/liftlibcontrol.h
new file mode 100644
index 00000000..2c6669e8
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/liftlibcontrol.h
@@ -0,0 +1,64 @@
+#ifndef LIFTLIBCONTROL_H
+#define LIFTLIBCONTROL_H
+
+enum lift_Direction {
+  lift_GO_LOAD = 8,
+  lift_GO_TOP = 6,
+  lift_GO_BOTTOM = 7,
+  lift_GO_UP = 4,
+  lift_GO_DOWN = 5
+};
+
+enum lift_Sensor {
+  lift_SENS_IMPULS = 0,
+  lift_SENS_TOP = 1,
+  lift_SENS_BOTTOM = 2,
+  lift_SENS_LOAD = 3
+};
+
+enum lift_Motor {
+  lift_MOTOR_ON = 0,
+  lift_MOTOR_UP = 1
+};
+
+enum lift_Command {
+  lift_CMD_NONE = 0,
+  lift_CMD_TOP = 1,
+  lift_CMD_BOTTOM = 2,
+  lift_CMD_UP = 3,
+  lift_CMD_DOWN = 4
+};
+
+/* Global variables */
+extern int lift_levelPos[16];
+extern int lift_one_level;
+extern int lift_cntValid;
+extern int lift_cnt;
+extern int lift_level;
+extern int lift_loadLevel;
+extern int lift_loadPending;
+extern int lift_loadSensor;
+extern int lift_cmd;
+extern int lift_timMotor;
+extern int lift_timImp;
+extern int lift_directionUp;
+extern int lift_lastImp;
+extern int lift_dbgCnt;
+extern int lift_endCnt;
+
+/* Checksum */
+extern int lift_checksum;
+
+/* prototypes */
+void lift_ctrl_init(void); /* DM prototype */
+void lift_ctrl_loop(void); /* DM prototype */
+
+/* internal prototypes */
+int lift_check_run(void);
+void lift_wait_for_motor_start(void);
+void lift_do_cmd(void);
+void lift_do_impulse( int val, int motor, int reset );
+void lift_check_cmd(void);
+void lift_check_level(void);
+
+#endif
diff --git a/test/monniaux/tacle-bench-lift/liftlibio.c b/test/monniaux/tacle-bench-lift/liftlibio.c
new file mode 100644
index 00000000..f61df2d0
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/liftlibio.c
@@ -0,0 +1,65 @@
+#include "liftlibio.h"
+
+/* Global variables */
+int lift_ctrl_io_in[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
+int lift_ctrl_io_out[4] = {0, 0, 0, 0};
+int lift_ctrl_io_analog[4] = {0, 0, 0, 0};
+int lift_ctrl_io_led[16] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
+int lift_ctrl_dly1;
+int lift_ctrl_dly2;
+
+/* Simulated hardware */
+volatile int lift_simio_in;
+volatile int lift_simio_out;
+volatile int lift_simio_led;
+volatile int lift_simio_adc1;
+volatile int lift_simio_adc2;
+volatile int lift_simio_adc3;
+
+void lift_io_init()
+{
+  lift_ctrl_dly1 = 0;
+  lift_ctrl_dly2 = 0;
+}
+
+
+void lift_ctrl_set_vals()
+{
+  int val = 0, i;
+  _Pragma( "loopbound min 4 max 4" )
+  for ( i = 4 - 1; i >= 0; --i ) {
+    val <<= 1;
+    val |= lift_ctrl_io_out[i] ? 1 : 0;
+  }
+  lift_simio_out = val;
+  _Pragma( "loopbound min 16 max 16" )
+  for ( i = 14 - 1; i >= 0; --i ) {
+    val <<= 1;
+    val |= lift_ctrl_io_led[i] ? 1 : 0;
+  }
+  lift_simio_led = val;
+  lift_checksum += val;
+}
+
+
+void lift_ctrl_get_vals()
+{
+  int i;
+  unsigned short int in0 = lift_simio_in;
+  unsigned short int in1 = lift_ctrl_dly1;
+  unsigned short int in2 = lift_ctrl_dly2;
+  lift_ctrl_dly2 = lift_ctrl_dly1;
+  lift_ctrl_dly1 = in0;
+  /* majority voting for input values
+     delays input value change by one period */
+  _Pragma( "loopbound min 10 max 10" )
+  for ( i = 0; i < 10; ++i ) {
+    lift_ctrl_io_in[i] = ( ( in0 & 1 ) + ( in1 & 1 ) + ( in2 & 1 ) ) > 1;
+    in0 >>= 1;
+    in1 >>= 1;
+    in2 >>= 1;
+  }
+  lift_ctrl_io_analog[0] = lift_simio_adc1;
+  lift_ctrl_io_analog[1] = lift_simio_adc2;
+  lift_ctrl_io_analog[2] = lift_simio_adc3;
+}
diff --git a/test/monniaux/tacle-bench-lift/liftlibio.h b/test/monniaux/tacle-bench-lift/liftlibio.h
new file mode 100644
index 00000000..1a67cfb5
--- /dev/null
+++ b/test/monniaux/tacle-bench-lift/liftlibio.h
@@ -0,0 +1,27 @@
+#ifndef LIFTLIBIO_H
+#define LIFTLIBIO_H
+
+/* Global variables */
+extern int lift_ctrl_io_in[10];
+extern int lift_ctrl_io_out[4];
+extern int lift_ctrl_io_analog[4];
+extern int lift_ctrl_io_led[16];
+extern int lift_ctrl_dly1, lift_ctrl_dly2;
+
+/* Simulated hardware */
+extern volatile int lift_simio_in;
+extern volatile int lift_simio_out;
+extern volatile int lift_simio_led;
+extern volatile int lift_simio_adc1;
+extern volatile int lift_simio_adc2;
+extern volatile int lift_simio_adc3;
+
+/* Checksum */
+extern int lift_checksum;
+
+/* prototypes */
+void lift_io_init( void );
+void lift_ctrl_get_vals( void );
+void lift_ctrl_set_vals( void );
+
+#endif