Using Concolic Execution to Provide Automatic Feedback on LC-3 Programs

Liu, Zikai

Permalink

https://hdl.handle.net/2142/110284 Copy

Description

Title

Using Concolic Execution to Provide Automatic Feedback on LC-3 Programs

Author(s)

Liu, Zikai

Contributor(s)

Lumetta, Sreven

Issue Date

2021-05

Keyword(s)

• concolic testing
• assembly language
• teaching programming
• student feedback

Abstract

Students in introductory programming courses need quick and targeted feedback to make progress in learning the difficult task of programming, but staff to provide such feedback are often in short supply or simply unavailable when a student is studying. In this thesis, we present KLC3, a concolic execution engine for LC-3 assembly built upon KLEE. With novel symbolic executor, memory model, and other modules, we can precisely identify improper operations in an LC-3 program (such as accessing an undefined memory location) and its discrepancies with a correct version of the code (such as printing different characters to the display). Human-readable reports, test cases, and scripts are generated automatically to help students debug their code. KLC3 was deployed to provide automatic feedback to over 100 students taking ECE220 at the joint ZJUUIUC campus in Fall 2020. Student feedback was solicited anonymously and was uniformly positive. To meet our goal of providing feedback in 5 minutes for any submission, we apply a series of optimizations. A cache is added to the relevant constraint solver of KLEE to avoid redundant iterations, which reduces the 5-minute timeout rate from 65.1% to 13.5% for 960 student submissions of a complicated LC-3 assignment. Loop path reduction, a KLEE search heuristic originally proposed for C assignments, is generalized to assembly programming and implemented in KLC3. With the optimizations, we are now able to test the full set of 3188 LC-3 student programs from Fall 2020 using sufficiently large symbolic input spaces while keeping the 5-minute timeout rate to 4.08%. For each of the remaining samples--those that time out--KLC3 detects problems and provides insightful feedback. Some optimizations show possible benefits for the original KLEE and when used in other applications.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/110284

Owning Collections