15-213, Spring 2008Lab Assignment L1: Manipulating BitsAssigned: Jan. 15, Due: Wed., Jan. 30, 11:59PMRandy Bryant ([email protected]) is the lead person for this assignment.1 IntroductionThe purpose of this assignment is to become more familiar with bit-level representations of common pat-terns, integers, and floating-point numbers. You’ll do this by solving a series of programming “puzzles.”Many of these puzzles are quite artificial, but you’ll find yourself thinking much more about bits in workingyour way through them.1.1 LogisticsThis is an individual project. All handins are electronic. Clarifications and corrections will be posted on theAutolab message board.1.2 Creating your Autolab AccountAll 15-213 labs are being offered this term through a Web service developed by Prof. David O’Hallaroncalled Autolab. Before you can download your lab materials, you will need to create your Autolab account.Point your browser at the Autolab front pagehttp://autolab.cs.cmu.eduand select the “15213-s08” link. Apache will prompt you for a user name and password. Enter your Andrewlogin ID, leave the password field blank, and press “OK”. If you are on Autolab’s list of registered students,you will be directed to the Autolab “Create” page, where you will be asked to enter a password, nickname,and email address. After you enter this information, Apache will prompt you again for your user name andpassword. This time, enter your Andrew login ID and the password you just registered with Autolab, andthen press “OK”. You will be sent to the main Autolab page for this course, which you should bookmark forfuture use.A couple of important notes on creating your account:1• Autolab passwords are encrypted on the network and the server, so you can safely use your Andrewpassword as your Autolab password if you don’t want to have remember another password.• After you have created your account, you can change your password, nickname, and email addressanytime by visiting the Autolab “Update” page.• If you added the class late, you might not be included in Autolab’s list of valid students, and thus won’tbe redirected to the Autolab “Create” page. If this happens, just send email to [email protected] an Autolab account, and someone will add you to the list.1.3 Obtaining your Lab MaterialsYour lab materials are contained in a Unix tar file called datalab-handout.tar, which you can down-load from Autolab. After logging in to Autolab through the front pagehttp://autolab.cs.cmu.eduyou can retrieve the datalab-handout.tar file by selecting “Download lab materials” and then hittingthe “Go” button.Start by copying datalab-handout.tar to a (protected) directory in which you plan to do your work.Then give the command “tar xvf datalab-handout.tar”. This will create a directory calleddatalab-handout that contains a number of files. The only file you will be modifying and handingin is bits.c.WARNING: Do not let the Windows WinZip program open up your .tar file (many web browsers are setto do this automatically). Instead, save the file to your AFS directory and use the Linux tar program toextract the files.The file btest.c contains code that performs a simple, non-exhaustive check of the functional correctnessof your code. The file README contains additional documentation about BTEST. Use the command maketo generate the test code and run it with the command ./btest.The included program DLC can be used to check your solutions for compliance with the coding rules. Theincluded programs ISHOW and FSHOW can be used to help examine the bit representations of integer andfloating point numbers.The files in the subdirectory bddcheck implement the BDD checker, a tool that formally verifies yourcode. The remaining files are used to build the program BTEST.The bits.c file contains a skeleton for each of the 15 programming puzzles. Your assignment is to com-plete each function skeleton according to a strict set of programming rules, intended to help you understandhow values are represented at the bit-level and how to manipulate bit patterns using standard C operations.2 EvaluationYour code will be compiled with GCC and exhaustively tested with the BDD checker. Your score will becomputed out of a maximum of 75 points based on the following distribution:240 Correctness of code.30 Performance of code, based on number of operators used in each function.5 Style points, based on your instructor’s subjective evaluation of the quality of your solutions and yourcomments.The 15 puzzles you must solve have been given a difficulty rating between 1 and 4, such that their weightedsum totals to 40.The code in BTEST simply tests your functions for a number of different cases. For most functions, the num-ber of possible argument combinations far exceeds what could be tested exhaustively. To provide completecoverage, we have created an experimental formal verification program, CBIT that, in effect, tests your func-tions for all possible combinations of arguments. It does this by viewing each bit of the function result asa Boolean function of the bits comprising the function arguments. It uses a data structure known as BinaryDecision Diagrams (BDDs) (R. E. Bryant, IEEE Transactions on Computers, August, 1986) to representthese Boolean functions in a way that the program can efficiently compare the results of your functions withthose of a set of reference solutions. If the bit-level functions match, then the two C functions computeidentical results. Otherwise, CBIT can generate a counterexample, i.e., a set of function arguments whereyour function will produce a different result than the reference solution.You do not invoke CBIT directly. Instead, there is a series of Perl scripts that set up and evaluate the calls toit. Executeunix> ./bddcheck/check.pl -f funto check function fun. Executeunix> ./bddcheck/check.plto check all of your functions.Note: The Perl scripts are a bit picky about the formatting of your code. They expect the function to openwith a line of the form:int fun (...)orunsigned fun (...)and to end with a single right brace in the leftmost column. That should be the only right brace in theleftmost column of your function.You will get full credit for a puzzle if the BDD checker determines that your solution is correct, and nocredit otherwise. The formal verification provided by the BDD checker will show you that there are no bugslurking in your code. You’ll
View Full Document
Unlocking...