Added verification tool

firmware/.gitignore

@@ -14,3 +14,9 @@ xdk*
 
 # ETAGS file
 TAGS
+
+# CTypesgen
+tools/verification/ctypesgen
+
+# Compiled python
+*.pyc

firmware/Makefile

@@ -111,9 +111,14 @@ endif
 # Startup and system code
 #
 #
-SYSTEM		?= chip/startup_samd20.c chip/system_samd20.c
+SYSTEM		?= chip/system_samd20.c chip/startup_samd20.c
 INCLUDE_PATH	+= chip/ chip/cmsis/ samd20/ samd20/component/
 
+# Verification suite code
+#
+#
+SYSTEM		+= tools/verification/verification_tc.c
+
 # Linker Scripts
 #
 #
@@ -214,7 +219,7 @@ gdbscript: Makefile config.mk
 	@$(ECHO) "file $(TARGET).elf" >> gdbscript
 ifdef BLACKMAGIC_PATH
 	@$(ECHO) "# Connect to a specified blackmagic" >> gdbscript
-	@$(ECHO) "target external-remote $(BLACKMAGIC_PATH)" >> gdbscript
+	@$(ECHO) "target extended-remote $(BLACKMAGIC_PATH)" >> gdbscript
 endif
 
 # Prints a list of symlinks to a device
@@ -248,4 +253,4 @@ emacs:
 clean:
 	$(RM) $(OUTPUT_PATH)*
 	$(RM) gdbscript
-	$(RM) TAGS
+	$(RM) TAGS

firmware/chip/sections.ld

@@ -68,6 +68,11 @@ SECTIONS
 		*(.rodata .rodata* .gnu.linkonce.r.*)
 		*(.ARM.extab* .gnu.linkonce.armextab.*)
 
+		/* Verification functions are protected from optimisation and
+		by being placed in their own section */
+
+		KEEP(*(.text.verif .text.verif.*))
+
 		/* Support C constructors, and C destructors in both user code
 		and the C library. This also provides support for C++ code. */
 

firmware/tools/get-python-deps.sh

@@ -0,0 +1,4 @@
+#!/bin/sh
+
+sudo apt-get install python-pip
+sudo pip install colorama

firmware/tools/get_arm-none-eabi-gdb_with_python.sh

@@ -0,0 +1,71 @@
+#!/bin/bash
+
+# ------------------------------------------------------------------------------
+# Get arm-none-eabi-gdb with python support
+# Should take about 15 minutes
+# ------------------------------------------------------------------------------
+
+mkdir gdb-build
+cd gdb-build
+
+# Grab the pre-requisites
+sudo apt-get install apt-src \
+gawk \
+gzip \
+perl \
+autoconf \
+m4 \
+automake \
+libtool \
+libncurses5-dev \
+gettext \
+gperf \
+dejagnu \
+expect \
+tcl \
+autogen \
+flex \
+flip \
+bison \
+tofrodos \
+texinfo \
+g++ \
+gcc-multilib \
+libgmp3-dev \
+libmpfr-dev \
+debhelper \
+texlive \
+texlive-extra-utils
+
+# Grab the sources - UPDATE WITH LATEST SOURCES
+#wget https://launchpad.net/gcc-arm-embedded/4.8/4.8-2014-q2-update/+download/gcc-arm-none-eabi-4_8-2014q2-20140609-src.tar.bz2
+
+# Extract
+tar xjf gcc*
+cd gcc*
+
+# Extract gdb
+cd src
+tar xf gdb*
+cd gdb*
+
+# Configure
+host_arch=`uname -m | sed 'y/XI/xi/'`
+PKGVERSION="GNU Tools for ARM Embedded Processors --with-python=yes"
+
+./configure --target=arm-none-eabi \
+    --disable-nls \
+    --disable-sim \
+    --with-libexpat \
+    --with-python=yes \
+    --with-lzma=no \
+    --build=$host_arch-linux-gnu --host=$host_arch-linux-gnu \
+    --with-pkgversion="$PKGVERSION"
+
+# Make (j = Ncores + 1)
+make -j3
+sudo make install
+
+# Cleanup
+cd ../../../..
+#sudo rm -rf gdb-build

