Symbolic Execution

se.rb

# https://github.com/taw/z3
# A Peer Architecture for Lightweight Symbolic Execution
require 'z3'
require 'ruby_parser'
parser = RubyParser.new
class Checker
  def initialize(eval_mode: true)
    @solver = Z3::Solver.new
    @eval_mode = eval_mode
  end

  def eval_expr(s, env)
    # p eval:s if @eval_mode
    case s
    in Sexp[:lit, value] then value
    in Sexp[:lvar, x] then env.fetch(x)
    in Sexp[:call, nil, :puts, x] then puts(eval_expr(x, env))
    in Sexp[:call, nil, :symbol, x] then Z3.Int(x.to_s)
    in Sexp[:call, nil, :assert, x] then assert(eval_expr(x, env))
    in Sexp[:call, nil, :assume, x] then raise NotImplementedError
    # in Sexp[:call, nil, x] then env.fetch(x)
    in Sexp[:call, nil, f, *xs] then
      binding = env[f][1].zip(xs.map { |e| eval_expr(e, env) }).to_h
      eval_expr(env[f][2], env[f][3].merge(binding))
    in Sexp[:call, x, op] then eval_expr(x, env).send(op)
    in Sexp[:call, x, op, y] then eval_expr(x, env).send(op, eval_expr(y, env))
    in Sexp[:while, x, *ys] then ys.each { |e| eval_expr(e, env) } while condition(eval_expr(x, env))
    in Sexp[:if, x, y, z] then condition(eval_expr(x, env)) ? eval_expr(y, env) : eval_expr(z, env)
    in Sexp[:lasgn, x, y] then env[x] = eval_expr(y, env)
    in Sexp[:block, *xs] then xs.map { |x| eval_expr(x, env) }.last
    in Sexp[:defn, f, Sexp[:args, *xs], *ys] then env[f] = [:lambda, xs, Sexp[:block, *ys], env]
    in true|false|nil then s
    else raise "expr is #{s.inspect}"
    end
  end

  class DepthException < StandardError
  end

  def check(expr, env = {})
    pp expr
    @path = []
    loop do
      @path_condition = []
      begin
        result = eval_expr(expr, env.dup)
      rescue DepthException => e
        puts e
      rescue AssertFail => e
        p e
        return counterexample.to_h { |k, v| [k.to_s.intern, v.to_i] }
      end
      @path.pop until @path.empty? || @path[-1]
      return if @path.empty?

      @path[-1] = false
    end
    nil
  end

  def solve(expr)
    @solver.reset
    @solver.assert(expr)
    @solver.satisfiable?
  end

  def counterexample
    @solver.reset
    @solver.assert(!@path_condition.inject(&:&))
    @solver.satisfiable? ? @solver.model : nil
  end

  def assert(formula)
    raise AssertFail, @path_condition unless condition(formula)

    # return solve(!(@path_condition + [formula]).inject(&:&))
  end

  class AssertFail < StandardError; end

  def condition(formula)
    return formula if @eval_mode

    if true
      truecond = solve((@path_condition + [formula]).inject(&:&))
      falsecond = solve((@path_condition + [!formula]).inject(&:&))
      return true if truecond && !falsecond
      return false if falsecond && !truecond
    end
    if @path_condition.length < @path.length
      branch = @path[@path_condition.length]
      @path_condition << (branch ? formula : !formula)
      return branch
    end

    raise DepthException, 'Depth exceeded' if @path.length >= 10

    @path << true
    @path_condition << formula
    true
  end
end

cc = Checker.new

cc.eval_expr(parser.parse('1+1'), {}) == 2 or raise
# cc.eval_expr(parser.parse('1+x;'), { x: Z3.Int('x') }).is_a?(Z3::IntExpr) or raise
p cc.eval_expr(parser.parse('def f(x);y=x;y+2;end;f(1)'), {})
p cc.eval_expr(parser.parse('def f(x)=x+3;f(1)'), {})
# p cc.eval_expr(code, {})
cc = Checker.new(eval_mode: false)
p  r1: cc.check(parser.parse('x=symbol(:x);if x<0 then x=-x end; assert x>=-1 ;x'))
p  r2: cc.check(parser.parse('x=symbol(:x);if x<0 then x=-x end; assert x>=0 ;x'))
p  r3: cc.check(parser.parse('x=symbol(:x);if x<0 then x=-x end; assert x>=1 ;x'))