EECS 590代写、代做C++编程设计

日期：2025-04-10 10:20

Advanced Programming Languages

Homework Assignment 6F and 6C

EECS 590

Pairs. You may work with a partner for HW 6F and HW 6C. You may also work alone.

If you work with a partner, we expect roughly 1.5× the work described below from the

partnership (but not 2× — there is communication and teamwork overhead). If you work

with a partner then the partnership will submit one final PDF writeup (selecting the team

members on Gradescope) and one final code project (selecting the team members on the

autograder). You must indicate your partnership or solo status in the writeup text (see

below).

Logistics. The previous homework assignment was largely theoretical. This homework

assignment is largely practical. There is no peer review component for this homework as signment.

In class we have covered operational semantics (large- and small-step), axiomatic seman tics (including verification condition generation) and some abstract interpretation. You are

now qualified to pull ideas from many of those techniques together and create a non-trivial

program analysis.

This analysis will target off-the-shelf C programs. We will use the CIL library to parse and

process C programs into an IMP-like OCaml representation. We will use the Z3 automated

theorem prover of de Moura and Bjorner to reason about infeasible paths or otherwise decide

questions of logic.

Our analysis will automatically generate test inputs that will force the subject program

to cover all of its branches. This is undecidable in general (by direct reduction with the

halting problem). Automated test input (and test case) generation is a research problem

that is receiving quite a bit of attention; see the papers on the course webpage for more

information. This problem is also known as program reachability, the same issue we discussed

in the context of software model checking.

I have provided an introductory analysis. It performs flow-sensitive, path-sensitive,

context-insensitive, intraprocedural path enumeration, symbolic execution, and constraint

generation to create test inputs. Unlike previous assignments, for this assignment you may

change anything in the main file you like.

Initial steps:

1. Compile tigen, our test-input generation program. See the file README-GradPL.txt in

the code archive for details. Reproducing the systems research results of others is a

1

key part of modern research. Getting the code up and running is explicitly part of this

assignment and is your responsibility. Talk to your friends, post on the forum, scour

the Internet — do whatever it takes to make it happen.

2. Take a look at some of the included small subject programs. Think about how you

would generate test inputs to reach and cover all of their branches. Then run tigen

and inspect the test cases it actually creates.

As a sanity check, on my machine, the report.txt output is:

array-1.i.c : reached 0 / 4

array-2.i.c : reached 8 / 8

array-3.i.c : reached 0 / 10

array-4.i.c : reached 1 / 4

balanced.i.c : reached 4 / 8

bsearch-1.i.c : reached 4 / 8

bsearch-2.i.c : reached 6 / 8

bubblesort.i.c : reached 5 / 6

conway.i.c : reached 6 / 6

dotprod.i.c : reached 2 / 2

eq-index.i.c : reached 6 / 6

fibo.i.c : reached 6 / 6

float-1.i.c : reached 2 / 6

float-2.i.c : reached 7 / 8

float-3.i.c : reached 5 / 8

float-4.i.c : reached 4 / 14

float-5.i.c : reached 1 / 4

gcd.i.c : reached 4 / 4

hailstone.i.c : reached 5 / 6

leven.i.c : reached 7 / 10

many-features.i.c : reached 0 / 8

matmul.i.c : reached 3 / 6

matrix-path.i.c : reached 0 / 8

mymin-1.i.c : reached 7 / 8

roman.i.c : reached 21 / 28

selsort.i.c : reached 6 / 6

simple-1.i.c : reached 2 / 2

simple-2.i.c : reached 4 / 4

simple-3.i.c : reached 8 / 8

simple-4.i.c : reached 5 / 6

string.i.c : reached 0 / 8

struct-1.i.c : reached 3 / 10

struct-2.i.c : reached 0 / 8

struct-3.i.c : reached 0 / 18

struct-float.i.c : reached 0 / 16

subseqsum.i.c : reached 0 / 12

2

Your output may be slightly different, but if you are reaching significantly fewer

branches, you may be encountering a local setup or installation concern.

3. Read some of the papers associated with this homework on the course webpage.

This exercise is open-ended. You must do something to convince me that you have

an integrated understanding of the theory and practice of using PL research techniques to

analyze programs. More concretely, you must modify tigen.ml so that it is “better” in a

way of your choosing. As a rough estimate, I would expect a diff of your modified source

