check.sh: Update variable parsing/splitting to use awk

This allows for greater flexibility on managing local variables as vars
will be split into:

global_vars = << ... >>
local_vars = << ... >>
vars = << global_vars, local_vars, pc, stack >>

Signed-off-by: Catalin Marinas <catalin.marinas@arm.com>

3 files changed, 91 insertions, 10 deletions

diff --git a/check.sh b/check.sh
index f7c228c..917b516 100755
--- a/check.sh
+++ b/check.sh
@@ -21,10 +21,7 @@ if grep -q -e "^\s*ProcessEnabled(self)\s*==" $SPEC.tla; then
 	sed -i -e 's%pc\[self\] = ".*"$%& /\\\ ProcessEnabled(self)%' $SPEC.tla
 fi
 
-# Split << pc, stack >> out of the default vars and generate proc_vars
-# Match single line and multiline patterns
-SUBST="{s/\<vars\>/proc_vars/;s/\<pc,\s*\|\<stack,\s*//g;s/>>/>>\n     vars == << proc_vars, pc, stack >>/}"
-sed -i -e "/^vars\s*==.*>>$/$SUBST" $SPEC.tla
-sed -i -e "/^vars\s*==[^>]*/,/>>$/$SUBST" $SPEC.tla
+# Generate{global,local}_vars
+gawk -i inplace -f varsplit.awk $SPEC.tla
 
 tlc -workers $(nproc) $@ $SPEC.tla | tee -a $SPEC.log
diff --git a/ctxsw.tla b/ctxsw.tla
index f5b3698..ff53dd2 100644
--- a/ctxsw.tla
+++ b/ctxsw.tla
@@ -306,10 +306,9 @@ Perms   == Permutations(PROCS) \cup Permutations(TASKS) \cup Permutations(MMS)
 
 VARIABLES _mm_, _mm_m, _mm, prev, next, oldmm
 
-proc_vars == << task, mm, proc_mm, interrupts, prev_mm, freemms, runqueue, 
-           _mm_, _mm_m, _mm, prev, next, oldmm >>
-
-vars == << proc_vars, pc, stack >>
+global_vars == << prev_mm, freemms, proc_mm, task, mm, runqueue, interrupts >>
+local_vars == << next, prev, _mm_m, oldmm, _mm, _mm_ >>
+vars == << global_vars, local_vars, pc, stack >>
 
 ProcSet == (TASKS) \cup (PROCS)
 
@@ -615,7 +614,7 @@ Interrupt(self) ==
 	\* non-reentrant handler
 	/\ pc[self] # "handle_irq"
 	/\ IntCall(self, "interrupt", "handle_irq")
-	/\ UNCHANGED proc_vars
+	/\ UNCHANGED << global_vars, local_vars >>
 
 PreemptNext == (\E self \in ProcSet : Interrupt(self)) \/ Next
 
diff --git a/varsplit.awk b/varsplit.awk
new file mode 100755
index 0000000..e84df79
--- /dev/null
+++ b/varsplit.awk
@@ -0,0 +1,85 @@
+#!/usr/bin/gawk -f
+
+function parse_vars(vars_set)
+{
+	print
+
+	# read subsequent lines if the current one finishes with a comma
+	line = $0
+	while (/,[ \t]*/) {
+		if ((getline) > 0) {
+			print
+			line = line $0
+		}
+	}
+
+	# extract the variable names and build a set
+	n = split(line, vars, /[, \t]+/)
+	for (i = 2; i <= n; i++)
+		vars_set[vars[i]] = ""
+}
+
+function print_vars(name, vars_set)
+{
+	len = length(vars_set)
+	i = 1
+	printf("%s == << ", name)
+	for (v in vars_set) {
+		printf("%s", v)
+		if (i < len)
+			printf(", ")
+		i++
+	}
+	printf(" >>\n")
+}
+
+BEGIN {
+	mode = ""
+}
+
+# Only transform the PlusCal generated code
+/^\\\* BEGIN TRANSLATION/ {
+	mode = "gvars"
+}
+
+# Global variable parsing (first encounter)
+mode == "gvars" && /^VARIABLE/ {
+	parse_vars(global_vars)
+
+	# delete pc and stack
+	delete global_vars["pc"]
+	delete global_vars["stack"]
+
+	mode = "lvars"
+	next
+}
+
+# Local variable parsing (second encounter)
+mode == "lvars" && /^VARIABLE/ {
+	parse_vars(local_vars)
+
+	mode = "vars"
+	next
+}
+
+# Replace the "vars" definition
+mode == "vars" && /^vars[ \t]*==[ \t]*<</ {
+	# find the end angle brackets
+	while ($0 !~ />>/) {
+		if ((getline) <=0)
+			break
+	}
+
+	# print the new var definitions
+	print_vars("global_vars", global_vars)
+	print_vars("local_vars", local_vars)
+	print "vars == << global_vars, local_vars, pc, stack >>"
+
+	mode = ""
+	next
+}
+
+# Default mode, print everything
+{
+	print
+}