15 213 Spring 2008 Lab Assignment L1 Manipulating Bits Assigned Jan 15 Due Wed Jan 30 11 59PM Randy Bryant Randy Bryant cs cmu edu is the lead person for this assignment 1 Introduction The purpose of this assignment is to become more familiar with bit level representations of common patterns 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 working your way through them 1 1 Logistics This is an individual project All handins are electronic Clarifications and corrections will be posted on the Autolab message board 1 2 Creating your Autolab Account All 15 213 labs are being offered this term through a Web service developed by Prof David O Hallaron called Autolab Before you can download your lab materials you will need to create your Autolab account Point your browser at the Autolab front page http autolab cs cmu edu and select the 15213 s08 link Apache will prompt you for a user name and password Enter your Andrew login 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 and password This time enter your Andrew login ID and the password you just registered with Autolab and then press OK You will be sent to the main Autolab page for this course which you should bookmark for future 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 Andrew password 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 address anytime 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 t be redirected to the Autolab Create page If this happens just send email to 15 213 staff cs cmu edu requesting an Autolab account and someone will add you to the list 1 3 Obtaining your Lab Materials Your lab materials are contained in a Unix tar file called datalab handout tar which you can download from Autolab After logging in to Autolab through the front page http autolab cs cmu edu you can retrieve the datalab handout tar file by selecting Download lab materials and then hitting the 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 called datalab handout that contains a number of files The only file you will be modifying and handing in is bits c WARNING Do not let the Windows WinZip program open up your tar file many web browsers are set to do this automatically Instead save the file to your AFS directory and use the Linux tar program to extract the files The file btest c contains code that performs a simple non exhaustive check of the functional correctness of your code The file README contains additional documentation about BTEST Use the command make to 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 The included programs ISHOW and FSHOW can be used to help examine the bit representations of integer and floating point numbers The files in the subdirectory bddcheck implement the BDD checker a tool that formally verifies your code 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 complete each function skeleton according to a strict set of programming rules intended to help you understand how values are represented at the bit level and how to manipulate bit patterns using standard C operations 2 Evaluation Your code will be compiled with GCC and exhaustively tested with the BDD checker Your score will be computed out of a maximum of 75 points based on the following distribution 2 40 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 your comments The 15 puzzles you must solve have been given a difficulty rating between 1 and 4 such that their weighted sum totals to 40 The code in BTEST simply tests your functions for a number of different cases For most functions the number of possible argument combinations far exceeds what could be tested exhaustively To provide complete coverage we have created an experimental formal verification program CBIT that in effect tests your functions for all possible combinations of arguments It does this by viewing each bit of the function result as a Boolean function of the bits comprising the function arguments It uses a data structure known as Binary Decision Diagrams BDDs R E Bryant IEEE Transactions on Computers August 1986 to represent these Boolean functions in a way that the program can efficiently compare the results of your functions with those of a set of reference solutions If the bit level functions match then the two C functions compute identical results Otherwise CBIT can generate a counterexample i e a set of function arguments where your function will produce a different result than the reference solution You do not invoke it Execute CBIT directly Instead there is a series of Perl scripts that set up and evaluate the calls to unix bddcheck check pl f fun to check function fun Execute unix bddcheck check pl to check all of your functions Note The Perl scripts are a bit picky about the formatting of your code They expect the function to open with a line of the form int fun or unsigned fun and to end with a single right brace in the leftmost column That should be the only right brace in the leftmost column of your function You will get full credit for a puzzle if the BDD checker determines that your solution is correct and no credit otherwise The formal verification provided by the BDD checker will show you that there are no bugs lurking in your code You ll find yourself wishing you could do this kind of testing with every program you 3 write Unfortunately BDDs can handle only relatively simple functions such as the
View Full Document
Unlocking...