15-414 HW 7 1Instructor: Edmund M. Clarke Teaching Assistant: Michael Carl TschantzHomework Author: Arie GurfinkelAssignment 71 Using CBMCFor this problem we will use the CBMC program analysis tool. You can run it simply by thefollowing command:/afs/andrew.cmu.edu/usr24/mtschant/15414-f07/cbmc --unwind 5 --function foo program.cFor this problem, you will use the following C functions:/** GLOBALS */int buf[4];int hi = 0;int lo = 0;int size = 4;/** FUNCTION enqueue */void enqueue (int x){buf [hi] = x;hi = (hi + 1);}/** FUNCTION dequeue */int dequeue (){int res = buf [lo];lo = (lo + 1);return res;}/** FUNCTION queue_test */void queue_test (void){while (nondet_int ()){if (nondet_int ()){int x = nondet_int ();enqueue (x);}elsedequeue ();}115-414 HW 7 2}/** FUNCTION BINSEARCH */int binsearch (int x){int a[16];signed low = 0, high = 16;while (low < high){signed middle = low + ((high - low) >> 1);if (a[middle]<x)high = middle;else if (a [middle] > x)low = middle + 1;else /* a [middle] == x ! */return middle;}return -1;}(a) Use CBMC to show that the function queuetest can cause a buffer overflow. Show theexecution that causes an overflow. What was the smallest unwindin g bou nd requiredfor finding this counterexample? (Hint: you will want to disable unwinding assertionswith --no-unwinding-assertions for this example).(b) Fix the buffer overflows in the previous example. Use CBMC to verify that there is nooverflow after the loop is unrolled 40 times. Can this result be used to conclude thatthe program has no buffer overflows?(c) Use CBMC to check whether the function binsearch accesses the array a outside ofits bounds in 5 steps or less (i.e., use unwind bound of 5). What can we learn from theresult? Is the function safe, unsafe, or nothing is known?(d) Repeat part (c) with unwinding boun d of 10. What can you conclude from the result?2 From Programs to ConstraintsFor this problem, you will need to convert a program into a set of constraints. The constraintsshould be such that every satisfying assignment corresponds to an execution of the program thatviolates an assertion. The program is given below:void main (void){int i;char * buf;215-414 HW 7 3char last;if (buf [i] == ’\0’){int start = 0;while (start < i){buf [start] = ’f’;start++;last = buf [start - 1];}}}(a) Show the resu lt of unrolling the loop twice (2) and adding an unwinding assertion.(b) Convert the loop-free program (with assertion) from part (a) into Single Static Assign-ment (SSA) form.(c) Generate a constraint system C from the SSA p rogram in part (a) such that C issatisfiable if and only if the unwinding assertion can be violated.(d) Is the constraint system C from part (c) satisfiable? If yes, show a satisfying assignment.3 Checking Custom PropertiesLocks are commonly used to grant exclusive access to resources. Assume that we h ave a lockingAPI consisting of two functions: lock, and unlock. The function lock acquires a lock, and thefunction unlock releases it. Furthermore, a proper use of the API must conform to a lockingdiscipline: a lo ck cannot be acquired (releas ed ) twice in a row without a corresponding unlock(lock) in between. For example, a sequence of callslock (); unlock (); lock (); unlock ();is legal, and th e sequencelock (); lock (); unlock (); unlock ();is not.In this problem you will need to use CBMC to ch eck whether the follow ing two functions conformto the locking discipline or not./** prototypes */int nondet_int ();void lock (void);void unlock (void);int read_input (void) { return nondet_int (); }/** FUNCTION LOCK1 */315-414 HW 7 4void lock1 (void){int in_irq;int buf[10];int i;if (in_irq) lock ();for (i = 0; i < 5; i++)buf [i] = read_input ();if (in_irq) lock ();}/** FUNCTION LOCK2 */void lock2 (void){int request, old, total;request = 0;do {lock ();old = total;request = read_input ();if (request){unlock ();total = total + 1;}} while (total != old);unlock ();}(a) Instrument the two fun ctions above with asserts to check that a lock is never acquiredor released twice in a row .(b) Use CBMC to check whether th e function lock1 satisfies the locking discipline. Is thefunction correct? If not, show an erroneous execution.(c) Use CBMC to check whether the function lock2 incorrectly acquires or releases a locktwice in a row within 20 executions of the loop. What can you conclude from the resultof the analysis? Can the program be considered safe? Will increasing th e unwindingbound be useful?(d) Use CBMC to check that if the lock is n ot held before execution of the body of theloop in lock2, then the lock is held after execution of the body of the loop if and onlyif total == old. Does the result indicate that the program is correct or not? Explainyour