Asee peer logo

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

Download Paper |

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

Permanent URL

https://peer.asee.org/31956

Download Count

2

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 |

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.

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. https://peer.asee.org/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