Constraint-Based Search in Software Synthesis

lecture 8 n.w
1 / 65
Embed
Share

Explore the inductive synthesis problem, overall strategy sketch, building constraints, semantics of a simple programming language, handling loops, and symbolic evaluation of commands within the context of constraint-based search. Learn about symbolic execution, simplification, encoding, and solving techniques in software synthesis.

  • Software Synthesis
  • Constraint-Based Search
  • Symbolic Execution
  • Programming Language
  • Constraints
rayaanacharya
ypont Follow

Uploaded on | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

Download Presentation

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript

  1. Lecture 8 Constraint-based search Continued Armando Solar-Lezama

  2. The inductive synthesis problem ? ?? ? ?(??,?) where E = {x1, x2, , xk} 2

  3. Overall Strategy Sketch with harnesses Symbolic Execution Simplification Encoding Solver

  4. Building Constraints Program sketching Armando Solar-Lezama, International Journal on Software Tools for Technology Transfer October 2013, Volume 15, Issue 5-6, pp 475-495

  5. Semantics of a simple language e:= n | x | e1 + e2 | e1 > e2 c:= x := e | c1 ; c2 | if e then c1 else c2 | while e do c What does an expression mean? An expression reads the state and produces a value The state is modeled as a map ? from vars to values ? ? ??? Ex: ? ? = ??.?(?) ? ? = ??.? ? ?1+ ?2 = ??.? ?1? + ? ?2? ? ?1> ?2 = ??.?? ? ?1? > ? ?2? ? ?? 1 ???? 0

  6. Semantics of a simple language e:= n | x | e1 + e2 c:= x := e | c1 ; c2 | if e then c1 else c2 | while e do c What does a command mean? A command modifies the state ? ? Ex: ? ? ? = ??.?[? (? ? ?)] ? ?1;?2 = ??.? ?2 (? ?1 ?) ? ?? ? ? ?? ?1???? ?2 = ??.??.??? ? ? = 1 ? ?? ? ?1 ? ? ???? ? ?2 ? ?

  7. What about loops? Semantics of a while loop Let ? = ? ? ??? ? ?? ? ? satisfies the following equation: ? = ??.??.??? ? ? ?? ? ? ? ? ? ???? ?? Equation can have many solutions when loop doesn t terminate Rich theory for finding least fixed point solution We ll settle for a simpler strategy: unroll k times and then give up

  8. Symbolic execution of sketches Very similar to what we just saw But values are now parameterized by ? The denotation function will keep track of contexts

  9. Symbolic Evaluation of Commands Commands have two roles Modify the symbolic state Generate constraints Constraints represent sets of valid ? functions

  10. Symbolic Evaluation of Commands Assignments and Assertion

  11. Symbolic Evaluation of Commands If statement

  12. Conditionals Initial set of viable ? if e else C2 then C1

  13. Conditionals Subset such that ? ?? = 1 if e Subset such that ? ?? = 0 else C2 then C1

  14. Conditionals if e else C2 then C1 Subset that also passes all the assertions in C2

  15. Conditionals if e else C2 then C1 U Result of conditional

  16. Symbolic Evaluation of Commands While loops

  17. A sketch as a constraint system x > (??1) x+1 > (??1) int lin(int x){ if(x > (??1)) return (??2)*x + (??3); else return (??4)*x; } (??2)*x + (??3) (??2)*(x+1) + (??3) void main(int x){ int t1 = lin(x); int t2 = lin(x+1); if(x<4) assert t1 >= x*x; if(x>=3) assert t2-t1 == 1; } (??4)*(x+1) (??4)*x mux mux 1 x>=4 - x<3 x*x = >= or or and 17

  18. int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } 18

  19. x int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } 19

  20. x >> & int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } 20

  21. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } 21

  22. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x 22

  23. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & 23

  24. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + 24

  25. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + mux x 25

  26. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + mux x >> & 26

  27. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + mux x >> & & + 27

  28. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + mux x >> & & + mux x 28

  29. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + mux x >> & & + mux x 29

  30. x >> & & + int popSketched (bit[W] x) implements pop { repeat(??) { x = (x & ??) + ((x >> ??) & ??); } return x; } mux x >> & & + mux x >> & & + mux S(x,?) = x 30

  31. Simplification

  32. Structural Hashing h0 h1 h2 + + * * a b

  33. Structural Hashing h0 h1 h2 h0 h1 h2 + + + * * * * a b a b

  34. Structural Hashing h0 h1 h2 h0 h1 h2 h0 h1 h2 + + + + * * * * * a b a b a b

  35. Structural hashing + rewriting b a h0 + + 0 < < < ^ ^

  36. Structural hashing + rewriting b a h0 ? + ? < ? ? < 0 + + 0 < < < ^ ^

  37. Structural hashing + rewriting a h0 ? + ? < ? ? < 0 + 0 < < < ^ ^

  38. Structural hashing + rewriting a h0 ? + ? < ? ? < 0 + 0 < < < ^ ^

  39. Structural hashing + rewriting a h0 ? + ? < ? ? < 0 + 0 < < ^ ^

  40. Structural hashing + rewriting a h0 ? + ? < ? ? < 0 + ? ? ? 0 < < ^ ^

  41. Structural hashing + rewriting a h0 ? + ? < ? ? < 0 + ? ? ? 0 < < ^

  42. Structural hashing + rewriting a h0 ? + ? < ? ? < 0 + ? ? ? 0 < < ^

  43. Structural hashing + rewriting h0 0 ? + ? < ? ? < 0 ? ? ? < < ^

  44. Structural hashing + rewriting h0 0 ? + ? < ? ? < 0 ? ? ? < < ^

  45. Structural hashing + rewriting 0 h0 ? + ? < ? ? < 0 ? ? ? < ^

  46. Structural hashing + rewriting 0 h0 ? + ? < ? ? < 0 ? ? ? < ^

  47. Structural hashing + rewriting 0 h0 ? + ? < ? ? < 0 ? ? ? <

  48. Constraints to SAT SAT Solver only understands CNF Sum (OR) of variables and their negation Equivalent to ? ??? ?? h0 h1 h2 xor Assert

  49. Constraints to SAT SAT Solver only understands CNF Sum (OR) of variables and their negation Equivalent to ? ??? ?? h0 h1 h2 ?1 xor ?2 Assert

  50. Constraints to SAT SAT Solver only understands CNF Sum (OR) of variables and their negation Equivalent to ? ??? ?? 0 1 ?1 ?1 0 ?1 1 h0 h1 h2 ?1 xor ?2 Assert

Related


No related presentations.

More Related Content