Initial State Dependence Checker #6
Description
Design an LC3 implementation and calling routine that checks a program for dependence on non-assigned registers or memory locations. On failure, produces initial conditions that can be played to demonstrate the failure. This analysis runs the risk of being halting problem'd if done improperly.
Potentially using rust z3 bindings on bitfields to test uninitialized values. May need z3 constraint generation methods for Instruction types. Validity checks on z3 constrained values would be that none of the failure conditions can be met, and then generating all the non-failure conditions. Programs that modify their own instructions produce a lot of complication for this analysis. Would need to create multiple copies to evaluate on diverging valid branches. Would also need to create multiple copies when the produced instruction is variable.
Brainstormed ways in which a program might fail a check:
- Takes too many steps to finish analysis (heuristic for avoiding hard infinite loops/unbounded computation)
- Due to this it is possible that a program eventually runs to correct competition, but takes too long to do so. If strict correctness is needed, the user would need to analyze the example manually to confirm an infinite loop.
- Infinite loop detected due to repeat with no side effect where looping is entirely via JMP or a BR with a status register that will not change (pretty difficult analysis, may skip)
- Causes a regular LC3 error via permission exception or invalid instruction
- Attempts to execute an uninitialized memory location (since at least one random initialization produces a non-instruction)
- Attempts to execute a memory location that, on some initialization, is an invalid instruction