June 15, 2019
June 15, 2019
October 19, 2019
Electrical and Computer
Assembly language instruction represents a core required skill for many computer science and electrical and computer engineering curriculums. A common approach in assembly language pedagogy involves teaching students to translate from C to assembly. Unfortunately, the typical approach to verifying the correctness of these translations lacks rigor. This paper presents a comprehensive, carefully-designed framework to improve this process along with results gained from its use in an introductory course on microprocessors.
The field of software and compiler testing provides a rich background which this work builds on. This work directly incorporates Miro Samek’s method of providing assertions specialized to limit memory use and occupy static (flash) memory. Kent Beck’s original xUnit testing methodology and the growth of the test-driven development (TDD) paradigm provide a philosophical underpinning for this work, in which the correctness of student code must be quickly verifiable by an automatic process. James Grenning’s work in adapting TDD for embedded C applications illustrates methods for testing code in the absence of actual hardware using mocks and stubs. Google’s ASans tool and the field of fuzzing demonstrates the possibility of much deeper automatic verification; however, the high resource requirements for these tools make them impractical in this application.
Verifying the correctness of an assembly language program presents several unique opportunities and challenges. Most importantly, the correct translation can always be obtained by compiling the C program the students must translate. This opens up the possibility of highly-effective automatic verification methods. However, the general problem of determining the equality of two arbitrary functions is undecidable. In addition, the limited resources of most microcontrollers exclude the use of many useful tools, such as: C++ or other high-level languages and their well-developed testing frameworks; approaches which require hundreds of bytes of memory; and approaches which are computationally expensive. Therefore, this approach relies on a reasonable set of common-sense assumptions which hold for most pedagogically-relevant cases.
At its core, this pure C framework provides a func_compare macro which invokes the known-correct C function using a set of instructor-provided test vectors. The framework then compares these results against the results obtained by invoking the student-written assembly function using the same test vectors. Verbose diagnostic output in the case of a failure assists students in correcting their mistakes. A wide range of supporting tools enables instructors to develop a large suite of high-quality tests. Specifically, this framework enabled the creation of 125 programming examples and exercises for an on-line, interactive e-book covering the use of the PIC24 family of microcontrollers. The e-book framework allows students to get immediate, in-browser feedback on their assembly programs based on the output from this framework. Results from an introductory course in microprocessors based on this e-book and its underlying framework demonstrate its effectiveness in improving pedagogy for microcontroller instruction.
Jones, B. A. (2019, June), A Framework for Automatically Verifying Students’ Assembly-language Translations of C Functions Paper presented at 2019 ASEE Annual Conference & Exposition , Tampa, Florida. 10.18260/1-2--31956
ASEE holds the copyright on this document. It may be read by the public free of charge. Authors may archive their work on personal websites or in institutional repositories with the following citation: © 2019 American Society for Engineering Education. Other scholars may excerpt or quote from these materials with the same citation. When excerpting or quoting from Conference Proceedings, authors should, in addition to noting the ASEE copyright, list all the original authors and their institutions and name the host city of the conference. - Last updated April 1, 2015