main restrucuring symbolic jobs, SRP.x files simplified

include/SRP.h

@@ -34,5 +34,5 @@
 
 #define TASK(J)			void IRQh(J) ()
 
-#define BREAKPOINT      { asm volatile("" ::: "memory"); }
+#define BREAKPOINT      { asm volatile("nop" ::: "memory"); }
 

include/SRP_wcet.h

@@ -45,7 +45,6 @@ typedef struct locks
 } locks;
 
 
-
 int event_count = 0;
 
 /* Create array containing structs of type locks */
@@ -55,26 +54,17 @@ locks eventlist[MAX_NUM_LOCKS];
 #define TRACE_EVENT(event, el)({eventlist[event_count].time = DWT->CYCCNT; eventlist[event_count].action = event; eventlist[event_count].elem = el; event_count+=1;})
 
 
-// #define Ceiling(R)		(R##_Ceiling)
-// #define Code(J)			(J##_Code)
-// #define IRQn(J) 		(J##_IRQn)
-// #define H(X)			((1 << __NVIC_PRIO_BITS)-X)
 #define IRQh(J) 		(J##_IRQh)
 
-// #define BARRIER_LOCK 	{ }
-// #define BARRIER_UNLOCK 	{ }
 #define JOB_REQUEST(J)	{ }
 
 #define LOCK(X) 		TRACE_EVENT(L, X);
 #define UNLOCK(X) 		TRACE_EVENT(R, X);
 
-// #define SETPRIO(J)		{ }
-// #define ENABLE(J)		{ }
-
 #define TASK(J)			void IRQh(J) ()
 
-#define BREAKPOINT      { asm volatile("" ::: "memory"); }
+#define BREAKPOINT
 
 void finish_execution(void) {}
-void terminate_execution(void) {}
+//void terminate_execution(void) {}
 

src/main.c

 //#define KLEE
+#define KLEE_WCET
 
 #ifdef KLEE
 #include "SRP_klee.h"
-#elif KLEE_WCET
+#define TRACE(X)	{}
+
+#elif defined KLEE_WCET
 #include "SRP_wcet.h"
+#define TRACE(X)	{}
+
 #else
-#include "main.h"
-#define enable_itm
-#endif
+// Production code
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
 
+#include "dwt.h"
+#include "Trace.h"
+
+#include <stm32f401xe.h>
+#include "SRP.h"
+
+#define TRACE(X) trace_printf(X)
+#endif
 
 // job bindings
 #define j1_IRQn EXTI1_IRQn
@@ -28,96 +42,113 @@
 #define r1_Ceiling 2
 #define r2_Ceiling 1
 
