Refinement	  Type	  Inference	  via	  Horn	  Constraint	  Optimization
Kodai	  Hashimoto and	  Hiroshi	  Unno
(University	  of	  Tsukuba,	  Japan)Our	  Goal:	  Path-­‐Sensitive	  Program	  Analysis	  of	  Higher-­‐order	  Non-­‐det.	  Functional	  Programs• Precondition	  inference • Non-­‐termination	  analysis• Bug	  finding• (Conditional)	  termination	  analysis• Modular	  verification•…

Refinement	  type	  optimization
2015/9/10

a	  generalization	  of	  ordinary	  refinement	  type	  inferenceSAS	  20152

Refinement	  Type	  Inference
Programlet	  rec	  sum	  x	  =…

InferRefinement	  Typessum	  :	   𝑥: int → 𝑦	   	  𝑦 ≥ 0},…

Refinement	  types	  can	  precisely express	  program	  behaviors• {𝑥 ∶ int	  |	  𝑥 ≥ 0}	   FOL	  predicates	  (e.g.,	  QFLIA)
Non-­‐negative	  integers• (𝑥	  :	  int) → {𝑦	  :	  int ∣ 𝒚 ≥ 𝒙}
Functions	  that	   take	  an	  integer	  𝑥 and	   return	  an	  integer	  𝑦 not	   less	   than	   𝑥2015/9/10

SAS	  2015

3

A	  Challenge	  in	  Refinement	  Type	  Inference
Which	  refinement	  type	  should	  be	  inferred?
let	 rec sum	 x	 =	 if x	 =	 0	 then 0	 else x +	 sum	 (x-1)
contradiction𝑥 𝑥 < 0 → {𝑦 ∣	  ⊥}<∶

int → {𝑦 ∣ 𝑦 ≥ 0}<∶𝑥 𝑥 = −1 → {𝑦 ∣	  ⊥}incomparable
𝑥 𝑥 < −5 → {𝑦 ∣	  ⊥}𝑥 𝑥 = 0 → {𝑦 ∣ 𝑦 = 0}…

The	  most	  general	  types	  are	  often	  not	  expressible	  in	  the	  underlying	  logic	  (e.g.,	  QFLIA)

2015/9/10

SAS	  20154

Existing	  Refinement	  Type	  Inference Tools
Infer	  refinement	  types	  precise	  enoughto	  verify	  a	  given	  safety	  specification• Refinement	  Caml	  [Unno+	  ’08,	  ’09,	  ’13,	  ’15]
• Liquid	  Types	  [Jhala+	  ’08,	  ’09,	  …,	  ’15]
• MoCHi [Kobayashi+	  ’11,	  ’13,	  ’14,	  ’15,	  ’15]
• Depcegar [Terauchi	  ’10]
• HMC	  [Jhala+	  ’11]
• Popeye	  [Zhu	  &	  Jagannathan ’13]

Inferred	  types	  are	  often	  too	  specific	  to	  the	  spec.
→ Limited	  applications	  2015/9/10

SAS	  20155

Our	  Approach:	  Refinement	  Type	  Optimization
Infer	  maximally	  preferred	  (i.e. Pareto	  optimal)	  refinement	  types	  with	  respect	  to	  a	  user-­‐specified	  preference	  orderhigh…

…

𝑥 𝑥 < 0 → {𝑦 ∣	  ⊥}…
𝑥 𝑥 < −5 → {𝑦 ∣	  ⊥}

…
low2015/9/10…

…

𝑥 𝑥 = −1 → {𝑦 ∣	  ⊥}𝑥 𝑥 = 0 → {𝑦 ∣ 𝑦 = 0}…

…

int → {𝑦 ∣ 𝑦 ≥ 0}…

SAS	  2015

…

…
…
6

How	  to	  Specify	  Preference	  Orders	  (1/3)• Refinement	  type	  template
Predicate	  variables(𝑥 ∶ {𝑥 ∣ 𝑷(𝒙)}) → {𝑦 ∣ 𝑸(𝒙, 𝒚)}	  𝑃 𝑥 ↦ 𝑥 < 0	  ,	  𝑄 𝑥, 𝑦 ↦	  ⊥𝑥	   	  𝑥 < 0} → {𝑦 ∣	  ⊥}2015/9/10	  𝑃 𝑥 ↦ 𝑥 = 0	  ,	  𝑄 𝑥, 𝑦 ↦ 𝑦 = 0𝑥 𝑥 = 0 → {𝑦 ∣ 𝑦 = 0}SAS	  2015