to indicate at least 200 changed lines. Then you must write up a formal three- or four paragraph explanation of what you did and why it was worthwhile. Your explanation should

motivate your changes and explain why the problem you tackled is important.

Any of the following could suffice:

• Modify tigen so that it handles string-valued data. Textual input generation is in creasingly popular, both using modern LLM-style techniques or traditional symbolic

approaches (e.g., some students have integrated the DPrle external decision procedure

to handle some string constraints). While not required, handling string or textual data

often involves inferring a grammar or regular expression constraints.

• Modify tigen so that it handles loops in an intelligent manner. For example, you

might use a dataflow-style join — if it is to possible reach the loop head knowing

x = 0 ∧ y = 55 and it is also possible to reach the loop head knowing x = 5 ∧ y = 55,

you should process the loop in a state where y = 55 (or, better yet, x ≥ 0 ∧ y = 55).

• Modify tigen so that it handles arrays. Note that Z3 already has built-in handling for

the McCarthy select and update axioms, but you’ll have to integrate it.

• Modify tigen so that it handles the heap (i.e., dynamic pointers) more precisely. For

example, you might introduce an explicit handling of malloc (which either returns 0

or a new non-zero address that is distinct from all previous addresses) and free.

• Modify tigen so that it uses computed alias information. CIL comes with John Kodu mal’s implementation of Manuvir Das’ One-Level Flow alias analysis to aid in reasoning

about pointers, but it is not currently used in this project. As a hint, alias analysis in formation leads directly to “distinctness” constraints. This would be a relatively short

change, so you should also do something else and/or provide compelling examples to

show that the alias analysis really helps.

• Modify tigen so that its performance and scalability are non-trivially improved. This

typically requires more “engineering” than “theory”, but getting an analysis to run

on millions of lines of code (e.g., the Linux kernel, SQL Server) is very difficult. Your

modified version should run significantly faster on large benchmarks of your choosing.

3

• Modify or post-process tigen so that the performance of its generated test inputs is

non-trivially improved. That is, perform test suite selection or test suite reduction or

even time-aware test suite prioritization or a similar improvement. Ideally we would

like the smallest number of test cases that require the smallest amount of wall-clock

time to execute but still covert the greatest fraction of the subject programs. This is

a reasonable project if you are more interested in CS theory than in systems hackery.

• Modify tigen to handle record data types (e.g., structures and/or unions).

• Modify tigen to handle floating-point data types. In practice, this ends up being insuffi-

cient for full credit for most students, as a direct implementation of Z3’s Real datatype

(especially without considering the differences between real numbers in mathematics

and IEEE floating point numbers) may not provide enough material to demonstrate

your mastery of course concepts. Think carefully before you select this option.

• Modify tigen to accept additional constraints provided by the user (e.g., pre- and post conditions on the subject program, an external constraint language that you parse at

the beginning, or whatever you like). For example, you may want to specify that you’re

only interested in test inputs involving negative numbers. Part of a larger project might

be to have tigen output multiple diverse test inputs that cover the same path.

• Modify tigen to be context-sensitive. You might compute the call graph and analyze the

functions in reverse dependency order. You might do a full-blown CFL reachability

analysis. Or you might just start in the target function and take very long paths

through the entire reachable program. Handling recursion is a related topic.

