Merge pull request #492 from lf-lang/time-overflows

Subtract time with care for overflow

core/tag.c

@@ -58,6 +58,25 @@ instant_t lf_time_add(instant_t a, interval_t b) {
   return res;
 }
 
+instant_t lf_time_subtract(instant_t a, interval_t b) {
+  if (a == NEVER || b == FOREVER) {
+    return NEVER;
+  }
+  if (a == FOREVER || b == NEVER) {
+    return FOREVER;
+  }
+  instant_t res = a - b;
+  // Check for overflow
+  if (res < a && b < 0) {
+    return FOREVER;
+  }
+  // Check for underflow
+  if (res > a && b > 0) {
+    return NEVER;
+  }
+  return res;
+}
+
 tag_t lf_tag_add(tag_t a, tag_t b) {
   instant_t res = lf_time_add(a.time, b.time);
   if (res == FOREVER) {

core/threaded/reactor_threaded.c

@@ -586,7 +586,7 @@ void _lf_initialize_start_tag(environment_t* env) {
   // If we have a non-zero STA offset, then we need to allow messages to arrive
   // at the start time.  To avoid spurious STP violations, we temporarily
   // set the current time back by the STA offset.
-  env->current_tag.time -= lf_fed_STA_offset;
+  env->current_tag.time = lf_time_subtract(env->current_tag.time, lf_fed_STA_offset);
 #else
   // For other than federated decentralized execution, there is no lf_fed_STA_offset variable defined.
   // To use uniform code below, we define it here as a local variable.

tag/api/tag.h

@@ -110,6 +110,15 @@ tag_t lf_tag_add(tag_t a, tag_t b);
  */
 instant_t lf_time_add(instant_t a, interval_t b);
 
+/**
+ * @brief Return an instant minus an interval, saturating on overflow and underflow.
+ *
+ * @param a
+ * @param b
+ * @return instant_t
+ */
+instant_t lf_time_subtract(instant_t a, interval_t b);
+
 /**
  * Compare two tags. Return -1 if the first is less than
  * the second, 0 if they are equal, and +1 if the first is