7How	  to	  Specify	  Preference	  Orders	  (2/3)
max/min optimization	  constraints	  𝒎𝒂𝒙 𝑷 :	  infer	  a	  maximally-­‐weak predicate	  for	  𝑷
𝒎𝒊𝒏 𝑸 : infer	  a	  maximally-­‐strong predicate	  for 𝑸
Precondition

Postconditionsum	  :	  (𝑥 ∶ 	   {𝑥 ∣ 𝑷(𝒙)}) → {𝑦 ∣ 𝑸(𝒙, 𝒚)}let	 rec sum	 x	 =	 if x	 =	 0	 then 0	 else x +	 sum	 (x-1)
𝒎𝒂𝒙 𝑷
𝒎𝒊𝒏 𝑸𝑥 𝑥 < 0 → {𝑦 ∣	  ⊥}2015/9/10

int → {𝑦 ∣ 𝑦 ≥ 0}

𝑥 𝑥=0 →
SAS	  2{𝑦015 ∣ 𝑦 = 0}8How	  to	  Specify	  Preference	  Orders	  (3/3)
a	  priority	  order ⊏	  on	  predicate	  variables
𝑸 ⊏ 𝑷:	  𝑄 is	  given	  higher	  priority	  over 𝑃sum	  :	  (𝑥	  :	  {𝑥 ∣ P(𝑥)}) → {𝑦 ∣ Q(𝑥,	  y)}let	 rec sum	 x	 =	 if x	 =	 0	 then 0	 else x +	 sum	 (x-1)
𝒎𝒂𝒙 𝑷
𝒎𝒊𝒏 𝑸𝑷⊏𝑸𝑸⊏𝑷𝑥∶ 𝑥 𝑥<0
2015/9/10→ {𝑦 ∣	  ⊥}SAS	  2015𝑥 ∶ int → {𝑦 ∣ 𝑦 ≥ 0}
9Outline• Refinement	  Type	  Optimization• Applications• Our	  Type	  Optimization	  Method• Implementation	  &	  Experiments• Summary

2015/9/10

SAS	  201510

Applications	  of	  Refinement	  Type	  Optimization• Non-­‐termination	  analysis• Conditional	  termination	  analysis• Precondition	  inference• Bug	  finding• Modular	  verification•…
2015/9/10

SAS	  201511

Non-­‐Termination	  Analysis
Find	  a	  program	  input	  that	  violates	  the	  termination	  No	  return	  value =	  Non-­‐terminating
propertysum	  :	  (𝑥	  :	  {𝑥 ∣ P(𝑥)}) → {𝑦 ∣ Q(𝑥, 𝑦)} ⊥	  ⇐ 𝑸 𝒙, 𝒚let	 rec sum	 x	 =	 if x	 =	 0	 then 0	 else x +	 sum	 (x-1)

infer	  a	  maximally-­‐weak	  precondition	  𝑷Existing	  non-­‐termination	  analysis	  tool	  may	  infer:𝑥 𝑥 = −1 → {𝑦 ∣	  ⊥}𝒎𝒂𝒙 𝑷𝑥∶ 𝑥 𝒙<𝟎→ {𝑦 ∣	  ⊥}sum	  never	  terminates	  if	  𝒙 < 𝟎

2015/9/10

SAS	  201512

Non-­‐Termination	  Analysis	  ofNon-­‐Deterministic	  Programsf	  :	  (𝑥: int) → {𝑟 ∣ Q(𝑟)} ⊥	  ⇐ 𝑄 𝑟non-­‐determinism
let	 rec f x =inlet	 n: =𝒏 read_int()𝑷(𝒙, 𝒏)} =	 read_int()	 in
if n =	 x	 then f	 (x+1)	 else x

f	  never	  terminates
infer	  a	  	  	  𝒎𝒂𝒙 𝑷if	  the	  user	  always	  maximally-­‐weak	  inputs	  same	  v
alue
condition 𝑷n	  : 	  𝑛 	   	  𝒏 = 𝒙	  } as	  an	  argument	  𝒙f	  :	  (𝑥: int) → {𝑟 ∣	  ⊥ },	   …
2015/9/10

SAS	  201513

Non-­‐Termination	  Analysis	  ofHigher-­‐Order	  Programsmain	  :	  (𝑥	   :	  {𝑥 ∣ P(𝑥)}) → {𝑦 ∣ Q(𝑥, 𝑦)},	   … ⊥	  ⇐ 𝑄 𝑥, 𝑦let	 rec fix (f:int ->	 int)	 x	 =let x’=	 f	 x	 in
if x’=	 x then x else fix	 f	 x’let	 to_zero x =	 if x =	 0	 then 0	 else x - 1
let main	 x	 =	 fix	 to_zero x