firmware/tools/verification/.dir-locals.el

@@ -0,0 +1,32 @@
+;; Emacs settings for this project
+;; Copyright (C) 2013  Richard Meadows
+;;
+;; Permission is hereby granted, free of charge, to any person obtaining
+;; a copy of this software and associated documentation files (the
+;; "Software"), to deal in the Software without restriction, including
+;; without limitation the rights to use, copy, modify, merge, publish,
+;; distribute, sublicense, and/or sell copies of the Software, and to
+;; permit persons to whom the Software is furnished to do so, subject to
+;; the following conditions:
+;;
+;; The above copyright notice and this permission notice shall be
+;; included in all copies or substantial portions of the Software.
+;;
+;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+;; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+;; MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+;; NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+;; LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+;; OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+;; WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+;;; Directory Local Variables
+;;; See Info node `(emacs) Directory Variables' for more information.
+
+;; Use a special debugger for arm targets
+;; Keep this directory as the default directory when navigating subdirectoies
+
+((nil
+  (gud-gdb-command-name . "arm-none-eabi-gdb -i=mi")
+  (eval setq default-directory
+	(locate-dominating-file buffer-file-name ".dir-locals.el"))))

firmware/tools/verification/Makefile

@@ -0,0 +1,8 @@
+# Makefile for verification tests
+
+all: verification_tc.py
+
+%.py: %.c
+	@echo "Generating Python Wrappers...."
+	@echo
+	ctypesgen/ctypesgen.py -o $@ --cpp="gcc -E -DCTYPESGEN" $<

firmware/tools/verification/tc/times_two.py

@@ -0,0 +1,36 @@
+#!/usr/bin/env python
+
+# ------------------------------------------------------------------------------
+# Imports
+# ------------------------------------------------------------------------------
+
+import os
+import sys
+sys.path.append("./tools/verification")
+from verification import *
+import verification_tc
+
+# ------------------------------------------------------------------------------
+# Test Script
+# ------------------------------------------------------------------------------
+
+class times_two_tc:
+    def __init__(self, tester):
+        self.name = self.__class__.__name__
+
+        tester.print_header(self.__class__.__name__)
+
+        params = verification_tc.struct_times_two_tc_params()
+        params.input = 4
+
+        result = tester.run_tc(self.name, params)
+
+        tester.print_info(str(result))
+
+# ------------------------------------------------------------------------------
+# Run test
+# ------------------------------------------------------------------------------
+
+tester = samd20_test()
+times_two_tc(tester)
+del tester

firmware/tools/verification/verification.py

@@ -0,0 +1,98 @@
+#!/usr/bin/env python
+
+# ------------------------------------------------------------------------------
+# Verification Framework
+# ------------------------------------------------------------------------------
+# This script is inteneded to be run from inside gdb, with gdb already
+# attached to the target - probably this is done in .gdbinit.
+#
+# You should be running gdb like this:
+#
+# arm-none-eabi-gdb -q -x tools/verification/tc/my_tc.py
+#
+#
+# The useful output from this script appears on stderror, sorry about
+# that. Hence you should supress stdout if you don't want loads of
+# info from gdb.
+#
+# Something like this should work:
+# > /dev/null arm-none-eabi-gdb -q -x tools/verfication/tc/my_tc.py
+#
+# ------------------------------------------------------------------------------
+
+from __future__ import print_function
+
+import gdb
+import re
+import sys
+from time import *
+from colorama import *
+
+
+def printf(string):
+        print (string, file=sys.stderr)
+
+LINE_LENGTH = 80
+
+class samd20_test:
+
+        # Prints something in the centre of the line
+        def print_centre(self, string):
+                count = (LINE_LENGTH - len(string)) / 2
+                printf ((" " * count) + string)
+
+        # Prints a pretty header
+        def print_header(self, string):
+                printf (Fore.YELLOW)
+                printf (("*" * LINE_LENGTH) + Fore.RESET)
+                self.print_centre(string)
+                printf (Fore.YELLOW + ("*" * LINE_LENGTH) + Fore.RESET)
+
+        def print_info(self, string):
+                """Prints an info line"""
+                printf(Fore.CYAN + "\nINFO    " + Fore.RESET + string + "\n\n")
+
+        #### GDB
+
+        def __init__(self):
+                self.inferior = gdb.selected_inferior()
+
+                # Load everything into gdb and run
+                gdb.execute("load")
+                gdb.execute("b main")
+                gdb.execute("run")
+
+                # Stopped at the top of main. Go to tc_main
+                gdb.execute("del 1")
+                gdb.execute("b tc_main")
+                gdb.execute("set $pc=tc_main")
+                gdb.execute("c")
+
+        def __del__(self):
+                self.print_info("quit")
+                gdb.execute("quit")
+
+
+        def run_tc(self, tc_name, parameters):
+                """Runs a test case"""
+
+                # Write the parameters
+                self.write_varible(tc_name+"_params", parameters)
+
+                # Presuming there"s a breakpoint at the top of tc_main
+                gdb.execute("set $lr=$pc")
+                gdb.execute("set $pc="+tc_name)
+                gdb.execute("c")
+
+                # Test case done. Return results
+                return self.read_variable(tc_name+"_results")
+
+        #### Read / Write
+
+        def read_variable(self, name):
+                gdb.execute("p " + name, to_string=True)
+                return gdb.history(0)
+
+        def write_varible(self, name, value):
+                pvar = self.read_variable(name)
+                self.inferior.write_memory(pvar.address, value)

firmware/tools/verification/verification_tc.c

@@ -0,0 +1,80 @@
+/*
+ * C stubs for verification suite test cases
+ * Copyright (C) 2014  Richard Meadows <richardeoin>
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining
+ * a copy of this software and associated documentation files (the
+ * "Software"), to deal in the Software without restriction, including
+ * without limitation the rights to use, copy, modify, merge, publish,
+ * distribute, sublicense, and/or sell copies of the Software, and to
+ * permit persons to whom the Software is furnished to do so, subject to
+ * the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+ * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+ * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+
+/* CTypes just gets confused by function attributes... */
+#ifdef CTYPESGEN
+#define __verification__
+
+#else
+#define __verification__ \
+  __attribute__ ((section(".text.verif"))) \
+  __attribute__ ((optimize("O0")))	   \
+
+#endif
+
+/****************************//* nmea_decode_tc *//****************************/
+
+/* Parameters in */
+struct nmea_decode_tc_params {
+  int in;
+} nmea_decode_tc_params;
+/* Results out */
+struct nmea_decode_tc_results {
+  int result;
+} nmea_decode_tc_results;
+/* Function */
+__verification__ void nmea_decode_tc(void) {
+
+  nmea_decode_tc_results.result = 2 * nmea_decode_tc_params.in;
+}
+
+/****************************//* times_two_tc *//****************************/
+/* The simplest test case. ever.   Used to check for sanity                 */
+
+/* Parameters in */
+struct times_two_tc_params {
+  int input;
+} times_two_tc_params;
+/* Results out */
+struct times_two_tc_results {
+  int result;
+} times_two_tc_results;
+/* Function */
+__verification__ void times_two_tc(void) {
+
+  times_two_tc_results.result = 2 * times_two_tc_params.input;
+}
+
+/*******************************//* tc_main *//********************************/
+
+/**
+ * Called at the start of the test case run
+ */
+__verification__ void tc_main(void) {
+  /* Test enviroment initialisation */
+
+  /* Wait forever while test cases execute */
+  while (1);
+}