-static int state;
-
-void work(int i)
-{
+void work(int i) {
 	volatile int k = 0;
-    for (int j =0; j < 100 * i; j++)
-    {
+	for (int j = 0; j < 100 * i; j++) {
 		k++;
 	}
 }
 
-TASK(j1)
-{
+TASK(j1) {
+	TRACE("j1_enter\n");
 	LOCK(r2);
-
 	JOB_REQUEST(j2); 			// job execution request for j2
 
-    if (state > 0)
-    {
+	if (state > 0) {
 		work(10);
-    }
-    else
-    {
+	} else {
 		work(5);
 	}
 
 	LOCK(r1);
-#ifdef enable_itm
-    trace_printf("j1_r1_locked, before job request j2\n");
-#endif
+	TRACE("j1_r1_locked, before job request j2\n");
+
 	JOB_REQUEST(j2);
-#ifdef enable_itm
-    trace_printf("j1_r1_locked, after job request j2\n");
-#endif
+	TRACE("j1_r1_locked, after job request j2\n");
 	UNLOCK(r1);
 	UNLOCK(r2);
 }
 
-TASK(j2)
-{
-#ifdef enable_itm
-    trace_printf("j2_enter\n");
-#endif
+TASK(j2) {
+	TRACE("j2_enter\n");
 	LOCK(r1);
-#ifdef enable_itm
-    trace_printf("j2_r1_locked\n");
+	TRACE("j2_r1_locked\n");
 	work(5);
-
-#endif
 	UNLOCK(r1);
-#ifdef enable_itm
-    trace_printf("j2_exit\n");
-#endif
+	TRACE("j2_exit\n");
 }
 
 TASK(j3) {
-#ifdef enable_itm
-	trace_printf("j3_enter\n");
-#endif
+	TRACE("j3_enter\n");
 	LOCK(r1);
-#ifdef enable_itm
-		trace_printf("j3_r1_locked\n");
-#endif
+	TRACE("j3_r1_locked\n");
 	work(1);
-
 	UNLOCK(r1);
 	JOB_REQUEST(j1);
-#ifdef enable_itm
-	trace_printf("j3_exit\n");
-#endif
+	TRACE("j3_exit\n");
 }
 
-#ifdef KLEE_WCET
-// will be set by gdb
-static volatile int wcet_task;
-#endif
+#ifdef KLEE
+/* The case when KLEE makes the path analysis */
+static int state;
+static int job;
 
-int main()
-{
-#ifdef enable_itm
-    trace_printf("\nInit\n");
-#endif
+int main() {
+	klee_make_symbolic(&job, sizeof(job), "job");
 
-#ifndef KLEE
+	switch (job) {
+		case 1:
+		// check task 1
+		klee_make_symbolic(&state, sizeof(state), "state");
+		EXTI1_IRQHandler();
+		break;
+		case 2:
+		// check task 2
+		klee_make_symbolic(&state, sizeof(state), "state");
+		EXTI2_IRQHandler();
+		break;
+		case 3:
+		// check task 3
+		klee_make_symbolic(&state, sizeof(state), "state");
+		EXTI3_IRQHandler();
+		break;
+	}
+
+#elif defined KLEE_WCET
+/* The case when gdb runs WCET benchmarking */
+static int state;
+static int job;
+int main() {
 
 	dwt_enable();
 	DWT->CYCCNT = 0;
-#ifndef KLEE_WCET
 
+	switch (job) {
+	case 1:
+		TRACE_EVENT(S, j1);
+		EXTI1_IRQHandler();
+		TRACE_EVENT(E, j1);
+		break;
+	case 2:
+		TRACE_EVENT(S, j2);
+		EXTI2_IRQHandler();
+		TRACE_EVENT(E, j2);
+		break;
+	case 3:
+		TRACE_EVENT(S, j3);
+		EXTI3_IRQHandler();
+		TRACE_EVENT(E, j3);
+		break;
+	}
+
+	finish_execution();			// gdb breakpoint
+	// terminate_execution();
+}
+
+#else
 // this will be run in the production code
+int main() {
+	TRACE("\nInit\n");
 	SETPRIO(j1);				// Set HW priorities
 	SETPRIO(j2);
 	SETPRIO(j3);
@@ -125,39 +156,16 @@ int main()
 	ENABLE(j2);
 	ENABLE(j3);
 
-    //JOB_REQUEST(j1);			// comment out in assignment c
 	JOB_REQUEST(j3);// use in assignment c
 
-    BREAKPOINT;
-    while (1) ;
-    return 0;
-
-    /* The case when NOT running WCET benchmark nor KLEE-analysis */
-#else
-
-    TRACE_EVENT(S, j1);
-    EXTI1_IRQHandler();
-    TRACE_EVENT(E, j1);
-#endif
-
-    finish_execution();
-    terminate_execution();
+	BREAKPOINT
+	;
 
-#elif (JOB == 1)
-    // check task 1
-    klee_make_symbolic(&state, sizeof(state), "state");
-    EXTI1_IRQHandler();
-
-#elif (JOB == 2)
-    // check task 2
-    klee_make_symbolic(&state, sizeof(state), "state");
-    EXTI2_IRQHandler();
-#elif (JOB == 3)
-    // check task 3
-    klee_make_symbolic(&state, sizeof(state), "state");
-    EXTI3_IRQHandler();
-#endif
+	while (1)
+	;
+	return 0;
 }
+#endif
 
 /*
  Assignments