infer	  a	  main	  never	  terminates	  	  	  𝒎𝒂𝒙 𝑷
maximally-­‐weak	  if	   𝒙 < 𝟎precondition	  𝑷main	  :	  (𝑥: 	  𝒙	   	  𝒙 < 𝟎	  }) → {𝑟 ∣	  ⊥ },2015/9/10

fix	  :	   𝑓: (𝑎 ∶ {𝑎 𝑎 < 0}) → {𝑏 𝑏 < 𝑎)}→ (𝑥 ∶ {𝑥 ∣ 𝑥 < 0)}) → {𝑦 ∣	  ⊥},	  to_zero	  :	  (𝑥 ∶ {𝑥 ∣ 𝑥 SAS	  <20150}) → {𝑦 ∣ 𝑦 < 𝑥}14

Applications	  of	  Refinement	  Type	  Optimization• Non-­‐termination	  analysis• Conditional	  termination	  analysis• Precondition	  inference• Bug	  finding• Modular	  verification•…
2015/9/10SAS	  201515

Conditional	  Termination	  Analysis	  (1/2)• Infer	  a	  sufficient	  condition	  for	  termination• Our	  approach	  is	  inspired	  by	  a	  program	  transformation	  approach	  to	  termination	  analysis
of	  imperative	  programs	  [Gulwani+	  ’08,	  ’09]
let	 rec sum	 x	 =	 if x	 =	 0	 then 0	 else x +	 sum	 (x-1)
the	  initialvalue	  of	  xthe	  number	  of	  recursive	  calls

let	 rec sum_t x	 i c =if x	 =	 0	 then 0	 else x	 +	 sum_t (x-1)	 i (c+1)
2015/9/10

SAS	  201516

Conditional	  Termination	  Analysis	  (2/2)
Infer	  a	  sufficient	  condition	  for	  termination≤ 𝑓 𝑖,𝑖 𝑐 ⇐∃𝑓. 𝑐 ≤ 𝑓 ∃𝑓.
𝑖 ⇐𝑐 𝐵𝑛𝑑. 	  	  𝐵𝑃𝑛𝑑𝑥 𝑖, 𝑐∧ 𝐼𝑛𝑣⇐ 𝑃 𝑥,𝑥 𝑖,∧𝑐𝐼𝑛𝑣 𝑥, 𝑖, 𝑐
sum_t:	   𝑥 ∶ 𝑥 𝑷(𝒙) → 𝑖 ∶ int → (𝑐 ∶ 𝑐 𝑰𝒏𝒗(𝒙, 𝒊, 𝒄) ) → int
let	 rec	 sum_t x	 i c	 =𝐼𝑛𝑣 𝑥, 𝑖, 𝑐
if x	 =	 0	 then 0	 else x	 +	 sum_t (x-1)	 i (c+1)⇐𝑐 =0∧𝑖 = 𝑥

𝒎𝒂𝒙 𝑷 , 𝒎𝒊𝒏 𝑩𝒏𝒅
𝑷 ⊏ 𝑩𝒏𝒅sum_t:	   𝑥 ∶ 𝑥 𝒙 ≥ 𝟎 → 𝑖 ∶ int →(𝑐 ∶ 𝑐 𝑥 ≤ 𝑖 ∧ 𝑖 = 𝑥 + 𝑐 ) → int
𝑓 𝑖 = 𝑖	   	  	  	  	  	  𝐵𝑛𝑑 𝑖, 𝑐 ↦ 𝒄 ≤ 𝒊
2015/9/10

SAS	  2015

sum	  x	  terminates	  when	   𝑥 ≥ 0because	  𝑐 ≤ 𝑖17Outline• Refinement	  Type	  Optimization• Applications• Our	  Type	  Optimization	  Method• Implementation	  &	  Experiments• Summary

2015/9/10

SAS	  201518

Overall	  Structure
Functional	  Program
Constraint
Generationuser-­‐specified
preference	  order(max/min	  opt.
constraints	  +a	  priority	  order)

Horn	  Clause
Constraints
Horn	  Constraint
Optimization

additional
Horn	  Clause
constraints	  Refinement	  Types
2015/9/10SAS	  201519

Example:	  Type	  Optimization	  by	  Our	  Methodsum	  :	  (𝑥	  :	  {𝑥 ∣ P(𝑥)}) → {𝑦 ∣	   ⊥ }let	 rec sum	 x	 =	 if x	 =	 0	 then 0	 else x +	 sum	 (x-1)
Constraint
Generation⊥	  ⇐ 𝑃 𝑥 ∧ 𝑥 = 0,
𝐻abc = ∀𝑥.
𝑃 𝑥−1 ⇐𝑃 𝑥 ∧𝑥 ≠ 0
Horn	  Constraint
Optimization𝑥∶ 𝑥 𝑥<02015/9/10

