Blogofbrew

home

Teaching Ruby to Program Itself

21 Apr 2015

Thanks to everyone who attended my April 2015 Iowa Ruby Brigade talk. These are my notes, source code is here.

##How to call C from Ruby

Easymode, call your C binary from the shell in Ruby

print `echo Just use backticks`

Call your Ruby code fom C

#include "ruby.h"
int main(int argc, char **argv) { 
  VALUE result;
  ruby_sysinit(&argc, &argv);
  RUBY_INIT_STACK;
  ruby_init();
  ruby_init_loadpath();
  rb_eval_string("x = 3*4") ;
  result = rb_gv_get("x");
  printf("Result = %d\n", NUM2INT(result));
  return ruby_cleanup(0);
}

How to write Ruby extensions in C

#Example C extension, fib-example

MyFib.c

#include "ruby.h"

VALUE method_fib(VALUE self, VALUE arg1) {
        int x = 33;
        return INT2NUM(x);
}

void Init_myfib() {
	VALUE MyFib = rb_define_module("MyFib");
	rb_define_method(MyFib, "fib", method_fib, 1);	
}

extconf.rb

require 'mkmf'

ext_name = 'MyFib'

dir_config(ext_name)

create_makefile(ext_name)

myfibDriver.rb

#myfib.rb
require 'MyFib/myfib'
include MyFib
puts fib(777777)

Compiling and running the C extension

ruby extconf.rb
make
ruby myfibDriver.rb
# outputs 33

Compiling CRuby with code coverage

git clone https://github.com/ruby/ruby.git
cd ruby
brew install openssl 

(optional) uncomment #option nodynamic in ruby/ext/Setup

mkdir ~/.rubies
CFLAGS='--coverage -g -O0 -Wall' LDFLAGS='--coverage'   ./configure --prefix=/Users/crb002/.rubies/ruby-trunk --with-openssl-dir=/usr/local/opt/openssl
make
make test
make test-all
#make test-all TESTS="csv/"

Pretty printing coverage for C

brew install lcov
lcov --capture --directory ./  --output-file coverage.info
genhtml coverage.info --output-directory coveragehtml

Raw code coverage in Ruby

#Raw ruby coverage using Coverage
require "coverage.so"
Coverage.start
#run your code
p Coverage.result

Simplecov for pretty-print coverage in Ruby

require 'simplecov'
SimpleCov.start

How to call the z3 SMT solver with SMT-LIB2 syntax

z3 -smt2 problem.smt

An example SMT-LIB2 program

(declare-const p Bool) ;Declaring a constant function
(declare-const q Bool)
(declare-const r Bool)
(define-fun conjecture () Bool  ;Declaring a function which returns a Bool 
	(=> (and (=> p q) (=> q r))
		(=> p r)))
(assert (not conjecture))
(check-sat)

Key concept. Constants in SMT-LIB are functions which take no arguments.

IF THEN ELSE in Ruby

if(a and b)
	return 37
else
   return 24
end

IF THEN ELSE in SMT-LIB

(ite (and a b) 37 24)

Printing in SMT-LIB

(display (+ 1 2 3))  ;(+ 1 2 3)

Simplifying expressions in SMT-LIB

(declare-const x Int)
(simplify (+ x 2 x 1)) ; (+ 3 (* 2 x)) 

Project Euler problem 4, find the largest palindrome made from the product of two 3-digit numbers.

;Code by Craig Stuntz 2014
(declare-const product Int)
(declare-const factor1 Int)
(declare-const factor2 Int)
(assert (and >= factor 100) (< factor1 1000)) ;Ensure 3 digits
(assert (and >= factor 100) (< factor1 1000))
(assert (= (* factor1 factor2) product))
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (and (>= a 8)  (<= a 9)) )
(assert (and (>= b 0)  (<= b 9)) )
(assert (and (>= c 0)  (<= c 9)) )
; Asssert that the product is a palendrome
(assert (= product (+ (* 100000  a)  (* 10000  b)  (* 1000  c) (* 100  c)  (* 10 b) a )))
(maximize (+ factor1 factor2)) ; Hack since Z3 doesn't maximize products yet
(check-sat)
(get-model)

;(+ factor1 factor2) |-> 1906
;sat
; (model
; ...
; (define-fun factor1 () Int 913)
; (define-fun factor2 () Int 993)
; (define-fun product () Int 906609)
; )

SMT-LIB Tutorial with Z3

#Putting it all together to test Fizz-Buzz-Jaberwocky

def fizbuzz(num)
   case
   when num % 15 == 0 then "FizzBuzz"
   when num % 5 == 0 then "Fizz"
   when num % 3 == 0 then "Buzz"
   when ((num % 13 == 7) and (num > 300) and (num % 7 == 0))  then "Jaberwocky"
   else num
   end
end

#Synopsys.

Test before you code.

Run your tests with code coverage.

Use Z3 as a bench calculator to help fill testing gaps.

Build a CRuby binary with code coverage to see the low level hot spots in your app.

Other links:

SMT-LIB language

Z3 SMT Solver

Concolic Testing

My reading picks for this summer:

Conceptual Mathematics: A First Introduction to Categories

Real World OCaml

Your Code as a Crime Scene