A Framework for Automatically Verifying Students’ Assembly-language Translations of C Functions

Bryan A. Jones

Download Paper | Permalink

Conference: 2019 ASEE Annual Conference & Exposition
Location: Tampa, Florida
Publication Date: June 15, 2019
Start Date: June 15, 2019
End Date: June 19, 2019
Conference Session: Insights for Teaching ECE Courses - Session I
Tagged Division: Electrical and Computer
Page Count: 13
DOI: 10.18260/1-2--31956
Permanent URL: https://peer.asee.org/31956
Download Count: 575

Request a correction

Paper Authors

biography

Bryan A. Jones Mississippi State University

visit author page

Bryan A. Jones received the B.S.E.E. and M.S. degrees in electrical engineering from Rice University, Houston, TX, in 1995 and 2002, respectively, and the Ph.D. degree in electrical engineering from Clemson University, Clemson, SC, in 2005. He is currently an Associate Professor at Mississippi State University, Mississippi State, MS.

From 1996 to 2000, he was a Hardware Design Engineer with Compaq, where he specialized in board layout for high-availability redundant array of independent disks (RAID) controllers. His research interests include engineering education, robotics, and literate programming.

visit author page

Download Paper | Permalink

Abstract

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.

Citation
Format

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

TY - CPAPER
AB - 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.

AU - Bryan A. Jones
CY - Tampa, Florida
DA - 2019/06/15
PB - ASEE Conferences
TI - A Framework for Automatically Verifying Students’ Assembly-language Translations of C Functions
UR - https://peer.asee.org/31956
DO - 10.18260/1-2--31956
ER -