• Modify tigen to incorporate ideas from the popular and effective afl (see https:

//github.com/google/AFL), such as the use of a genetic algorithm.

• Modify tigen so that it implements key ideas from a well-cited or classic test input

generation tool. Examples might include Godefroid et al.’s DART project (random

test input generation), Sen et al.’s CUTE project (concolic testing), or Lakhotia et

al.’s AUSTIN project (empirical optimizations and best practices).

• Rewrite tigen so that it supports another target language with functionality compa rable to the provided baseline. Please check with the instructor before selecting this

option: it usually involves taking the provided tigen code as documentation and writ ing something entirely new. This means that more of the focus is on writing code to

process intermediate representations (rather than implementing a research idea), and

thus more coding work may be required. However, it may be appealing to students

working on a new language. For example, if you are involved in Cyrus Omar’s Hazel

language project, writing a test input generator for Hazel that can be incorporated into

that project going forward may feel more impactful than writing a “one-off” tool that

helps with learning for a class but is not used later.

4

Exercise 6C. Coding. Submit your modified tigen.ml file. In addition, submit two new

subject programs in the style of the subject programs already included. Your homework

should perform well on those new subject programs.

Exercise 6F-1. Bookkeeping [2 points].

1. Clearly indicate whether this is partner work (and make sure both names are clearly

indicated) or solo work.

2. How did this assignment go? What were the high points and the low points? We’re

interested in hearing your opinions, and this is also an opportunity to speak directly

about any meta-level concerns that arose during this assignment. For example, if you

ran out of time, you might feel more comfortable mentioning that here than in the

formal section of the report.

Exercise 6F-2. Report [22 points]. Provide a multi-paragraph report describing your

changes (as above) as well as any other compelling figures or charts relevant to supporting

your case.

Recall that you should demonstrate that you did something useful with respect to this

homework’s goals of using program analysis techniques either (1) in your research or (2) to

understand programs or (3) to find bugs or (4) to verify properties of programs or (5) to

make related tools more usable.

Exercise 6F-3. Research Communication [4 points]. Compose a brief (one- or two paragraph) email to one of the authors of the tools or papers you used in this homework

and include the text of it in your submission. In addition, indicate whether you are willing

to use your name or whether you would like to be portrayed as an anonymous student in

my class. I will check off the fact that you wrote something and potentially forward it

along (or suggest that you do so personally). You can comment on any aspect of your

experience with their work — your comments need not be positive. For example, you might

ask Bjorner why Z3 doesn’t handle multiplication, complain to Kodumal or Das that OLF

isn’t precise enough for C programs, or tell Necula or McPeak that you find CIL’s memory

lvalue semantics unintuitive. You might write to Lakhotia and ask him how he managed to

scale to large programs given all the difficulties you observed when wrestling with C. If you

do offer criticism, strive to make it constructive by commenting on what you would have

liked to have seen instead or how you might like to see things improved if the time were

available. If you absolutely cannot think of anything to say, thank them for making their

tools available and let them know that you used them with success. Even minor comments

about documentation or a fresh-eyed perspective on usability can be helpful.

The purpose of this non-standard exercise is two-fold.

• First, I have observed multiple instances in this class of a student being unwilling to

contact the author of some publicly-available project. While I realize that you don’t

5

want to be known as a whiny grad student who didn’t bother to read the manual (or

some other misconception), it’s also not worth wasting your time to try to decipher a

research prototype when the author is only an email away. I think it would legitimately

be good practice for many students to correspond with an arbitrary researcher. You

may not get a response, but the sky won’t fall. (In addition, I know the people involved

in all of this software and they are all quite friendly.)

• Second, internships are not the only way to build up contacts and networks. It is en tirely reasonable to grow a friendship or collaboration with someone over time, starting

with a lowly email about research, moving on to chatting a conferences, and eventually

working together on new research. You’re rarely certain of exactly where you will end

up or what you will be working on, so it behooves you to know as many people out

there as possible.

• Third, many software systems papers (especially in programming languages, software

engineering, or operating systems) benefit from conducting a direct empirical compar ison to a previous project. This often involves locating, compiling and running the

source code from that previous project. Despite the rise of containerization, virtual

machines, paper artifact badges, and the like, getting the code from a prior paper to

run often requires communicating with the prior authors.

Exercise 6F-4. Guided Notes Feedback [2 points]. This semester we ran a pilot

program of providing guided notes. Many students report that Graduate Programming Lan guages can be demanding in terms of the number of new things to keep track of (e.g.,

new typography and vocabulary, formal mathematical and logical reasoning, etc.). Peda gogy studies suggest that guided notes can reduce cognitive overhead and support study

skills (e.g., see teaching-tip-of-the-week/engaging-students-with-guided-notes.html), but their use

may not be as clear in this graduate-level setting as opposed to an undergraduate context.

Write one positive sentence about the guided notes and write one sentence with a suggestion

for improvement. (1 point for positive sentence, 1 point for negative sentence.) The content

of your answer does not influence your grade in any way: this is feedback to help improve

future semesters.

Submission. Turn in the formal component of the assignment as a single PDF document

via the gradescope website. Your name and Michigan email address must appear on the

first page of your PDF submission but may not appear anywhere else. Turn in the coding

component of the assignment via the autograder.io website.

6