1# 2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3# 4# SPDX-License-Identifier: BSD-2-Clause 5# 6 7# code and classes for controlling SMT solvers, including 'fast' solvers, 8# which support SMTLIB2 push/pop and are controlled by pipe, and heavyweight 9# 'slow' solvers which are run once per problem on static input files. 10import signal 11solverlist_missing = """ 12This tool requires the use of an SMT solver. 13 14This tool searches for the file '.solverlist' in the current directory and 15in every parent directory up to the filesystem root. 16""" 17solverlist_format = """ 18The .solverlist format is one solver per line, e.g. 19 20# SONOLAR is the strongest offline solver in our experiments. 21SONOLAR: offline: /home/tsewell/bin/sonolar --input-format=smtlib2 22# CVC4 is useful in online and offline mode. 23CVC4: online: /home/tsewell/bin/cvc4 --incremental --lang smt --tlimit=5000 24CVC4: offline: /home/tsewell/bin/cvc4 --lang smt 25# Z3 is a useful online solver. Use of Z3 in offline mode is not recommended, 26# because it produces incompatible models. 27Z3 4.3: online: /home/tsewell/dev/z3-dist/build/z3 -t:2 -smt2 -in 28# Z3 4.3: offline: /home/tsewell/dev/z3-dist/build/z3 -smt2 -in 29 30N.B. only ONE online solver is needed, so Z3 is redundant in the above. 31 32Each non-comment line is ':' separated, with this pattern: 33name : online/offline/fast/slow : command 34 35The name is used to identify the solver. The second token specifies 36the solver mode. Solvers in "fast" or "online" mode must support all 37interactive SMTLIB2 features including push/pop. With "slow" or "offline" mode 38the solver will be executed once per query, and push/pop will not be used. 39 40The remainder of each line is a shell command that executes the solver in 41SMTLIB2 mode. For online solvers it is typically worth setting a resource 42limit, after which the offline solver will be run. 43 44The first online solver will be used. The offline solvers will be used in 45parallel, by default. The set to be used in parallel can be controlled with 46a strategy line e.g.: 47strategy: SONOLAR all, SONOLAR hyp, CVC4 hyp 48 49This specifies that SONOLAR and CVC4 should both be run on each hypothesis. In 50addition SONOLAR will be applied to try to solve all related hypotheses at 51once, which may be faster than solving them one at a time. 52""" 53 54solverlist_file = ['.solverlist'] 55class SolverImpl: 56 def __init__ (self, name, fast, args, timeout): 57 self.fast = fast 58 self.args = args 59 self.timeout = timeout 60 self.origname = name 61 self.mem_mode = None 62 if self.fast: 63 self.name = name + ' (online)' 64 else: 65 self.name = name + ' (offline)' 66 67 def __repr__ (self): 68 return 'SolverImpl (%r, %r, %r, %r)' % (self.name, 69 self.fast, self.args, self.timeout) 70 71def parse_solver (bits): 72 import os 73 import sys 74 mode_set = ['fast', 'slow', 'online', 'offline'] 75 if len (bits) < 3 or bits[1].lower () not in mode_set: 76 print 'solver.py: solver list could not be parsed' 77 print ' in %s' % solverlist_file[0] 78 print ' reading %r' % bits 79 print solverlist_format 80 sys.exit (1) 81 name = bits[0] 82 fast = (bits[1].lower () in ['fast', 'online']) 83 args = bits[2].split () 84 assert os.path.exists (args[0]), (args[0], bits) 85 if not fast: 86 timeout = 6000 87 else: 88 timeout = 30 89 return SolverImpl (name, fast, args, timeout) 90 91def find_solverlist_file (): 92 import os 93 import sys 94 path = os.path.abspath (os.getcwd ()) 95 while not os.path.exists (os.path.join (path, '.solverlist')): 96 (parent, _) = os.path.split (path) 97 if parent == path: 98 print "solver.py: '.solverlist' missing" 99 print solverlist_missing 100 print solverlist_format 101 sys.exit (1) 102 path = parent 103 fname = os.path.join (path, '.solverlist') 104 solverlist_file[0] = fname 105 return fname 106 107def get_solver_set (): 108 solvers = [] 109 strategy = None 110 for line in open (find_solverlist_file ()): 111 line = line.strip () 112 if not line or line.startswith ('#'): 113 continue 114 bits = [bit.strip () for bit in line.split (':', 2)] 115 if bits[0] == 'strategy': 116 [_, strat] = bits 117 strategy = parse_strategy (strat) 118 elif bits[0] == 'config': 119 [_, config] = bits 120 assert solvers 121 parse_config_change (config, solvers[-1]) 122 else: 123 solvers.append (parse_solver (bits)) 124 return (solvers, strategy) 125 126def parse_strategy (strat): 127 solvs = strat.split (',') 128 strategy = [] 129 for solv in solvs: 130 bits = solv.split () 131 if len (bits) != 2 or bits[1] not in ['all', 'hyp']: 132 print "solver.py: strategy element %r" % bits 133 print "found in .solverlist strategy line" 134 print "should be [solvername, 'all' or 'hyp']" 135 sys.exit (1) 136 strategy.append (tuple (bits)) 137 return strategy 138 139def parse_config_change (config, solver): 140 for assign in config.split (','): 141 bits = assign.split ('=') 142 assert len (bits) == 2, bits 143 [lhs, rhs] = bits 144 lhs = lhs.strip ().lower () 145 rhs = rhs.strip ().lower () 146 if lhs == 'mem_mode': 147 assert rhs in ['8', '32'] 148 solver.mem_mode = rhs 149 else: 150 assert not 'config understood', assign 151 152def load_solver_set (): 153 import sys 154 (solvers, strategy) = get_solver_set () 155 fast_solvers = [sv for sv in solvers if sv.fast] 156 slow_solvers = [sv for sv in solvers if not sv.fast] 157 slow_dict = dict ([(sv.origname, sv) for sv in slow_solvers]) 158 if strategy == None: 159 strategy = [(nm, strat) for nm in slow_dict 160 for strat in ['all', 'hyp']] 161 for (nm, strat) in strategy: 162 if nm not in slow_dict: 163 print "solver.py: strategy option %r" % nm 164 print "found in .solverlist strategy line" 165 print "not an offline solver (required for parallel use)" 166 print "(known offline solvers %s)" % slow_dict.keys () 167 sys.exit (1) 168 strategy = [(slow_dict[nm], strat) for (nm, strat) in strategy] 169 assert fast_solvers, solvers 170 assert slow_solvers, solvers 171 return (fast_solvers[0], slow_solvers[0], strategy, slow_dict.values ()) 172 173(fast_solver, slow_solver, strategy, model_strategy) = load_solver_set () 174 175from syntax import (Expr, fresh_name, builtinTs, true_term, false_term, 176 foldr1, mk_or, boolT, word32T, word8T, mk_implies, Type, get_global_wrapper) 177from target_objects import structs, rodata, sections, trace, printout 178from logic import mk_align_valid_ineq, pvalid_assertion1, pvalid_assertion2 179 180import syntax 181import subprocess 182import sys 183import resource 184import re 185import random 186import time 187import tempfile 188import os 189 190last_solver = [None] 191last_10_models = [] 192last_satisfiable_hyps = [None] 193last_hyps = [None] 194last_check_model_state = [None] 195inconsistent_hyps = [] 196 197active_solvers = [] 198max_active_solvers = [5] 199 200random_name = random.randrange (1, 10 ** 9) 201count = [0] 202 203save_solv_example_time = [-1] 204 205def save_solv_example (solv, last_msgs, comments = []): 206 count[0] += 1 207 name = 'ex_%d_%d' % (random_name, count[0]) 208 f = open ('smt_examples/' + name, 'w') 209 for msg in comments: 210 f.write ('; ' + msg + '\n') 211 solv.write_solv_script (f, last_msgs) 212 f.close () 213 214def write_last_solv_script (solv, fname): 215 f = open (fname, 'w') 216 hyps = last_hyps[0] 217 cmds = ['(assert %s)' % hyp for (hyp, _) in hyps] + ['(check-sat)'] 218 solv.write_solv_script (f, cmds) 219 f.close () 220 221def run_time (elapsed, proc): 222 user = None 223 sys = None 224 try: 225 import psutil 226 ps = psutil.Process (proc.pid) 227 ps_time = ps.cpu_times () 228 user = ps_time.user 229 sys = ps_time.system 230 if elapsed == None: 231 elapsed = time.time () - ps.create_time () 232 except ImportError, e: 233 return '(cannot import psutil, cannot time solver)' 234 except Exception, e: 235 pass 236 times = ['%.2fs %s' % (t, msg) 237 for (t, msg) in zip ([elapsed, user, sys], 238 ['elapsed', 'user', 'sys']) 239 if t != None] 240 if not times: 241 return '(unknown time)' 242 else: 243 return '(%s)' % ', '.join (times) 244 245def smt_typ (typ): 246 if typ.kind == 'Word': 247 return '(_ BitVec %d)' % typ.num 248 elif typ.kind == 'WordArray': 249 return '(Array (_ BitVec %d) (_ BitVec %d))' % tuple (typ.nums) 250 elif typ.kind == 'TokenWords': 251 return '(Array (_ BitVec %d) (_ BitVec %d))' % ( 252 token_smt_typ.num, typ.num) 253 return smt_typ_builtins[typ.name] 254 255token_smt_typ = syntax.word64T 256 257smt_typ_builtins = {'Bool':'Bool', 'Mem':'{MemSort}', 'Dom':'{MemDomSort}', 258 'Token': smt_typ (token_smt_typ)} 259 260smt_typs_omitted = set ([builtinTs['HTD'], builtinTs['PMS']]) 261 262smt_ops = dict (syntax.ops_to_smt) 263# these additional smt ops aren't used as keywords in the syntax 264more_smt_ops = { 265 'TokenWordsAccess': 'select', 'TokenWordsUpdate': 'store' 266} 267smt_ops.update (more_smt_ops) 268 269def smt_num (num, bits): 270 if num < 0: 271 return '(bvneg %s)' % smt_num (- num, bits) 272 if bits % 4 == 0: 273 digs = bits / 4 274 rep = '%x' % num 275 prefix = '#x' 276 else: 277 digs = bits 278 rep = '{x:b}'.format (x = num) 279 prefix = '#b' 280 rep = rep[-digs:] 281 rep = ('0' * (digs - len(rep))) + rep 282 assert len (rep) == digs 283 return prefix + rep 284 285def smt_num_t (num, typ): 286 assert typ.kind == 'Word', typ 287 return smt_num (num, typ.num) 288 289def mk_smt_expr (smt_expr, typ): 290 return Expr ('SMTExpr', typ, val = smt_expr) 291 292class EnvMiss (Exception): 293 def __init__ (self, name, typ): 294 self.name = name 295 self.typ = typ 296 297cheat_mem_doms = [True] 298 299tokens = {} 300 301def smt_expr (expr, env, solv): 302 if expr.is_op (['WordCast', 'WordCastSigned']): 303 [v] = expr.vals 304 assert v.typ.kind == 'Word' and expr.typ.kind == 'Word' 305 ex = smt_expr (v, env, solv) 306 if expr.typ == v.typ: 307 return ex 308 elif expr.typ.num < v.typ.num: 309 return '((_ extract %d 0) %s)' % (expr.typ.num - 1, ex) 310 else: 311 if expr.name == 'WordCast': 312 return '((_ zero_extend %d) %s)' % ( 313 expr.typ.num - v.typ.num, ex) 314 else: 315 return '((_ sign_extend %d) %s)' % ( 316 expr.typ.num - v.typ.num, ex) 317 elif expr.is_op (['ToFloatingPoint', 'ToFloatingPointSigned', 318 'ToFloatingPointUnsigned', 'FloatingPointCast']): 319 ks = [v.typ.kind for v in expr.vals] 320 expected_ks = {'ToFloatingPoint': ['Word'], 321 'ToFloatingPointSigned': ['Builtin', 'Word'], 322 'ToFloatingPointUnsigned': ['Builtin', 'Word'], 323 'FloatingPointCast': ['FloatingPoint']} 324 expected_ks = expected_ks[expr.name] 325 assert ks == expected_ks, (ks, expected_ks) 326 oname = 'to_fp' 327 if expr.name == 'ToFloatingPointUnsigned': 328 expr.name == 'to_fp_unsigned' 329 op = '(_ %s %d %d)' % tuple ([oname + expr.typ.nums]) 330 vs = [smt_expr (v, env, solv) for v in expr.vals] 331 return '(%s %s)' % (op, ' '.join (vs)) 332 elif expr.is_op (['CountLeadingZeroes', 'WordReverse']): 333 [v] = expr.vals 334 assert expr.typ.kind == 'Word' and expr.typ == v.typ 335 v = smt_expr (v, env, solv) 336 oper = solv.get_smt_derived_oper (expr.name, expr.typ.num) 337 return '(%s %s)' % (oper, v) 338 elif expr.is_op ('CountTrailingZeroes'): 339 [v] = expr.vals 340 expr = syntax.mk_clz (syntax.mk_word_reverse (v)) 341 return smt_expr (expr, env, solv) 342 elif expr.is_op (['PValid', 'PGlobalValid', 343 'PWeakValid', 'PArrayValid']): 344 if expr.name == 'PArrayValid': 345 [htd, typ_expr, p, num] = expr.vals 346 num = to_smt_expr (num, env, solv) 347 else: 348 [htd, typ_expr, p] = expr.vals 349 assert typ_expr.kind == 'Type' 350 typ = typ_expr.val 351 if expr.name == 'PGlobalValid': 352 typ = get_global_wrapper (typ) 353 if expr.name == 'PArrayValid': 354 typ = ('Array', typ, num) 355 else: 356 typ = ('Type', typ) 357 assert htd.kind == 'Var' 358 htd_s = env[(htd.name, htd.typ)] 359 p_s = smt_expr (p, env, solv) 360 var = solv.add_pvalids (htd_s, typ, p_s, expr.name) 361 return var 362 elif expr.is_op ('MemDom'): 363 [p, dom] = [smt_expr (e, env, solv) for e in expr.vals] 364 md = '(%s %s %s)' % (smt_ops[expr.name], p, dom) 365 solv.note_mem_dom (p, dom, md) 366 if cheat_mem_doms: 367 return 'true' 368 return md 369 elif expr.is_op ('MemUpdate'): 370 [m, p, v] = expr.vals 371 assert v.typ.kind == 'Word' 372 m_s = smt_expr (m, env, solv) 373 p_s = smt_expr (p, env, solv) 374 v_s = smt_expr (v, env, solv) 375 return smt_expr_memupd (m_s, p_s, v_s, v.typ, solv) 376 elif expr.is_op ('MemAcc'): 377 [m, p] = expr.vals 378 assert expr.typ.kind == 'Word' 379 m_s = smt_expr (m, env, solv) 380 p_s = smt_expr (p, env, solv) 381 return smt_expr_memacc (m_s, p_s, expr.typ, solv) 382 elif expr.is_op ('Equals') and expr.vals[0].typ == builtinTs['Mem']: 383 (x, y) = [smt_expr (e, env, solv) for e in expr.vals] 384 if x[0] == 'SplitMem' or y[0] == 'SplitMem': 385 assert not 'mem equality involving split possible', ( 386 x, y, expr) 387 sexp = '(mem-eq %s %s)' % (x, y) 388 solv.note_model_expr (sexp, boolT) 389 return sexp 390 elif expr.is_op ('Equals') and expr.vals[0].typ == word32T: 391 (x, y) = [smt_expr (e, env, solv) for e in expr.vals] 392 sexp = '(word32-eq %s %s)' % (x, y) 393 return sexp 394 elif expr.is_op ('StackEqualsImplies'): 395 [sp1, st1, sp2, st2] = [smt_expr (e, env, solv) 396 for e in expr.vals] 397 if sp1 == sp2 and st1 == st2: 398 return 'true' 399 assert st2[0] == 'SplitMem', (expr.vals, st2) 400 [_, split2, top2, bot2] = st2 401 if split2 != sp2: 402 res = solv.check_hyp_raw ('(= %s %s)' % (split2, sp2)) 403 assert res == 'unsat', (split2, sp2, expr.vals) 404 eq = solv.get_stack_eq_implies (split2, top2, st1) 405 return '(and (= %s %s) %s)' % (sp1, sp2, eq) 406 elif expr.is_op ('ImpliesStackEquals'): 407 [sp1, st1, sp2, st2] = expr.vals 408 eq = solv.add_implies_stack_eq (sp1, st1, st2, env) 409 sp1 = smt_expr (sp1, env, solv) 410 sp2 = smt_expr (sp2, env, solv) 411 return '(and (= %s %s) %s)' % (sp1, sp2, eq) 412 elif expr.is_op ('IfThenElse'): 413 (sw, x, y) = [smt_expr (e, env, solv) for e in expr.vals] 414 return smt_ifthenelse (sw, x, y, solv) 415 elif expr.is_op ('HTDUpdate'): 416 var = solv.add_var ('updated_htd', expr.typ) 417 return var 418 elif expr.kind == 'Op': 419 vals = [smt_expr (e, env, solv) for e in expr.vals] 420 if vals: 421 sexp = '(%s %s)' % (smt_ops[expr.name], ' '.join(vals)) 422 else: 423 sexp = smt_ops[expr.name] 424 maybe_note_model_expr (sexp, expr.typ, expr.vals, solv) 425 return sexp 426 elif expr.kind == 'Num': 427 return smt_num_t (expr.val, expr.typ) 428 elif expr.kind == 'Var': 429 if (expr.name, expr.typ) not in env: 430 trace ('Env miss for %s in smt_expr' % expr.name) 431 trace ('Environment is %s' % env) 432 raise EnvMiss (expr.name, expr.typ) 433 val = env[(expr.name, expr.typ)] 434 assert val[0] == 'SplitMem' or type(val) == str 435 return val 436 elif expr.kind == 'Invent': 437 var = solv.add_var ('invented', expr.typ) 438 return var 439 elif expr.kind == 'SMTExpr': 440 return expr.val 441 elif expr.kind == 'Token': 442 return solv.get_token (expr.name) 443 else: 444 assert not 'handled expr', expr 445 446def smt_expr_memacc (m, p, typ, solv): 447 if m[0] == 'SplitMem': 448 p = solv.cache_large_expr (p, 'memacc_pointer', syntax.word32T) 449 (_, split, top, bot) = m 450 top_acc = smt_expr_memacc (top, p, typ, solv) 451 bot_acc = smt_expr_memacc (bot, p, typ, solv) 452 return '(ite (bvule %s %s) %s %s)' % (split, p, top_acc, bot_acc) 453 if typ.num in [8, 32, 64]: 454 sexp = '(load-word%d %s %s)' % (typ.num, m, p) 455 else: 456 assert not 'word load type supported', typ 457 solv.note_model_expr (p, syntax.word32T) 458 solv.note_model_expr (sexp, typ) 459 return sexp 460 461def smt_expr_memupd (m, p, v, typ, solv): 462 if m[0] == 'SplitMem': 463 p = solv.cache_large_expr (p, 'memupd_pointer', syntax.word32T) 464 v = solv.cache_large_expr (v, 'memupd_val', typ) 465 (_, split, top, bot) = m 466 memT = syntax.builtinTs['Mem'] 467 top = solv.cache_large_expr (top, 'split_mem_top', memT) 468 top_upd = smt_expr_memupd (top, p, v, typ, solv) 469 bot = solv.cache_large_expr (bot, 'split_mem_bot', memT) 470 bot_upd = smt_expr_memupd (bot, p, v, typ, solv) 471 top = '(ite (bvule %s %s) %s %s)' % (split, p, top_upd, top) 472 bot = '(ite (bvule %s %s) %s %s)' % (split, p, bot, bot_upd) 473 return ('SplitMem', split, top, bot) 474 elif typ.num == 8: 475 p = solv.cache_large_expr (p, 'memupd_pointer', syntax.word32T) 476 p_align = '(bvand %s #xfffffffd)' % p 477 solv.note_model_expr (p_align, syntax.word32T) 478 solv.note_model_expr ('(load-word32 %s %s)' % (m, p_align), 479 syntax.word32T) 480 return '(store-word8 %s %s %s)' % (m, p, v) 481 elif typ.num in [32, 64]: 482 solv.note_model_expr ('(load-word%d %s %s)' % (typ.num, m, p), 483 typ) 484 solv.note_model_expr (p, syntax.word32T) 485 return '(store-word%d %s %s %s)' % (typ.num, m, p, v) 486 else: 487 assert not 'MemUpdate word width supported', typ 488 489def smt_ifthenelse (sw, x, y, solv): 490 if x[0] != 'SplitMem' and y[0] != 'SplitMem': 491 return '(ite %s %s %s)' % (sw, x, y) 492 zero = '#x00000000' 493 if x[0] != 'SplitMem': 494 (x_split, x_top, x_bot) = (zero, x, x) 495 else: 496 (_, x_split, x_top, x_bot) = x 497 if y[0] != 'SplitMem': 498 (y_split, y_top, y_bot) = (zero, y, y) 499 else: 500 (_, y_split, y_top, y_bot) = y 501 if x_split != y_split: 502 split = '(ite %s %s %s)' % (sw, x_split, y_split) 503 else: 504 split = x_split 505 return ('SplitMem', split, 506 '(ite %s %s %s)' % (sw, x_top, y_top), 507 '(ite %s %s %s)' % (sw, x_bot, y_bot)) 508 509def to_smt_expr (expr, env, solv): 510 if expr.typ == builtinTs['RelWrapper']: 511 vals = [to_smt_expr (v, env, solv) for v in expr.vals] 512 return syntax.adjust_op_vals (expr, vals) 513 s = smt_expr (expr, env, solv) 514 return mk_smt_expr (s, expr.typ) 515 516def typ_representable (typ): 517 return (typ.kind == 'Word' or typ == builtinTs['Bool'] 518 or typ == builtinTs['Token']) 519 520def maybe_note_model_expr (sexpr, typ, subexprs, solv): 521 """note this expression if values of its type can be represented 522 but one of the subexpression values can't be. 523 e.g. note (= x y) where the type of x/y is an SMT array.""" 524 if not typ_representable (typ): 525 return 526 if all ([typ_representable (v.typ) for v in subexprs]): 527 return 528 assert solv, (sexpr, typ) 529 solv.note_model_expr (sexpr, typ) 530 531def split_hyp_sexpr (hyp, accum): 532 if hyp[0] == 'and': 533 for h in hyp[1:]: 534 split_hyp_sexpr (h, accum) 535 elif hyp[0] == 'not' and hyp[1][0] == '=>': 536 (_, p, q) = hyp[1] 537 split_hyp_sexpr (p, accum) 538 split_hyp_sexpr (('not', q), accum) 539 elif hyp[0] == 'not' and hyp[1][0] == 'or': 540 for h in hyp[1][1:]: 541 split_hyp_sexpr (('not', h), accum) 542 elif hyp[0] == 'not' and hyp[1][0] == 'not': 543 split_hyp_sexpr (hyp[1][1], accum) 544 elif hyp[:1] + hyp[2:] == ('=>', 'false'): 545 split_hyp_sexpr (('not', hyp[1]), accum) 546 elif hyp[:1] == ('=', ) and ('true' in hyp or 'false' in hyp): 547 (_, p, q) = hyp 548 if q in ['true', 'false']: 549 (p, q) = (q, p) 550 if p == 'true': 551 split_hyp_sexpr (q, accum) 552 else: 553 split_hyp_sexpr (('not', q), accum) 554 else: 555 accum.append (hyp) 556 return accum 557 558def split_hyp (hyp): 559 if (hyp.startswith ('(and ') or hyp.startswith ('(not (=> ') 560 or hyp.startswith ('(not (or ') 561 or hyp.startswith ('(not (not ')): 562 return [flat_s_expression (h) for h in 563 split_hyp_sexpr (parse_s_expression (hyp), [])] 564 else: 565 return [hyp] 566 567mem_word8_preamble = [ 568'''(define-fun load-word32 ((m {MemSort}) (p (_ BitVec 32))) 569 (_ BitVec 32) 570(concat (concat (select m (bvadd p #x00000003)) (select m (bvadd p #x00000002))) 571 (concat (select m (bvadd p #x00000001)) (select m p)))) 572''', 573'''(define-fun load-word64 ((m {MemSort}) (p (_ BitVec 32))) 574 (_ BitVec 64) 575(bvor ((_ zero_extend 32) (load-word32 m p)) 576 (bvshl ((_ zero_extend 32) 577 (load-word32 m (bvadd p #x00000004))) #x0000000000000020)))''', 578'''(define-fun store-word32 ((m {MemSort}) (p (_ BitVec 32)) 579 (v (_ BitVec 32))) {MemSort} 580(store (store (store (store m p ((_ extract 7 0) v)) 581 (bvadd p #x00000001) ((_ extract 15 8) v)) 582 (bvadd p #x00000002) ((_ extract 23 16) v)) 583 (bvadd p #x00000003) ((_ extract 31 24) v)) 584) ''', 585'''(define-fun store-word64 ((m {MemSort}) (p (_ BitVec 32)) (v (_ BitVec 64))) 586 {MemSort} 587(store-word32 (store-word32 m p ((_ extract 31 0) v)) 588 (bvadd p #x00000004) ((_ extract 63 32) v)))''', 589'''(define-fun load-word8 ((m {MemSort}) (p (_ BitVec 32))) (_ BitVec 8) 590(select m p))''', 591'''(define-fun store-word8 ((m {MemSort}) (p (_ BitVec 32)) (v (_ BitVec 8))) 592 {MemSort} 593(store m p v))''', 594'''(define-fun mem-dom ((p (_ BitVec 32)) (d {MemDomSort})) Bool 595(not (= (select d p) #b0)))''', 596'''(define-fun mem-eq ((x {MemSort}) (y {MemSort})) Bool (= x y))''', 597'''(define-fun word32-eq ((x (_ BitVec 32)) (y (_ BitVec 32))) 598 Bool (= x y))''', 599'''(define-fun word2-xor-scramble ((a (_ BitVec 2)) (x (_ BitVec 2)) 600 (b (_ BitVec 2)) (c (_ BitVec 2)) (y (_ BitVec 2)) (d (_ BitVec 2))) Bool 601(bvult (bvadd (bvxor a x) b) (bvadd (bvxor c y) d)))''', 602'''(declare-fun unspecified-precond () Bool)''', 603] 604 605mem_word32_preamble = [ 606'''(define-fun load-word32 ((m {MemSort}) (p (_ BitVec 32))) 607 (_ BitVec 32) 608(select m ((_ extract 31 2) p)))''', 609'''(define-fun store-word32 ((m {MemSort}) (p (_ BitVec 32)) (v (_ BitVec 32))) 610 {MemSort} 611(store m ((_ extract 31 2) p) v))''', 612'''(define-fun load-word64 ((m {MemSort}) (p (_ BitVec 32))) 613 (_ BitVec 64) 614(bvor ((_ zero_extend 32) (load-word32 m p)) 615 (bvshl ((_ zero_extend 32) 616 (load-word32 m (bvadd p #x00000004))) #x0000000000000020)))''', 617'''(define-fun store-word64 ((m {MemSort}) (p (_ BitVec 32)) (v (_ BitVec 64))) 618 {MemSort} 619(store-word32 (store-word32 m p ((_ extract 31 0) v)) 620 (bvadd p #x00000004) ((_ extract 63 32) v)))''', 621'''(define-fun word8-shift ((p (_ BitVec 32))) (_ BitVec 32) 622(bvshl ((_ zero_extend 30) ((_ extract 1 0) p)) #x00000003))''', 623'''(define-fun word8-get ((p (_ BitVec 32)) (x (_ BitVec 32))) (_ BitVec 8) 624((_ extract 7 0) (bvlshr x (word8-shift p))))''', 625'''(define-fun load-word8 ((m {MemSort}) (p (_ BitVec 32))) (_ BitVec 8) 626(word8-get p (load-word32 m p)))''', 627'''(define-fun word8-put ((p (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 8))) 628 (_ BitVec 32) (bvor (bvshl ((_ zero_extend 24) y) (word8-shift p)) 629 (bvand x (bvnot (bvshl #x000000FF (word8-shift p))))))''', 630'''(define-fun store-word8 ((m {MemSort}) (p (_ BitVec 32)) (v (_ BitVec 8))) 631 {MemSort} 632(store-word32 m p (word8-put p (load-word32 m p) v)))''', 633'''(define-fun mem-dom ((p (_ BitVec 32)) (d {MemDomSort})) Bool 634(not (= (select d p) #b0)))''', 635'''(define-fun mem-eq ((x {MemSort}) (y {MemSort})) Bool (= x y))''', 636'''(define-fun word32-eq ((x (_ BitVec 32)) (y (_ BitVec 32))) 637 Bool (= x y))''', 638'''(define-fun word2-xor-scramble ((a (_ BitVec 2)) (x (_ BitVec 2)) 639 (b (_ BitVec 2)) (c (_ BitVec 2)) (y (_ BitVec 2)) (d (_ BitVec 2))) Bool 640(bvult (bvadd (bvxor a x) b) (bvadd (bvxor c y) d)))''', 641'''(declare-fun unspecified-precond () Bool)''' 642] 643 644word32_smt_convs = {'MemSort': '(Array (_ BitVec 30) (_ BitVec 32))', 645 'MemDomSort': '(Array (_ BitVec 32) (_ BitVec 1))'} 646word8_smt_convs = {'MemSort': '(Array (_ BitVec 32) (_ BitVec 8))', 647 'MemDomSort': '(Array (_ BitVec 32) (_ BitVec 1))'} 648 649def preexec (timeout): 650 def ret (): 651 # setting the session ID on a fork allows us to clean up 652 # the resulting process group, useful if running multiple 653 # solvers in parallel. 654 os.setsid () 655 if timeout != None: 656 resource.setrlimit(resource.RLIMIT_CPU, 657 (timeout, timeout)) 658 return ret 659 660class ConversationProblem (Exception): 661 def __init__ (self, prompt, response): 662 self.prompt = prompt 663 self.response = response 664 665def get_s_expression (stream, prompt): 666 try: 667 return get_s_expression_inner (stream, prompt) 668 except IOError, e: 669 raise ConversationProblem (prompt, 'IOError') 670 671def get_s_expression_inner (stdout, prompt): 672 """retreives responses from a solver until parens match""" 673 responses = [stdout.readline ().strip ()] 674 if not responses[0].startswith ('('): 675 bits = responses[0].split () 676 if len (bits) != 1: 677 raise ConversationProblem (prompt, responses[0]) 678 return bits[0] 679 lpars = responses[0].count ('(') 680 rpars = responses[0].count (')') 681 emps = 0 682 while rpars < lpars: 683 r = stdout.readline ().strip () 684 responses.append (r) 685 lpars += r.count ('(') 686 rpars += r.count (')') 687 if r == '': 688 emps += 1 689 if emps >= 3: 690 raise ConversationProblem (prompt, responses) 691 else: 692 emps = 0 693 return parse_s_expressions (responses) 694 695class SolverFailure (Exception): 696 def __init__ (self, msg): 697 self.msg = msg 698 699 def __str__ (self): 700 return 'SolverFailure (%r)' % self.msg 701 702class Solver: 703 def __init__ (self, produce_unsat_cores = False): 704 self.replayable = [] 705 self.unsat_cores = produce_unsat_cores 706 self.online_solver = None 707 self.parallel_solvers = {} 708 self.parallel_model_states = {} 709 710 self.names_used = {} 711 self.names_used_order = [] 712 self.external_names = {} 713 self.name_ext = '' 714 self.pvalids = {} 715 self.ptrs = {} 716 self.cached_exprs = {} 717 self.defs = {} 718 self.doms = set () 719 self.model_vars = set () 720 self.model_exprs = {} 721 self.arbitrary_vars = {} 722 self.stack_eqs = {} 723 self.mem_naming = {} 724 self.tokens = {} 725 self.smt_derived_ops = {} 726 727 self.num_hyps = 0 728 self.last_model_acc_hyps = (None, None) 729 730 self.pvalid_doms = None 731 self.assertions = [] 732 733 self.fast_solver = fast_solver 734 self.slow_solver = slow_solver 735 self.strategy = strategy 736 self.model_strategy = model_strategy 737 738 self.add_rodata_def () 739 740 last_solver[0] = self 741 742 def preamble (self, solver_impl): 743 preamble = [] 744 if solver_impl.fast: 745 preamble += ['(set-option :print-success true)'] 746 preamble += [ '(set-option :produce-models true)', 747 '(set-logic QF_AUFBV)', ] 748 if self.unsat_cores: 749 preamble += ['(set-option :produce-unsat-cores true)'] 750 751 if solver_impl.mem_mode == '8': 752 preamble.extend (mem_word8_preamble) 753 else: 754 preamble.extend (mem_word32_preamble) 755 return preamble 756 757 def startup_solver (self, use_this_solver = None): 758 if self not in active_solvers: 759 active_solvers.append (self) 760 while len (active_solvers) > max_active_solvers[0]: 761 solv = active_solvers.pop (0) 762 solv.close ('active solver limit') 763 764 if use_this_solver: 765 solver = use_this_solver 766 else: 767 solver = self.fast_solver 768 devnull = open (os.devnull, 'w') 769 self.online_solver = subprocess.Popen (solver.args, 770 stdin = subprocess.PIPE, stdout = subprocess.PIPE, 771 stderr = devnull, preexec_fn = preexec (solver.timeout)) 772 devnull.close () 773 774 for msg in self.preamble (solver): 775 self.send (msg, replay=False) 776 for (msg, _) in self.replayable: 777 self.send (msg, replay=False) 778 779 def close (self, reason = '?'): 780 self.close_parallel_solvers (reason = 'self.close (%s)' 781 % reason) 782 self.close_online_solver () 783 784 def close_online_solver (self): 785 if self.online_solver: 786 self.online_solver.stdin.close() 787 self.online_solver.stdout.close() 788 self.online_solver = None 789 790 def __del__ (self): 791 self.close ('__del__') 792 793 def smt_name (self, name, kind = ('Var', None), 794 ignore_external_names = False): 795 name = name.replace("'", "_").replace("#", "_").replace('"', "_") 796 if not ignore_external_names: 797 name = fresh_name (name, self.external_names) 798 name = fresh_name (name, self.names_used, kind) 799 self.names_used_order.append (name) 800 return name 801 802 def write (self, msg): 803 self.online_solver.stdin.write (msg + '\n') 804 self.online_solver.stdin.flush() 805 806 def send_inner (self, msg, replay = True, is_model = True): 807 if self.online_solver == None: 808 self.startup_solver () 809 810 msg = msg.format (** word32_smt_convs) 811 try: 812 self.write (msg) 813 response = self.online_solver.stdout.readline().strip() 814 except IOError, e: 815 raise ConversationProblem (msg, 'IOError') 816 if response != 'success': 817 raise ConversationProblem (msg, response) 818 819 def solver_loop (self, attempt): 820 err = None 821 for i in range (5): 822 if self.online_solver == None: 823 self.startup_solver () 824 try: 825 return attempt () 826 except ConversationProblem, e: 827 trace ('SMT conversation problem (attempt %d)' 828 % (i + 1)) 829 trace ('I sent %s' % repr (e.prompt)) 830 trace ('I got %s' % repr (e.response)) 831 trace ('restarting solver') 832 self.online_solver = None 833 err = (e.prompt, e.response) 834 trace ('Repeated SMT failure, giving up.') 835 raise ConversationProblem (err[0], err[1]) 836 837 def send (self, msg, replay = True, is_model = True): 838 self.solver_loop (lambda: self.send_inner (msg, 839 replay = replay, is_model = is_model)) 840 if replay: 841 self.replayable.append ((msg, is_model)) 842 843 def get_s_expression (self, prompt): 844 return get_s_expression (self.online_solver.stdout, prompt) 845 846 def prompt_s_expression_inner (self, prompt): 847 try: 848 self.write (prompt) 849 return self.get_s_expression (prompt) 850 except IOError, e: 851 raise ConversationProblem (prompt, 'IOError') 852 853 def prompt_s_expression (self, prompt): 854 return self.solver_loop (lambda: 855 self.prompt_s_expression_inner (prompt)) 856 857 def hyps_sat_raw_inner (self, hyps, model, unsat_core, 858 recursion = False): 859 self.send_inner ('(push 1)', replay = False) 860 for hyp in hyps: 861 self.send_inner ('(assert %s)' % hyp, replay = False, 862 is_model = False) 863 response = self.prompt_s_expression_inner ('(check-sat)') 864 if response not in set (['sat', 'unknown', 'unsat', '']): 865 raise ConversationProblem ('(check-sat)', response) 866 867 all_ok = True 868 m = {} 869 ucs = [] 870 if response == 'sat' and model: 871 all_ok = self.fetch_model (m) 872 if response == 'unsat' and unsat_core: 873 ucs = self.get_unsat_core () 874 all_ok = ucs != None 875 876 self.send_inner ('(pop 1)', replay = False) 877 878 return (response, m, ucs, all_ok) 879 880 def add_var (self, name, typ, kind = 'Var', 881 mem_name = None, 882 ignore_external_names = False): 883 if typ in smt_typs_omitted: 884 # skipped. not supported by all solvers 885 name = self.smt_name (name, ('Ghost', typ), 886 ignore_external_names = ignore_external_names) 887 return name 888 name = self.smt_name (name, kind = (kind, typ), 889 ignore_external_names = ignore_external_names) 890 self.send ('(declare-fun %s () %s)' % (name, smt_typ(typ))) 891 if typ_representable (typ) and kind != 'Aux': 892 self.model_vars.add (name) 893 if typ == builtinTs['Mem'] and mem_name != None: 894 if type (mem_name) == str: 895 self.mem_naming[name] = mem_name 896 else: 897 (nm, prev) = mem_name 898 if prev[0] == 'SplitMem': 899 prev = 'SplitMem' 900 prev = parse_s_expression (prev) 901 self.mem_naming[name] = (nm, prev) 902 return name 903 904 def add_var_restr (self, name, typ, mem_name = None): 905 name = self.add_var (name, typ, mem_name = mem_name) 906 return name 907 908 def add_def (self, name, val, env, ignore_external_names = False): 909 kind = 'Var' 910 if val.typ in smt_typs_omitted: 911 kind = 'Ghost' 912 smt = smt_expr (val, env, self) 913 if smt[0] == 'SplitMem': 914 (_, split, top, bot) = smt 915 def add (nm, typ, smt): 916 val = mk_smt_expr (smt, typ) 917 return self.add_def (name + '_' + nm, val, {}, 918 ignore_external_names = ignore_external_names) 919 split = add ('split', syntax.word32T, split) 920 top = add ('top', val.typ, top) 921 bot = add ('bot', val.typ, bot) 922 return ('SplitMem', split, top, bot) 923 924 name = self.smt_name (name, kind = (kind, val.typ), 925 ignore_external_names = ignore_external_names) 926 if kind == 'Ghost': 927 # skipped. not supported by all solvers 928 return name 929 if val.kind == 'Var': 930 trace ('WARNING: redef of var %r to name %s' % (val, name)) 931 932 typ = smt_typ (val.typ) 933 self.send ('(define-fun %s () %s %s)' % (name, typ, smt)) 934 935 self.defs[name] = parse_s_expression (smt) 936 if typ_representable (val.typ): 937 self.model_vars.add (name) 938 939 return name 940 941 def add_rodata_def (self): 942 ro_name = self.smt_name ('rodata', kind = 'Fun') 943 imp_ro_name = self.smt_name ('implies-rodata', kind = 'Fun') 944 assert ro_name == 'rodata', repr (ro_name) 945 assert imp_ro_name == 'implies-rodata', repr (imp_ro_name) 946 [rodata_data, rodata_ranges, rodata_ptrs] = rodata 947 if not rodata_ptrs: 948 assert not rodata_data 949 ro_def = 'true' 950 imp_ro_def = 'true' 951 else: 952 ro_witness = self.add_var ('rodata-witness', word32T) 953 ro_witness_val = self.add_var ('rodata-witness-val', word32T) 954 assert ro_witness == 'rodata-witness' 955 assert ro_witness_val == 'rodata-witness-val' 956 eq_vs = [(smt_num (p, 32), smt_num (v, 32)) 957 for (p, v) in rodata_data.iteritems ()] 958 eq_vs.append ((ro_witness, ro_witness_val)) 959 eqs = ['(= (load-word32 m %s) %s)' % v for v in eq_vs] 960 ro_def = '(and %s)' % ' \n '.join (eqs) 961 ro_ineqs = ['(and (bvule %s %s) (bvule %s %s))' 962 % (smt_num (start, 32), ro_witness, 963 ro_witness, smt_num (end, 32)) 964 for (start, end) in rodata_ranges] 965 assns = ['(or %s)' % ' '.join (ro_ineqs), 966 '(= (bvand rodata-witness #x00000003) #x00000000)'] 967 for assn in assns: 968 self.assert_fact_smt (assn) 969 imp_ro_def = eqs[-1] 970 self.send ('(define-fun rodata ((m %s)) Bool %s)' % ( 971 smt_typ (builtinTs['Mem']), ro_def)) 972 self.send ('(define-fun implies-rodata ((m %s)) Bool %s)' % ( 973 smt_typ (builtinTs['Mem']), imp_ro_def)) 974 975 def get_eq_rodata_witness (self, v): 976 # depends on assertion above, should probably fix this 977 ro_witness = mk_smt_expr ('rodata-witness', word32T) 978 return syntax.mk_eq (ro_witness, v) 979 980 def check_hyp_raw (self, hyp, model = None, force_solv = False, 981 hyp_name = None): 982 return self.hyps_sat_raw ([('(not %s)' % hyp, None)], 983 model = model, unsat_core = None, 984 force_solv = force_solv, hyps_name = hyp_name) 985 986 def next_hyp (self, (hyp, tag), hyp_dict): 987 self.num_hyps += 1 988 name = 'hyp%d' % self.num_hyps 989 hyp_dict[name] = tag 990 return '(! %s :named %s)' % (hyp, name) 991 992 def hyps_sat_raw (self, hyps, model = None, unsat_core = None, 993 force_solv = False, recursion = False, 994 slow_solver = None, hyps_name = None): 995 assert self.unsat_cores or unsat_core == None 996 997 hyp_dict = {} 998 raw_hyps = [(hyp2, tag) for (hyp, tag) in hyps 999 for hyp2 in split_hyp (hyp)] 1000 last_hyps[0] = list (raw_hyps) 1001 hyps = [self.next_hyp (h, hyp_dict) for h in raw_hyps] 1002 succ = False 1003 solvs_used = [] 1004 if hyps_name == None: 1005 hyps_name = 'group of %d hyps' % len (hyps) 1006 trace ('testing %s:' % hyps_name) 1007 if recursion: 1008 trace (' (recursion)') 1009 else: 1010 for (hyp, _) in raw_hyps: 1011 trace (' ' + hyp) 1012 1013 if force_solv != 'Slow': 1014 solvs_used.append (self.fast_solver.name) 1015 l = lambda: self.hyps_sat_raw_inner (hyps, 1016 model != None, unsat_core != None, 1017 recursion = recursion) 1018 try: 1019 (response, m, ucs, succ) = self.solver_loop (l) 1020 except ConversationProblem, e: 1021 response = 'ConversationProblem' 1022 1023 if succ and m and not recursion: 1024 succ = self.check_model ([h for (h, _) in raw_hyps], m) 1025 1026 if slow_solver == None: 1027 slow_solver = self.slow_solver 1028 if ((not succ or response not in ['sat', 'unsat']) 1029 and slow_solver and force_solv != 'Fast'): 1030 if solvs_used: 1031 trace ('failed to get result from %s' 1032 % solvs_used[0]) 1033 trace ('running %s' % slow_solver.name) 1034 self.close_online_solver () 1035 solvs_used.append (slow_solver.name) 1036 response = self.use_slow_solver (raw_hyps, 1037 model = model, unsat_core = unsat_core, 1038 use_this_solver = slow_solver) 1039 elif not succ: 1040 pass 1041 elif m: 1042 model.clear () 1043 model.update (m) 1044 elif ucs: 1045 unsat_core.extend (self.get_unsat_core_tags (ucs, 1046 hyp_dict)) 1047 1048 if response == 'sat': 1049 if not recursion: 1050 last_satisfiable_hyps[0] = list (raw_hyps) 1051 if model and not recursion: 1052 assert self.check_model ([h for (h, _) in raw_hyps], 1053 model) 1054 elif response == 'unsat': 1055 fact = '(not (and %s))' % ' '.join ([h 1056 for (h, _) in raw_hyps]) 1057 # sending this fact (and not its core-deps) might 1058 # lead to inaccurate cores in the future 1059 if not self.unsat_cores: 1060 self.send ('(assert %s)' % fact) 1061 else: 1062 # couldn't get a useful response from either solver. 1063 trace ('Solvers %s failed to resolve sat/unsat' 1064 % solvs_used) 1065 trace ('last solver result %r' % response) 1066 raise SolverFailure (response) 1067 return response 1068 1069 def get_unsat_core_tags (self, fact_names, hyps): 1070 names = set (fact_names) 1071 trace ('uc names: %s' % names) 1072 core = [hyps[name] for name in names 1073 if name.startswith ('hyp')] 1074 for s in fact_names: 1075 if s.startswith ('assert'): 1076 n = int (s[6:]) 1077 core.append (self.assertions[n][1]) 1078 trace ('uc tags: %s' % core) 1079 return core 1080 1081 def write_solv_script (self, f, input_msgs, solver = slow_solver, 1082 only_if_is_model = False): 1083 if solver.mem_mode == '8': 1084 smt_convs = word8_smt_convs 1085 else: 1086 smt_convs = word32_smt_convs 1087 for msg in self.preamble (solver): 1088 msg = msg.format (** smt_convs) 1089 f.write (msg + '\n') 1090 for (msg, is_model) in self.replayable: 1091 if only_if_is_model and not is_model: 1092 continue 1093 msg = msg.format (** smt_convs) 1094 f.write (msg + '\n') 1095 1096 for msg in input_msgs: 1097 msg = msg.format (** smt_convs) 1098 f.write (msg + '\n') 1099 1100 f.flush () 1101 1102 def exec_slow_solver (self, input_msgs, timeout = None, 1103 use_this_solver = None): 1104 solver = self.slow_solver 1105 if use_this_solver: 1106 solver = use_this_solver 1107 if not solver: 1108 return 'no-slow-solver' 1109 1110 (fd, name) = tempfile.mkstemp (suffix='.txt', 1111 prefix='graph-refine-problem-') 1112 tmpfile_write = open (name, 'w') 1113 self.write_solv_script (tmpfile_write, input_msgs, 1114 solver = solver) 1115 tmpfile_write.close () 1116 1117 proc = subprocess.Popen (solver.args, 1118 stdin = fd, stdout = subprocess.PIPE, 1119 preexec_fn = preexec (timeout)) 1120 os.close (fd) 1121 os.unlink (name) 1122 1123 return (proc, proc.stdout) 1124 1125 def use_slow_solver (self, hyps, model = None, unsat_core = None, 1126 use_this_solver = None): 1127 start = time.time () 1128 1129 cmds = ['(assert %s)' % hyp for (hyp, _) in hyps 1130 ] + ['(check-sat)'] 1131 1132 if model != None: 1133 cmds.append (self.fetch_model_request ()) 1134 1135 if use_this_solver: 1136 solver = use_this_solver 1137 else: 1138 solver = self.slow_solver 1139 1140 (proc, output) = self.exec_slow_solver (cmds, 1141 timeout = solver.timeout, use_this_solver = solver) 1142 1143 response = output.readline ().strip () 1144 if model != None and response == 'sat': 1145 assert self.fetch_model_response (model, 1146 stream = output) 1147 if unsat_core != None and response == 'unsat': 1148 trace ('WARNING no unsat core from %s' % solver.name) 1149 unsat_core.extend ([tag for (_, tag) in hyps]) 1150 1151 output.close () 1152 1153 if response not in ['sat', 'unsat']: 1154 trace ('SMT conversation problem after (check-sat)') 1155 1156 end = time.time () 1157 trace ('Got %r from %s.' % (response, solver.name)) 1158 trace (' after %s' % run_time (end - start, proc)) 1159 # adjust to save difficult problems 1160 cutoff_time = save_solv_example_time[0] 1161 if cutoff_time != -1 and end - start > cutoff_time: 1162 save_solv_example (self, cmds, 1163 comments = ['reference time %s seconds' % (end - start)]) 1164 1165 if model: 1166 assert self.check_model ([h for (h, _) in hyps], model) 1167 1168 return response 1169 1170 def add_parallel_solver (self, k, hyps, model = None, 1171 use_this_solver = None): 1172 cmds = ['(assert %s)' % hyp for hyp in hyps] + ['(check-sat)'] 1173 1174 if model != None: 1175 cmds.append (self.fetch_model_request ()) 1176 1177 trace (' --> new parallel solver %s' % str (k)) 1178 1179 if k in self.parallel_solvers: 1180 raise IndexError ('duplicate parallel solver ID', k) 1181 solver = self.slow_solver 1182 if use_this_solver: 1183 solver = use_this_solver 1184 (proc, output) = self.exec_slow_solver (cmds, 1185 timeout = solver.timeout, use_this_solver = solver) 1186 self.parallel_solvers[k] = (hyps, proc, output, solver, model) 1187 1188 def wait_parallel_solver_step (self): 1189 import select 1190 assert self.parallel_solvers 1191 fds = dict ([(output.fileno (), k) for (k, (_, _, output, _, _)) 1192 in self.parallel_solvers.iteritems ()]) 1193 try: 1194 (rlist, _, _) = select.select (fds.keys (), [], []) 1195 except KeyboardInterrupt, e: 1196 self.close_parallel_solvers (reason = 'interrupted') 1197 raise e 1198 k = fds[rlist.pop ()] 1199 (hyps, proc, output, solver, model) = self.parallel_solvers[k] 1200 del self.parallel_solvers[k] 1201 response = output.readline ().strip () 1202 trace (' <-- parallel solver %s closed: %s' % (k, response)) 1203 trace (' after %s' % run_time (None, proc)) 1204 if response not in ['sat', 'unsat']: 1205 trace ('SMT conversation problem in parallel solver') 1206 trace ('Got %r from %s in parallel.' % (response, solver.name)) 1207 m = {} 1208 check = None 1209 if response == 'sat': 1210 last_satisfiable_hyps[0] = hyps 1211 if k[0] != 'ModelRepair': 1212 if model == None or response != 'sat': 1213 output.close () 1214 return (k, hyps, response) 1215 # model issues 1216 m = {} 1217 if model != None: 1218 res = self.fetch_model_response (m, stream = output) 1219 output.close () 1220 if model != None and not res: 1221 # just drop this solver at this point 1222 trace ('failed to extract model.') 1223 return None 1224 if k[0] == 'ModelRepair': 1225 (_, k, i) = k 1226 (state, hyps) = self.parallel_model_states[k] 1227 else: 1228 i = 0 1229 state = None 1230 res = self.check_model_iteration (hyps, state, (response, m)) 1231 (kind, details) = res 1232 if kind == 'Abort': 1233 return None 1234 elif kind == 'Result': 1235 model.update (details) 1236 return (k, hyps, 'sat') 1237 elif kind == 'Continue': 1238 (solv, test_hyps, state) = details 1239 self.parallel_model_states[k] = (state, hyps) 1240 k = ('ModelRepair', k, i + 1) 1241 self.add_parallel_solver (k, test_hyps, 1242 use_this_solver = solv, model = model) 1243 return None 1244 1245 def wait_parallel_solver (self): 1246 while True: 1247 assert self.parallel_solvers 1248 try: 1249 res = self.wait_parallel_solver_step () 1250 except ConversationProblem, e: 1251 continue 1252 if res != None: 1253 return res 1254 1255 def close_parallel_solvers (self, ks = None, reason = '?'): 1256 if ks == None: 1257 ks = self.parallel_solvers.keys () 1258 else: 1259 ks = [k for k in ks if k in self.parallel_solvers] 1260 solvs = [(proc, output) for (_, proc, output, _, _) 1261 in [self.parallel_solvers[k] for k in ks]] 1262 if ks: 1263 trace (' X<-- %d parallel solvers killed: %s' 1264 % (len (ks), reason)) 1265 for k in ks: 1266 del self.parallel_solvers[k] 1267 procs = [proc for (proc, _) in solvs] 1268 outputs = [output for (_, output) in solvs] 1269 for proc in procs: 1270 os.killpg (proc.pid, signal.SIGTERM) 1271 for output in outputs: 1272 output.close () 1273 for proc in procs: 1274 os.killpg (proc.pid, signal.SIGKILL) 1275 proc.wait () 1276 1277 def parallel_check_hyps (self, hyps, env, model = None): 1278 """test a series of keyed hypotheses [(k1, h1), (k2, h2) ..etc] 1279 either returns (True, -) all hypotheses true 1280 or (False, ki) i-th hypothesis unprovable""" 1281 hyps = [(k, hyp) for (k, hyp) in hyps 1282 if not self.test_hyp (hyp, env, force_solv = 'Fast', 1283 catch = True, hyp_name = "('hyp', %s)" % k)] 1284 assert not self.parallel_solvers 1285 if not hyps: 1286 return ('unsat', None) 1287 all_hyps = foldr1 (syntax.mk_and, [h for (k, h) in hyps]) 1288 def spawn ((k, hyp), stratkey): 1289 goal = smt_expr (syntax.mk_not (hyp), env, self) 1290 [self.add_parallel_solver ((solver.name, strat, k), 1291 [goal], use_this_solver = solver, 1292 model = model) 1293 for (solver, strat) in self.strategy 1294 if strat == stratkey] 1295 if len (hyps) > 1: 1296 spawn ((None, all_hyps), 'all') 1297 spawn (hyps[0], 'hyp') 1298 solved = 0 1299 while True: 1300 ((nm, strat, k), _, res) = self.wait_parallel_solver () 1301 if strat == 'all' and res == 'unsat': 1302 trace (' -- hyps all confirmed by %s' % nm) 1303 break 1304 elif strat == 'hyp' and res == 'sat': 1305 trace (' -- hyp refuted by %s' % nm) 1306 break 1307 elif strat == 'hyp' and res == 'unsat': 1308 ks = [(solver.name, strat, k) 1309 for (solver, strat) in self.strategy] 1310 self.close_parallel_solvers (ks, 1311 reason = 'hyp shown unsat') 1312 solved += 1 1313 if solved < len (hyps): 1314 spawn (hyps[solved], 'hyp') 1315 else: 1316 trace (' - hyps confirmed individually') 1317 break 1318 if not self.parallel_solvers: 1319 res = 'timeout' 1320 trace (' - all solvers timed out or failed.') 1321 break 1322 self.close_parallel_solvers (reason = ('checked %r' % res)) 1323 return (res, k) 1324 1325 def parallel_test_hyps (self, hyps, env, model = None): 1326 (res, k) = self.parallel_check_hyps (hyps, env, model) 1327 return (res == 'unsat', k, res) 1328 1329 def slow_solver_multisat (self, hyps, model = None, timeout = 300): 1330 trace ('multisat check.') 1331 start = time.time () 1332 1333 cmds = [] 1334 for hyp in hyps: 1335 cmds.extend (['(assert %s)' % hyp, '(check-sat)']) 1336 if model != None: 1337 cmds.append (self.fetch_model_request ()) 1338 (proc, output) = self.exec_slow_solver (cmds, timeout = timeout) 1339 1340 assert hyps 1341 for (i, hyp) in enumerate (hyps): 1342 trace ('multisat checking %s' % hyp) 1343 response = output.readline ().strip () 1344 if response == 'sat': 1345 if model != None: 1346 model.clear () 1347 most_sat = hyps[: i + 1] 1348 assert self.fetch_model_response (model, 1349 stream = output) 1350 else: 1351 self.solver = None 1352 if i == 0 and response == 'unsat': 1353 self.send ('(assert (not %s))' % hyp) 1354 if i > 0: 1355 if response != 'unsat': 1356 trace ('conversation problem:') 1357 trace ('multisat got %r' % response) 1358 response = 'sat' 1359 break 1360 1361 if model: 1362 assert self.check_model (most_sat, model) 1363 1364 end = time.time () 1365 trace ('multisat final result: %r after %s' % (response, 1366 run_time (end - start, proc))) 1367 output.close () 1368 1369 return response 1370 1371 def fetch_model_request (self): 1372 vs = self.model_vars 1373 exprs = self.model_exprs 1374 1375 trace ('will fetch model%s for %d vars and %d compound exprs.' 1376 % (self.name_ext, len (vs), len (exprs))) 1377 1378 vs2 = tuple (vs) + tuple ([nm for (nm, typ) in exprs.values ()]) 1379 return '(get-value (%s))' % ' '.join (vs2) 1380 1381 def fetch_model_response (self, model, stream = None, recursion = False): 1382 if stream == None: 1383 stream = self.online_solver.stdout 1384 values = get_s_expression (stream, 1385 'fetch_model_response') 1386 if values == None: 1387 trace ('Failed to fetch model!') 1388 return None 1389 1390 expected_set = set (list (self.model_vars) 1391 + [nm for (nm, typ) in self.model_exprs.values ()]) 1392 malformed = [v for v in values if len (v) != 2 1393 or v[0] not in expected_set] 1394 if malformed: 1395 trace ('bad model response components:') 1396 for v in malformed: 1397 trace (repr (v)) 1398 return None 1399 1400 filt_values = [(nm, v) for (nm, v) in values 1401 if type (v) == str or '_' in v 1402 if set (v) != set (['?'])] 1403 dropped = len (values) - len (filt_values) 1404 if dropped: 1405 trace ('Dropped %d of %d values' % (dropped, len (values))) 1406 if recursion: 1407 trace (' .. aborting recursive attempt.') 1408 return None 1409 1410 abbrvs = [(sexp, name) for (sexp, (name, typ)) 1411 in self.model_exprs.iteritems ()] 1412 1413 r = make_model (filt_values, model, abbrvs) 1414 if dropped: 1415 model[('IsIncomplete', None)] = True 1416 return r 1417 1418 def get_arbitrary_vars (self, typ): 1419 self.arbitrary_vars.setdefault (typ, []) 1420 vs = self.arbitrary_vars[typ] 1421 def add (): 1422 v = self.add_var ('arbitary-var', typ, kind = 'Aux') 1423 vs.append (v) 1424 return v 1425 import itertools 1426 return itertools.chain (vs, itertools.starmap (add, 1427 itertools.repeat ([]))) 1428 1429 def force_model_accuracy_hyps (self): 1430 if len (self.model_exprs) == self.last_model_acc_hyps[0]: 1431 return self.last_model_acc_hyps[1] 1432 words = set () 1433 for (var_nm, typ) in self.model_exprs.itervalues (): 1434 if typ.kind == 'Word': 1435 s = '((_ extract %d %d) %s)' % (typ.num - 1, 1436 typ.num - 2, var_nm) 1437 words.add (s) 1438 elif typ == syntax.boolT: 1439 s = '(ite %s #b10 #b01)' % var_nm 1440 words.add (s) 1441 else: 1442 assert not 'model acc type known', typ 1443 hyps = [] 1444 w2T = syntax.Type ('Word', 2) 1445 arb_vars = self.get_arbitrary_vars (w2T) 1446 while words: 1447 while len (words) < 4: 1448 words.add (arb_vars.next ()) 1449 [a, b, c, d] = [words.pop () for x in range (4)] 1450 x = arb_vars.next () 1451 y = arb_vars.next () 1452 hyps.append (('(word2-xor-scramble %s)' 1453 % ' '.join ([a, x, b, c, y, d]), None)) 1454 self.last_model_acc_hyps = (len (self.model_exprs), hyps) 1455 return hyps 1456 1457 def check_model_iteration (self, hyps, state, (res, model)): 1458 """process an iteration of checking a model. the solvers 1459 sometimes give partially bogus models, which we need to 1460 check for. 1461 the state at any time is (confirmed, test, cand_model, solvs) 1462 We build additional hypotheses (e.g. x = 0) from models. 1463 The 'confirmed' additional hyps have been shown sat together 1464 with the original hyps, and 'test' are under test this 1465 iteration. If the test is true, 'cand_model' will be 1466 confirmed to be a valid (possibly incomplete) model. 1467 We may prune a model down to an incomplete one to try to 1468 find a valid part. The 'solvs' are solvers which have yet 1469 to have a model tested (as candidate) from the current 1470 'confirmed' hyps.""" 1471 if state == None: 1472 test = [] 1473 confirmed = hyps 1474 assert res == 'sat' 1475 cand_model = None 1476 solvs = self.model_strategy 1477 else: 1478 (confirmed, test, cand_model, solvs) = state 1479 1480 if cand_model and res == 'sat': 1481 if ('IsIncomplete', None) not in cand_model: 1482 return ('Result', cand_model) 1483 1484 if res == 'sat': 1485 if set (test) - set (confirmed): 1486 # confirm experiment 1487 confirmed = sorted (set (confirmed + test)) 1488 # progress was made, reenable all solvers 1489 solvs = solvs + [s for s in self.model_strategy 1490 if s not in solvs] 1491 elif res == 'unsat' and not test: 1492 printout ("WARNING: inconsistent sat/unsat.") 1493 inconsistent_hyps.append ((self, hyps, confirmed)) 1494 return ('Abort', None) 1495 else: 1496 # since not sat, ignore model contents 1497 model = None 1498 1499 # the candidate model wasn't confirmed, but might we 1500 # learn more by reducing it? 1501 if cand_model and res != 'sat': 1502 reduced = self.reduce_model (cand_model, hyps) 1503 r_hyps = get_model_hyps (reduced, self) 1504 solv = (solvs + self.model_strategy)[0] 1505 if set (r_hyps) - set (confirmed): 1506 return ('Continue', (solv, confirmed + r_hyps, 1507 (confirmed, r_hyps, None, solvs))) 1508 1509 # ignore the candidate model now, and try to continue with 1510 # the most recently returned model. that expires the solver 1511 # that produced this model from solvs 1512 solvs = solvs[1:] 1513 if not model and not solvs: 1514 # out of options 1515 return ('Abort', None) 1516 solv = (solvs + self.model_strategy)[0] 1517 1518 if model: 1519 test_hyps = get_model_hyps (model, self) 1520 else: 1521 model = None 1522 test_hyps = [] 1523 return ('Continue', (solv, confirmed + test_hyps, 1524 (confirmed, test_hyps, model, solvs))) 1525 1526 def check_model (self, hyps, model): 1527 orig_model = model 1528 state = None 1529 arg = ('sat', dict (model)) 1530 while True: 1531 res = self.check_model_iteration (hyps, state, arg) 1532 (kind, details) = res 1533 if kind == 'Abort': 1534 return False 1535 elif kind == 'Result': 1536 orig_model.clear () 1537 orig_model.update (details) 1538 return True 1539 assert kind == 'Continue' 1540 (solv, test_hyps, state) = details 1541 m = {} 1542 res = self.hyps_sat_raw (test_hyps, model = m, 1543 force_solv = solv, recursion = True) 1544 arg = (res, m) 1545 1546 def reduce_model (self, model, hyps): 1547 all_hyps = hyps + [h for (h, _) in self.assertions] 1548 all_hyps = map (parse_s_expression, all_hyps) 1549 m = reduce_model (model, self, all_hyps) 1550 trace ('reduce model size: %d --> %d' % (len (model), len (m))) 1551 return m 1552 1553 def fetch_model (self, model, recursion = False): 1554 try: 1555 self.write (self.fetch_model_request ()) 1556 except IOError, e: 1557 raise ConversationProblem ('fetch-model', 'IOError') 1558 return self.fetch_model_response (model, recursion = recursion) 1559 1560 def get_unsat_core (self): 1561 res = self.prompt_s_expression_inner ('(get-unsat-core)') 1562 if res == None: 1563 return None 1564 if [s for s in res if type (s) != str]: 1565 raise ConversationProblem ('(get-unsat-core)', res) 1566 return res 1567 1568 def check_hyp (self, hyp, env, model = None, force_solv = False, 1569 hyp_name = None): 1570 hyp = smt_expr (hyp, env, self) 1571 return self.check_hyp_raw (hyp, model = model, 1572 force_solv = force_solv, hyp_name = hyp_name) 1573 1574 def test_hyp (self, hyp, env, model = None, force_solv = False, 1575 catch = False, hyp_name = None): 1576 if catch: 1577 try: 1578 res = self.check_hyp (hyp, env, model = model, 1579 force_solv = force_solv, 1580 hyp_name = hyp_name) 1581 except SolverFailure, e: 1582 return False 1583 else: 1584 res = self.check_hyp (hyp, env, model = model, 1585 force_solv = force_solv, hyp_name = hyp_name) 1586 return res == 'unsat' 1587 1588 def assert_fact_smt (self, fact, unsat_tag = None): 1589 self.assertions.append ((fact, unsat_tag)) 1590 if unsat_tag and self.unsat_cores: 1591 name = 'assert%d' % len (self.assertions) 1592 self.send ('(assert (! %s :named %s))' % (fact, name), 1593 is_model = False) 1594 else: 1595 self.send ('(assert %s)' % fact) 1596 1597 def assert_fact (self, fact, env, unsat_tag = None): 1598 fact = smt_expr (fact, env, self) 1599 self.assert_fact_smt (fact, unsat_tag = unsat_tag) 1600 1601 def get_smt_derived_oper (self, name, n): 1602 if (name, n) in self.smt_derived_ops: 1603 return self.smt_derived_ops[(name, n)] 1604 if n != 1: 1605 m = n / 2 1606 top = '((_ extract %d %d) x)' % (n - 1, m) 1607 bot = '((_ extract %d 0) x)' % (m - 1) 1608 top_app = '(%s %s)' % (self.get_smt_derived_oper ( 1609 name, n - m), top) 1610 top_appx = '((_ zero_extend %d) %s)' % (m, top_app) 1611 bot_app = '(%s %s)' % (self.get_smt_derived_oper ( 1612 name, m), bot) 1613 bot_appx = '((_ zero_extend %d) %s)' % (n - m, bot_app) 1614 if name == 'CountLeadingZeroes': 1615 fname = 'bvclz_%d' % n 1616 elif name == 'WordReverse': 1617 fname = 'bvrev_%d' % n 1618 else: 1619 assert not 'name understood', (name, n) 1620 fname = self.smt_name (fname, kind = 'Fun') 1621 1622 if name == 'CountLeadingZeroes' and n == 1: 1623 self.send ('(define-fun %s ((x (_ BitVec 1)))' % fname 1624 + ' (_ BitVec 1) (ite (= x #b0) #b1 #b0))') 1625 elif name == 'CountLeadingZeroes': 1626 self.send (('(define-fun %s ((x (_ BitVec %d)))' 1627 + ' (_ BitVec %d) (ite (= %s %s)' 1628 + ' (bvadd %s %s) %s))') 1629 % (fname, n, n, top, smt_num (0, n - m), 1630 bot_appx, smt_num (m, n), top_appx)) 1631 elif name == 'WordReverse' and n == 1: 1632 self.send ('(define-fun %s ((x (_ BitVec 1)))' % fname 1633 + ' (_ BitVec 1) x)') 1634 elif name == 'WordReverse': 1635 self.send (('(define-fun %s ((x (_ BitVec %d)))' 1636 + ' (_ BitVec %d) (concat %s %s))') 1637 % (fname, n, n, bot_app, top_app)) 1638 else: 1639 assert not True 1640 self.smt_derived_ops[(name, n)] = fname 1641 return fname 1642 1643 # this is how you would test it 1644 num = random.randrange (0, 2 ** n) 1645 clz = len (bin (num + (2 ** n))[3:].split('1')[0]) 1646 assert self.check_hyp_raw ('(= (bvclz_%d %s) %s)' % 1647 (n, smt_num (num, n), smt_num (clz, n))) == 'unsat' 1648 num = num >> random.randrange (0, n) 1649 clz = len (bin (num + (2 ** n))[3:].split('1')[0]) 1650 assert self.check_hyp_raw ('(= (bvclz_%d %s) %s)' % 1651 (n, smt_num (num, n), smt_num (clz, n))) == 'unsat' 1652 1653 def cache_large_expr (self, s, name, typ): 1654 if s in self.cached_exprs: 1655 return self.cached_exprs[s] 1656 if len (s) < 80: 1657 return s 1658 name2 = self.add_def (name, mk_smt_expr (s, typ), {}) 1659 self.cached_exprs[s] = name2 1660 self.cached_exprs[(name2, 'IsCachedExpr')] = True 1661 return name2 1662 1663 def note_ptr (self, p_s): 1664 if p_s in self.ptrs: 1665 p = self.ptrs[p_s] 1666 else: 1667 p = self.add_def ('ptr', mk_smt_expr (p_s, word32T), {}) 1668 self.ptrs[p_s] = p 1669 return p 1670 1671 def add_pvalids (self, htd_s, typ, p_s, kind, recursion = False): 1672 htd_sexp = parse_s_expression (htd_s) 1673 if htd_sexp[0] == 'ite': 1674 [cond, l, r] = map (flat_s_expression, htd_sexp[1:]) 1675 return '(ite %s %s %s)' % (cond, 1676 self.add_pvalids (l, typ, p_s, kind), 1677 self.add_pvalids (r, typ, p_s, kind)) 1678 1679 pvalids = self.pvalids 1680 if htd_s not in pvalids and not recursion: 1681 [_, _, rodata_ptrs] = rodata 1682 if not rodata_ptrs: 1683 rodata_ptrs = [] 1684 for (r_addr, r_typ) in rodata_ptrs: 1685 r_addr_s = smt_expr (r_addr, {}, None) 1686 var = self.add_pvalids (htd_s, ('Type', r_typ), 1687 r_addr_s, 'PGlobalValid', 1688 recursion = True) 1689 self.assert_fact_smt (var) 1690 1691 p = self.note_ptr (p_s) 1692 1693 trace ('adding pvalid with type %s' % (typ, )) 1694 1695 if htd_s in pvalids and (typ, p, kind) in pvalids[htd_s]: 1696 return pvalids[htd_s][(typ, p, kind)] 1697 else: 1698 var = self.add_var ('pvalid', boolT) 1699 pvalids.setdefault (htd_s, {}) 1700 others = pvalids[htd_s].items() 1701 pvalids[htd_s][(typ, p, kind)] = var 1702 1703 def smtify (((typ, p, kind), var)): 1704 return (typ, kind, mk_smt_expr (p, word32T), 1705 mk_smt_expr (var, boolT)) 1706 pdata = smtify (((typ, p, kind), var)) 1707 (_, _, p, pv) = pdata 1708 impl_al = mk_implies (pv, mk_align_valid_ineq (typ, p)) 1709 self.assert_fact (impl_al, {}) 1710 for val in others: 1711 kinds = [val[0][2], pdata[1]] 1712 if ('PWeakValid' in kinds and 1713 'PGlobalValid' not in kinds): 1714 continue 1715 ass = pvalid_assertion1 (pdata, smtify (val)) 1716 ass_s = smt_expr (ass, None, None) 1717 self.assert_fact_smt (ass_s, unsat_tag = 1718 ('PValid', 1, var, val[1])) 1719 ass = pvalid_assertion2 (pdata, smtify (val)) 1720 ass_s = smt_expr (ass, None, None) 1721 self.assert_fact_smt (ass_s, 1722 ('PValid', 2, var, val[1])) 1723 1724 trace ('Now %d related pvalids' % len(pvalids[htd_s])) 1725 return var 1726 1727 def get_imm_basis_mems (self, m, accum): 1728 if m[0] == 'ite': 1729 (_, c, l, r) = m 1730 self.get_imm_basis_mems (l, accum) 1731 self.get_imm_basis_mems (r, accum) 1732 elif m[0] in ['store-word32', 'store-word8']: 1733 (_, m, p, v) = m 1734 self.get_imm_basis_mems (m, accum) 1735 elif type (m) == tuple: 1736 assert not 'mem construction understood', m 1737 elif (m, 'IsCachedExpr') in self.cached_exprs: 1738 self.get_imm_basis_mems (self.defs[m], accum) 1739 else: 1740 assert type (m) == str 1741 accum.add (m) 1742 1743 def get_basis_mems (self, m): 1744 # the obvious implementation requires exponential exploration 1745 # and may overrun the recursion limit. 1746 mems = set () 1747 processed_defs = set () 1748 1749 self.get_imm_basis_mems (m, mems) 1750 while True: 1751 proc = [m for m in mems if m in self.defs 1752 if m not in processed_defs] 1753 if not proc: 1754 return mems 1755 for m in proc: 1756 self.get_imm_basis_mems (self.defs[m], mems) 1757 processed_defs.add (m) 1758 1759 def add_split_mem_var (self, addr, nm, typ, mem_name = None): 1760 assert typ == builtinTs['Mem'] 1761 bot_mem = self.add_var (nm + '_bot', typ, mem_name = mem_name) 1762 top_mem = self.add_var (nm + '_top', typ, mem_name = mem_name) 1763 self.stack_eqs[('StackEqImpliesCheck', top_mem)] = None 1764 return ('SplitMem', addr, top_mem, bot_mem) 1765 1766 def add_implies_stack_eq (self, sp, s1, s2, env): 1767 k = ('ImpliesStackEq', sp, s1, s2) 1768 if k in self.stack_eqs: 1769 return self.stack_eqs[k] 1770 1771 addr = self.add_var ('stack-eq-witness', word32T) 1772 self.assert_fact_smt ('(= (bvand %s #x00000003) #x00000000)' 1773 % addr) 1774 sp_smt = smt_expr (sp, env, self) 1775 self.assert_fact_smt ('(bvule %s %s)' % (sp_smt, addr)) 1776 ptr = mk_smt_expr (addr, word32T) 1777 eq = syntax.mk_eq (syntax.mk_memacc (s1, ptr, word32T), 1778 syntax.mk_memacc (s2, ptr, word32T)) 1779 stack_eq = self.add_def ('stack-eq', eq, env) 1780 self.stack_eqs[k] = stack_eq 1781 return stack_eq 1782 1783 def get_stack_eq_implies (self, split, st_top, other): 1784 if other[0] == 'SplitMem': 1785 [_, split2, top2, bot2] = other 1786 rhs = top2 1787 cond = '(bvule %s %s)' % (split2, split) 1788 else: 1789 rhs = other 1790 cond = 'true' 1791 self.note_model_expr ('(= %s %s)' % (st_top, rhs), boolT) 1792 mems = set () 1793 self.get_imm_basis_mems (parse_s_expression (st_top), mems) 1794 assert len (mems) == 1, mems 1795 [st_top_base] = list (mems) 1796 k = ('StackEqImpliesCheck', st_top_base) 1797 assert k in self.stack_eqs, k 1798 assert self.stack_eqs[k] in [None, rhs], [k, 1799 self.stack_eqs[k], rhs] 1800 self.stack_eqs[k] = rhs 1801 return '(=> %s (= %s %s))' % (cond, st_top, rhs) 1802 1803 def get_token (self, string): 1804 if ('Token', string) not in self.tokens: 1805 n = len (self.tokens) + 1 1806 v = self.add_def ("token_%s" % string, 1807 syntax.mk_num (n, token_smt_typ), {}) 1808 self.tokens[('Token', string)] = v 1809 self.tokens[('Val', self.defs[v])] = string 1810 return self.tokens[('Token', string)] 1811 1812 def note_mem_dom (self, p, d, md): 1813 self.doms.add ((p, d, md)) 1814 1815 def note_model_expr (self, sexpr, typ): 1816 psexpr = parse_s_expression (sexpr) 1817 if psexpr not in self.model_exprs: 1818 s = ''.join ([c for c in sexpr if c not in " ()"]) 1819 s = s[:20] 1820 smt_expr = mk_smt_expr (sexpr, typ) 1821 v = self.add_def ('query_' + s, smt_expr, {}) 1822 self.model_exprs[psexpr] = (v, typ) 1823 1824 def add_pvalid_dom_assertions (self): 1825 if not self.doms: 1826 return 1827 if cheat_mem_doms: 1828 return 1829 dom = iter (self.doms).next ()[1] 1830 1831 pvs = [(var, (p, typ.size ())) 1832 for env in self.pvalids.itervalues () 1833 for ((typ, p, kind), var) in env.iteritems ()] 1834 pvs += [('true', (smt_num (start, 32), (end - start) + 1)) 1835 for (start, end) in sections.itervalues ()] 1836 1837 pvalid_doms = (pvs, set (self.doms)) 1838 if self.pvalid_doms == pvalid_doms: 1839 return 1840 1841 trace ('PValid/Dom complexity: %d, %d' % (len (pvalid_doms[0]), 1842 len (pvalid_doms[1]))) 1843 for (var, (p, sz)) in pvs: 1844 if sz > len (self.doms) * 4: 1845 for (q, _, md) in self.doms: 1846 left = '(bvule %s %s)' % (p, q) 1847 right = ('(bvule %s (bvadd %s %s))' 1848 % (q, p, smt_num (sz - 1, 32))) 1849 lhs = '(and %s %s)' % (left, right) 1850 self.assert_fact_smt ('(=> %s %s)' 1851 % (lhs, md)) 1852 else: 1853 vs = ['(mem-dom (bvadd %s %s) %s)' 1854 % (p, smt_num (i, 32), dom) 1855 for i in range (sz)] 1856 self.assert_fact_smt ('(=> %s (and %s))' 1857 % (var, ' '.join (vs))) 1858 1859 self.pvalid_doms = pvalid_doms 1860 1861 def narrow_unsat_core (self, solver, asserts): 1862 process = subprocess.Popen (solver[1], 1863 stdin = subprocess.PIPE, stdout = subprocess.PIPE, 1864 preexec_fn = preexec (solver[2])) 1865 self.write_solv_script (process.stdin, [], solver = solver, 1866 only_if_is_model = True) 1867 asserts = list (asserts) 1868 for (i, (ass, tag)) in enumerate (asserts): 1869 process.stdin.write ('(assert (! %s :named uc%d))\n' 1870 % (ass, i)) 1871 process.stdin.write ('(check-sat)\n(get-unsat-core)\n') 1872 process.stdin.close () 1873 try: 1874 res = get_s_expression (process.stdout, '(check-sat)') 1875 core = get_s_expression (process.stdout, 1876 '(get-unsat-core)') 1877 except ConversationProblem, e: 1878 return asserts 1879 trace ('got response %r from %s' % (res, solver[0])) 1880 if res != 'unsat': 1881 return asserts 1882 for s in core: 1883 assert s.startswith ('uc') 1884 return set ([asserts[int (s[2:])] for s in core]) 1885 1886 def unsat_core_loop (self, asserts): 1887 asserts = set (asserts) 1888 1889 orig_num_asserts = len (asserts) + 1 1890 while len (asserts) < orig_num_asserts: 1891 orig_num_asserts = len (asserts) 1892 trace ('Entering unsat_core_loop, %d asserts.' 1893 % orig_num_asserts) 1894 for solver in unsat_solver_loop: 1895 asserts = self.narrow_unsat_core (solver, 1896 asserts) 1897 trace (' .. now %d asserts.' % len (asserts)) 1898 return set ([tag for (_, tag) in asserts]) 1899 1900 def unsat_core_with_loop (self, hyps, env): 1901 unsat_core = [] 1902 hyps = [(smt_expr (hyp, env, self), tag) for (hyp, tag) in hyps] 1903 try: 1904 res = self.hyps_sat_raw (hyps, unsat_core = unsat_core) 1905 except ConversationProblem, e: 1906 res = 'unsat' 1907 unsat_core = [] 1908 if res != 'unsat': 1909 return res 1910 if unsat_core == []: 1911 core = list (hyps) + list (self.assertions) 1912 else: 1913 unsat_core = set (unsat_core) 1914 core = [(ass, tag) for (ass, tag) in hyps 1915 if tag in unsat_core] + [(ass, tag) 1916 for (ass, tag) in self.assertions 1917 if tag in unsat_core] 1918 return self.unsat_core_loop (core) 1919 1920def merge_envs (envs, solv): 1921 var_envs = {} 1922 for (pc, env) in envs: 1923 pc_str = smt_expr (pc, env, solv) 1924 for (var, s) in env.iteritems (): 1925 var_envs.setdefault(var, {}) 1926 var_envs[var].setdefault(s, []) 1927 var_envs[var][s].append (pc_str) 1928 1929 env = {} 1930 for var in var_envs: 1931 its = var_envs[var].items() 1932 (v, _) = its[-1] 1933 for i in range(len(its) - 1): 1934 (v2, pc_strs) = its[i] 1935 if len (pc_strs) > 1: 1936 pc_str = '(or %s)' % (' '.join (pc_strs)) 1937 else: 1938 pc_str = pc_strs[0] 1939 v = smt_ifthenelse (pc_str, v2, v, solv) 1940 env[var] = v 1941 return env 1942 1943def fold_assoc_balanced (f, xs): 1944 if len (xs) >= 4: 1945 i = len (xs) / 2 1946 lhs = fold_assoc_balanced (f, xs[:i]) 1947 rhs = fold_assoc_balanced (f, xs[i:]) 1948 return f (lhs, rhs) 1949 else: 1950 return foldr1 (f, xs) 1951 1952def merge_envs_pcs (pc_envs, solv): 1953 pc_envs = [(pc, env) for (pc, env) in pc_envs if pc != false_term] 1954 if pc_envs == []: 1955 path_cond = false_term 1956 else: 1957 pcs = list (set ([pc for (pc, _) in pc_envs])) 1958 path_cond = fold_assoc_balanced (mk_or, pcs) 1959 env = merge_envs (pc_envs, solv) 1960 1961 return (path_cond, env, len (pc_envs) > 1) 1962 1963def hash_test_hyp (solv, hyp, env, cache): 1964 assert hyp.typ == boolT 1965 s = smt_expr (hyp, env, solv) 1966 if s in cache: 1967 return cache[s] 1968 v = solv.test_hyp (mk_smt_expr (s, boolT), {}) 1969 cache[s] = v 1970 return v 1971 1972def hash_test_hyp_fast (solv, hyp, env, cache): 1973 assert hyp.typ == boolT 1974 s = smt_expr (hyp, env, solv) 1975 return cache.get (s) 1976 1977paren_re = re.compile (r"(\(|\))") 1978 1979def parse_s_expressions (ss): 1980 bits = [bit for s in ss for split1 in paren_re.split (s) 1981 for bit in split1.split ()] 1982 def group (n): 1983 if bits[n] != '(': 1984 return (n + 1, bits[n]) 1985 xs = [] 1986 n = n + 1 1987 while bits[n] != ')': 1988 (n, x) = group (n) 1989 xs.append (x) 1990 return (n + 1, tuple (xs)) 1991 (n, v) = group (0) 1992 assert n == len (bits), ss 1993 return v 1994 1995def parse_s_expression (s): 1996 return parse_s_expressions ([s]) 1997 1998def smt_to_val (s, toplevel = None): 1999 stores = [] 2000 if len (s) == 3 and s[0] == '_' and s[1][:2] == 'bv': 2001 ln = int (s[2]) 2002 n = int (s[1][2:]) 2003 return syntax.mk_num (n, ln) 2004 elif type (s) == tuple: 2005 assert type (s) != tuple, s 2006 elif s.startswith ('#b'): 2007 return syntax.mk_num (int (s[2:], 2), len (s) - 2) 2008 elif s.startswith ('#x'): 2009 return syntax.mk_num (int (s[2:], 16), (len (s) - 2) * 4) 2010 elif s == 'true': 2011 return true_term 2012 elif s == 'false': 2013 return false_term 2014 assert not 'smt_to_val: smt expr understood', s 2015 2016last_primitive_model = [0] 2017 2018def eval_mem_name_sexp (m, defs, sexp): 2019 import search 2020 while True: 2021 if sexp[0] == 'ite': 2022 (_, c, l, r) = sexp 2023 b = search.eval_model (m, c) 2024 if b == syntax.true_term: 2025 sexp = l 2026 elif b == syntax.false_term: 2027 sexp = r 2028 else: 2029 assert not 'eval_model result understood' 2030 elif sexp[0] == 'store-word32': 2031 (_, sexp, p2, v2) = sexp 2032 else: 2033 assert type (sexp) == str 2034 if sexp in defs: 2035 sexp = defs[sexp] 2036 else: 2037 return sexp 2038 2039def eval_mem_names (m, defs, mem_names): 2040 init_mem_names = {} 2041 for (m_var, naming) in mem_names.iteritems (): 2042 if type (naming) == tuple: 2043 (nm, sexp) = naming 2044 pred = eval_mem_name_sexp (m, defs, sexp) 2045 init_mem_names[m_var] = (nm, pred) 2046 elif type (naming) == str: 2047 m[m_var] = ((naming, ), {}) 2048 else: 2049 assert not 'naming kind understood', naming 2050 stack = init_mem_names.keys () 2051 while stack: 2052 m_var = stack.pop () 2053 if m_var in m: 2054 continue 2055 (nm, pred) = init_mem_names[m_var] 2056 if pred in m: 2057 (pred_chain, _) = m[pred] 2058 m[m_var] = (pred_chain + (nm,), {}) 2059 else: 2060 stack.extend ([m_var, pred]) 2061 2062def make_model (sexp, m, abbrvs = [], mem_defs = {}): 2063 last_primitive_model[0] = (sexp, abbrvs) 2064 m_pre = {} 2065 try: 2066 for (nm, v) in sexp: 2067 if type (nm) == tuple and type (v) == tuple: 2068 return False 2069 m_pre[nm] = smt_to_val (v) 2070 for (abbrv_sexp, nm) in abbrvs: 2071 if nm in m_pre: 2072 m_pre[abbrv_sexp] = m_pre[nm] 2073 except IndexError, e: 2074 print 'Error with make_model' 2075 print sexp 2076 raise e 2077 # only commit to adjusting m now we know we'll succeed 2078 m.update (m_pre) 2079 last_10_models.append (m_pre) 2080 last_10_models[:-10] = [] 2081 return True 2082 2083def get_model_hyps (model, solv): 2084 return ['(= %s %s)' % (flat_s_expression (x), smt_expr (v, {}, solv)) 2085 for (x, v) in model.iteritems () 2086 if x != ('IsIncomplete', None)] 2087 2088def add_key_model_vs (sexpr, m, solv, vs): 2089 if sexpr[0] == '=>': 2090 (_, lhs, rhs) = sexpr 2091 add_key_model_vs (('or', ('not', lhs), rhs), m, solv, vs) 2092 elif sexpr[0] == 'or': 2093 vals = [(x, get_model_val (x, m)) for x in sexpr[1:]] 2094 true_vals = [x for (x, v) in vals if v == syntax.true_term] 2095 if not true_vals: 2096 for x in sexpr[1:]: 2097 add_key_model_vs (x, m, solv, vs) 2098 elif len (true_vals) == 1: 2099 add_key_model_vs (true_vals[0], m, solv, vs) 2100 else: 2101 vs.add (sexpr) 2102 elif sexpr[0] == 'and': 2103 vals = [(x, get_model_val (x, m)) for x in sexpr[1:]] 2104 false_vals = [x for (x, v) in vals if v == syntax.false_term] 2105 if not false_vals: 2106 for x in sexpr[1:]: 2107 add_key_model_vs (x, m, solv, vs) 2108 elif len (false_vals) == 1: 2109 add_key_model_vs (false_vals[0], m, solv, vs) 2110 else: 2111 vs.add (sexpr) 2112 elif sexpr[0] == 'ite': 2113 (_, p, x, y) = sexpr 2114 v = get_model_val (p, m) 2115 add_key_model_vs (p, m, solv, vs) 2116 if v == syntax.true_term: 2117 add_key_model_vs (x, m, solv, vs) 2118 if v == syntax.false_term: 2119 add_key_model_vs (y, m, solv, vs) 2120 elif type (sexpr) == str: 2121 if sexpr not in vs: 2122 vs.add (sexpr) 2123 if sexpr in solv.defs: 2124 add_key_model_vs (solv.defs[sexpr], m, solv, vs) 2125 else: 2126 for x in sexpr[1:]: 2127 add_key_model_vs (x, m, solv, vs) 2128 2129def get_model_val (sexpr, m, toplevel = None): 2130 import search 2131 try: 2132 return search.eval_model (m, sexpr) 2133 except AssertionError, e: 2134 # this is awful, but happens sometimes because we're 2135 # evaluating in incomplete models 2136 return None 2137 2138last_model_to_reduce = [0] 2139 2140def reduce_model (m, solv, hyps): 2141 last_model_to_reduce[0] = (m, solv, hyps) 2142 vs = set () 2143 for hyp in hyps: 2144 add_key_model_vs (hyp, m, solv, vs) 2145 return dict ([(k, m[k]) for k in m if k in vs]) 2146 2147def flat_s_expression (s): 2148 if type(s) == tuple: 2149 return '(' + ' '.join (map (flat_s_expression, s)) + ')' 2150 else: 2151 return s 2152 2153pvalid_type_map = {} 2154 2155def fun_cond_test (fun, unsats = None): 2156 if unsats == None: 2157 unsats = [] 2158 ns = [n for n in fun.reachable_nodes (simplify = True) 2159 if fun.nodes[n].get_conts ()[1:] == ['Err'] 2160 if fun.nodes[n].cond != syntax.false_term] 2161 if not ns: 2162 return 2163 solv = Solver () 2164 for n in ns: 2165 vs = syntax.get_node_rvals (fun.nodes[n]) 2166 env = dict ([((nm, typ), solv.add_var (nm, typ)) 2167 for (nm, typ) in vs.iteritems ()]) 2168 r = solv.test_hyp (syntax.mk_not (fun.nodes[n].cond), env) 2169 if r == True: 2170 unsats.append ((fun.name, n)) 2171 return unsats 2172 2173def cond_tests (): 2174 unsats = [] 2175 from target_objects import functions 2176 [fun_cond_test (fun, unsats) for (f, fun) in functions.iteritems ()] 2177 assert not unsats, unsats 2178 2179#def compile_struct_pvalid (): 2180#def compile_pvalids (): 2181def quick_test (force_solv = False): 2182 """quick test that the solver supports the needed features.""" 2183 fs = force_solv 2184 solv = Solver () 2185 solv.assert_fact (true_term, {}) 2186 assert solv.check_hyp (false_term, {}, force_solv = fs) == 'sat' 2187 assert solv.check_hyp (true_term, {}, force_solv = fs) == 'unsat' 2188 v = syntax.mk_var ('v', word32T) 2189 z = syntax.mk_word32 (0) 2190 env = {('v', word32T): solv.add_var ('v', word32T)} 2191 solv.assert_fact (syntax.mk_eq (v, z), env) 2192 m = {} 2193 assert solv.check_hyp (false_term, {}, model = m, 2194 force_solv = fs) == 'sat' 2195 assert m.get ('v') == z, m 2196 2197def test (): 2198 solverlist = find_solverlist_file () 2199 print 'Loaded solver list from %s' % solverlist 2200 quick_test () 2201 quick_test (force_solv = 'Slow') 2202 print 'Solver self-test successful' 2203 2204if __name__ == "__main__": 2205 import sys, target_objects 2206 if sys.argv[1:] == ['testq']: 2207 target_objects.tracer[0] = lambda x, y: () 2208 test () 2209 elif sys.argv[1:] == ['test']: 2210 test () 2211 elif sys.argv[1:] == ['ctest']: 2212 cond_tests () 2213 2214 2215