5 Motivation for SMT solvers, and combination of decision procedures (Презентации лекций), страница 2
Описание файла
Файл "5 Motivation for SMT solvers, and combination of decision procedures" внутри архива находится в папке "Презентации лекций". PDF-файл из архива "Презентации лекций", который расположен в категории "". Всё это находится в предмете "boolean sat-smt solvers for software engineering" из 11 семестр (3 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
/ Trento / 2005 - presentGanesh / Stanford & MIT / 2005 - presentSeshia / CMU & Berkeley / 2004 - presentCombinationsVijay GaneshWednesday, 16 January, 1318Talk OutlineTopics covered in Lecture 1Motivation for SAT/SMT solvers in software engineering• Software engineering (SE) problems reduced to logic problems• Automation, engineering, usability of SE tools through solversHigh-level description of the SAT/SMT problem & logics• Rich logics close to program semantics• Demonstrably easy to solve in many practical casesModern SAT solver architecture & techniques• DPLL search, shortcomings• Modern CDCL SAT solver: propagate (BCP), decide (VSIDS), conflict analysis, clause learn, backJump,• Termination, correctness• Big lesson: learning from mistakesTopics covered in Lecture 2Modern SMT solver architecture & techniques• Rich logics closer to program semantics• DPLL(T), Combinations of solvers, Over/under approximations• My own contributions: STP & HAMPI• STP: Abstraction-refinement for solving• Applications to dynamic symbolic testing (aka concolic testing)• HAMPI: Bounded logics• SAT/SMT-based applications• Future of SAT/SMT solversVijay GaneshWednesday, 16 January, 1319STP Bit-vector & Array SolverProgramExpressionsSATSTP Solver(x = z+2 ORmem[i] + y <= 01)UNSAT• Bit-vector or machine arithmetic• Arrays for memory• C/C++/Java expressions• NP-completeVijay GaneshWednesday, 16 January, 1320The History of STP• Solver-based languages (Alloy team)1,000,000 Constraints• Solver-based debuggers• Solver-based type systems• Solver-based concurrency bugfinding• HAMPI: String Solvers• Ardilla by Ernst et al.• Kudzu & Kaluza by Song et al.• Klee by Engler et al.• George Candea’s Cloud 9 tester• STP + HAMPI exceed 100+ projects• STP• Enabled Concolic Testing• EXE by Engler et al• BAP/BitBlaze by Song et al.• Model checking by Dill et al.100,000 Constraints2005Vijay GaneshWednesday, 16 January, 132009Today21Programs Reasoning & STPWhy Bit-vectors and Arrays• STP logic tailored for software reliability applications• Support symbolic execution/program analysisC/C++/Java/...Bit-vectors and ArraysInt VarChar Var32 bit variable8 bit variableArithmetic operation(x+y, x-y, x*y, x/y,...)Arithmetic function(x+y,x-y,x*y,x/y,...)assignmentsx = expr;equalityx = expr;if conditionalif(cond) x = expr1 else x = expr2if-then-else constructx = if(cond) expr1 else expr2inequalityinequality predicateMemory read/writex = *ptr + i;Array read/writeptr[]; x = Read(ptr,i);Structure/ClassSerialized bit-vector expressionsFunctionSymbolic executionLoopsBoundingVijay GaneshWednesday, 16 January, 1322How to Automatically Crash Programs?Concolic Execution & STPProblem: Automatically generate crashing tests given only the codeProgramSymbolic ExecutionEnginewithImplicit SpecAutomatic TesterFormulasSTPSAT/UNSATCrashing TestsVijay GaneshWednesday, 16 January, 1323How to Automate Testing?Concolic Execution & STPStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1.
Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}• Formula captures computation• Tester attaches formula to capture specVijay GaneshWednesday, 16 January, 1324How to Automate Testing?Concolic Execution & STPStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1.
Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}Equivalent Logic Formula derived usingsymbolic executiondata_field, mem_ptr : ARRAY;len_field : BITVECTOR(32); //symbolici, j, ptr : BITVECTOR(32);//symbolic..mem_ptr[ptr+i] = process_data(data_field[i]);mem_ptr[ptr+i+1] = process_data(data_field[i+1]);..• Formula captures computation• Tester attaches formula to capture specVijay GaneshWednesday, 16 January, 1324How to Automate Testing?Concolic Execution & STPStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1. Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}Equivalent Logic Formula derived usingsymbolic executiondata_field, mem_ptr : ARRAY;len_field : BITVECTOR(32); //symbolici, j, ptr : BITVECTOR(32);//symbolic..mem_ptr[ptr+i] = process_data(data_field[i]);mem_ptr[ptr+i+1] = process_data(data_field[i+1]);..• Formula captures computation• Tester attaches formula to capture specVijay GaneshWednesday, 16 January, 1324How to Automate Testing?Concolic Execution & STPStructured input processing code:PDF Reader, Movie Player,...Buggy_C_Program(int* data_field, int len_field) {int * ptr = malloc(len_field*sizeof(int));int i; //uninitialized}while (i++ < process(len_field)) {//1.
Integer overflow causing NULL deref//2. Buffer overflow*(ptr+i) = process_data(*(data_field+i));}Equivalent Logic Formula derived usingsymbolic executiondata_field, mem_ptr : ARRAY;len_field : BITVECTOR(32); //symbolici, j, ptr : BITVECTOR(32);//symbolic..mem_ptr[ptr+i] = process_data(data_field[i]);mem_ptr[ptr+i+1] = process_data(data_field[i+1]);..//INTEGER OVERFLOW QUERY0 <= j <= process(len_field);ptr + i + j = 0?• Formula captures computation• Tester attaches formula to capture specVijay GaneshWednesday, 16 January, 1324How STP WorksBird’s Eye View: Translate to SATSTPBit-vector&Array Formula(x = z+2 ORmem[i] + y <= 01)...TranslateToSATBooleanSAT SolverSATUNSATWhy Translate to SAT?• Both theories NP-complete• Non SAT approaches didn’t work• Translation to SAT leverages solid engineeringVijay GaneshWednesday, 16 January, 1325How STP WorksRich Theories cause MEM Blow-upSTPBit-vector&Array Formula(x = z+2 ORmem[i] + y <= 01)...TranslateFormulaToGrowthSATBooleanSAT SolverSATUNSAT• Making information explicit• Space cost• Time costVijay GaneshWednesday, 16 January, 1326Explicit Information causes Blow-upArray Memory Read ProblemLogic Formula derived usingsymbolic executiondata_field, mem_ptr : ARRAY;len_field : BITVECTOR(32); //symbolici, j, ptr : BITVECTOR(32);//symbolic..mem_ptr[ptr+i] = process_data(data_field[i]);mem_ptr[ptr+i+1] = process_data(data_field[i+1]);..if(ptr+i = ptr+j) then mem_ptr[ptr+i] = mem_ptr[ptr+j);//INTEGER OVERFLOW QUERY0 <= j <= process(len_field);ptr + i + j < ptr?• Array Aliasing is implicit• Need to make information explicit during solving• Cannot be avoidedVijay GaneshWednesday, 16 January, 1327How STP WorksArray-read MEM Blow-up Problem• Problem: O(n2) axioms added, n is number of read indices• Lethal, if n is large, say, n = 100,000; # of axioms is 10 BillionFormula Growthv0 = expr0v1 = expr1Read(Mem,i0) = expr0Read(Mem,i1) = expr1Read(Mem,i2) = expr2...Read(Mem,in) = exprn...vn = exprn(i0 = i1) => (v0 = v1)(i0 = i2) => (v0 = v2)...(i1 = i2) => (v1 = v2)...Vijay GaneshWednesday, 16 January, 1328How STP WorksThe Array-read Solution• Key Observation• Most indices don’t alias in practice• Exploit locality of memory access in typical programs• Need only a fraction of array axioms for equivalenceRead(Mem,i0) = expr0Read(Mem,i1) = expr1Read(Mem,i2) = expr2...Read(Mem,in) = exprnVijay GaneshWednesday, 16 January, 13v0 = expr0v1 = expr1...vn = exprn(i0 = i1) => (v0 = v1)29STP Key Conceptual ContributionAbstraction-refinement PrincipleInput FormulaAbstraction StepAbstractedFormulaRefinementBoolean SAT SolverCheck AnswerVijay GaneshWednesday, 16 January, 13CorrectAnswer30How STP WorksWhat to Abstract & How to Refine?AbstractionRefinement1.
Less essential parts2. Causes MEM blow-up1. Guided2. Must rememberAbstraction managesformula growth hardnessRefinement managessearch-space hardnessVijay GaneshWednesday, 16 January, 1331How STP WorksAbstraction-refinement for Array-readsInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)SubstitutionsSimplificationsLinear SolvingArray AbstractionRefinement LoopConversion to SATBoolean SAT SolverResultVijay GaneshWednesday, 16 January, 1332How STP WorksAbstraction-refinement for Array-readsSubstitutionsRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000’(i0,i1)SimplificationsLinear SolvingArray Abstractioni0 = i1Refinement LoopConversion to SATBoolean SAT SolverResultVijay GaneshWednesday, 16 January, 1333How STP WorksAbstraction-refinement for Array-readsAbstracted InputArray Axioms DroppedInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)v0=0v1=1…vn=10,000’ (i0,i1)Refinement LoopSubstitutionsSimplificationsLinear SolvingArray AbstractionConversion to SATBoolean SAT SolverResultVijay GaneshWednesday, 16 January, 1334How STP WorksAbstraction-refinement for Array-readsAbstracted InputArray Axioms DroppedInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)v0=0v1=1…vn=10,000’ (i0,i1)Vijay GaneshWednesday, 16 January, 13SimplificationsLinear SolvingArray AbstractionRefinement LoopInputFormula falseinAssignmentSubstitutionsi0=0,i1=0v0=0, v1=1…Conversion to SATBoolean SAT SolverResult35How STP WorksAbstraction-refinement for Array-readsAbstracted InputArray Axioms DroppedInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)v0=0v1=1…vn=10,000’ (i0,i1)Refinement LoopVijay GaneshWednesday, 16 January, 13SimplificationsLinear SolvingArray Abstraction(i0=i1)!v0=v1Add Axiom thatis FalsifiedSubstitutionsi0=0,i1=0v0=0, v1=1…Conversion to SATBoolean SAT SolverResult36How STP WorksAbstraction-refinement for Array-readsInputRead(A,i0)=0Read(A,i1)=1…Read(A,in)=10,000(i0,i1)SubstitutionsSimplificationsLinear SolvingArray AbstractionRefinement LoopConversion to SATBoolean SAT SolverUNSATVijay GaneshWednesday, 16 January, 1337STP vs.