SAS	  2015

𝑚𝑎𝑥	  (𝑃)→ {𝑦 ∣	  ⊥}20

Example:	  Horn	  Constraint	  Optimization
repeatedly	  improves	  a	  current	  solution
until	  convergence
𝐻abcSolve𝑃 𝑥 ↦⊥𝑚𝑎𝑥	  (𝑃)Gen.	  Horn	  Constraints	  for	  improved	  Sols.	  
Solve
2015/9/10

Requires	  any	  solution	  for	  𝑃 to	  be	  strictly	  better	  than	  ⊥∀𝑥. (𝑃 𝑥 ⇐	  ⊥),𝐻′ = 𝐻abc ∪¬∀𝑥. (⊥⇐ 𝑃 𝑥 )𝑚𝑎𝑥	  (𝑃)𝑃 𝑥 ↦ 𝑥 < 0 Gen.
SAS	  2015

… Solve

Converge(No	  Solution)
21Horn	  Constraint	  Solver Solve• Extended	  template-­‐based	  invariant	  generation	  techniques	  [Colon+	  ’03,	  Gulwani+	  ’08] to	  solve	  existentially-­‐quantified	  Horn	  clause	  constraints• Extend	  the	  reach	  from	  imperative	  programs	  w/o	  recursion	  	  to	  higher-­‐order	  non-­‐det.	  programs• Any	  other	  solver	  for	  the	  class	  of	  constraints	  can	  be	  used	  instead	  [Unno+	  ’13,	  Beyene+	  ’14,	  Kuwahara+	  ’15]

2015/9/10

SAS	  201522

Outline• Refinement	  Type	  Optimization• Applications• Our	  Type	  Optimization	  Method• Implementation	  &	  Experiments• Summary

2015/9/10

SAS	  201523

Implementation	  &	  ExperimentsA	  refinement	  type	  checking	  and	  inference	  tool	  for	  OCaml• Implemented	  in	  Refinement	  Caml [Unno+	  ’08,	  ’09,	  …]• Z3 [Moura+	  ’08] as	  a	  backend	  SMT	  solver• Two	  preliminary	  experiments:• Various	  program	  analysis	  problems	  forhigher-­‐order non-­‐deterministic	  programs(partly	  obtained	  from	  [Kuwahara+	  ’14, Kuwahara+	  ’15])• Non-­‐termination	  verification	  problems
for first-­‐order	  non-­‐deterministic	  programs(obtained	  from	  [Chen+	  ’14,	  Larraz+’14,	   Kuwahara+	  ’15,	  …])

2015/9/10

SAS	  201524

Results	  of	  the	  Various	  Program	  Analysis	  Problems	  (excerpt)
Programfoldr_nonterm[Kuwahara+	  ’15]
fixpoint_nonterm[Kuwahara+	  ’15]
indirectHO_e[Kuwahara+	  ’15]
zip
[Kuwahara+	  ’14]
sum

Application#Iter.

Time(sec)

Opt.

Non-­‐termination

48.04

✔

Non-­‐termination

20.30

✔

Non-­‐termination

20.31

✔

Conditional	  Termination Analysis

412.24

Conditional	  Termination Analysis

612.02

appendConditional	  11
10.66
Termination
Analysis[Kuwahara+ ’14]
2015/9/10
2015
Environment:	  Intel	  Core	  i7-­‐3770	  SAS	  (3.40GHz),	  16	  GB	  of	  RAM✔
✔
25

Results	  of	  the	  First-­‐Order
Non-­‐Termination	   Verification	  Problems
Our tool
CppInv[Larraz+ ’14]
T2-­‐TACAS[Chen+	   ’14]
MoCHi
[Kuwahara+	  ’15]
TNT
[Emmes+	  ’12]
2015/9/10

Verified
41Time	  Out
27

Other
1370

6551

030

48

26

719359SAS	  201526

Summary
Refinement	  type	  optimization	  problems• Infer	   Pareto-­‐optimal	   refinement	  types	  with	   respect	   to	  a	  user-­‐specified	  preference	  order• Has	  applications	   to	  various	   program	  analysis	  problems	  of	  higher-­‐order	   and	  non-­‐deterministic	  functional	  programs
Refinement	  type	  optimization	  method• Reduction	   to	  a	  Horn	   constraint	   optimization	  problem• Horn	   constraint	  optimization	  method• Repeatedly	  improve	  the	  current	  solution	  until	  convergence

Prototype	  implementation	  and	   preliminary	  experiments
2015/9/10

SAS	  2015

Thank	  you!
27