Monday, 20 May 2013

"warning: Invalid parameter passed to C runtime function."

What a frustrating thing to see an error message "warning: Invalid parameter passed to C runtime function." in debugger window without any notice, what does it mean.

I wasn't able to google any useful information, so "I'm just going to leave this here" for those who also stuck at it.

The message "Invalid parameter passed to C runtime function." is being dumped into debugger in msvcrt.dll function __invoke_watson(), using well-known OutputDebugStringA().

Well, this can be easily seen using IDA disassembler. But how we can trace, what was a reason to signal this error? Especially when debugging MinGW-compiled win32-binary in GDB debugger? Just set breakpoint at OutputDebugStringA function (typing break OutputDebugStringA) and then dump your stack (typing bt).

In may case, my program was passing NULL parameter to strcmp() function located in msvcrt.dll, so that's why it (fairly) signalled about error.

Friday, 10 May 2013

Solving Problem Euler 31 - "Coin sums" using Z3 SMT-solver

In England the currency is made up of pound, £, and pence, p, and there are eight coins in general circulation: 1p, 2p, 5p, 10p, 20p, 50p, £1 (100p) and £2 (200p). It is possible to make £2 in the following way: 1£1 + 150p + 220p + 15p + 12p + 31p How many different ways can £2 be made using any number of coins?
Problem Euler 31 - Coin sums

Using MSR Z3 SMT solver for solving this is overkill, and also slow, but nevertheless, it works, showing all possible solutions as well. The piece of code for blocking already found solution and search for next, and thus, counting all solutions, was taken from here.

Constraints like "a>=0" should be present, because Z3 solver will search for solutions with negative numbers.
#!/usr/bin/python

from z3 import *

a,b,c,d,e,f,g,h = Ints('a b c d e f g h')
s = Solver()
s.add(1*a + 2*b + 5*c + 10*d + 20*e + 50*f + 100*g + 200*h == 200, 
   a>=0, b>=0, c>=0, d>=0, e>=0, f>=0, g>=0, h>=0)
result=[]

while True:
    if s.check() == sat:
        m = s.model()
        print m
        result.append(m)
        # Create a new constraint the blocks the current model
        block = []
        for d in m:
            # d is a declaration
            if d.arity() > 0:
                raise Z3Exception("uninterpreted functions are not suppported")
            # create a constant from declaration
            c=d()
            #print c, m[d]
            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                raise Z3Exception("arrays and uninterpreted sorts are not supported")
            block.append(c != m[d])
        #print "new constraint:",block
        s.add(Or(block))
    else:
            print len(result)
            break
Works very slow, and this is what it produces:
[h = 0, g = 0, f = 0, e = 0, d = 0, c = 0, b = 0, a = 200]
[f = 1, b = 5, a = 0, d = 1, g = 1, h = 0, c = 2, e = 1]
[f = 0, b = 1, a = 153, d = 0, g = 0, h = 0, c = 1, e = 2]
...
[f = 0, b = 31, a = 33, d = 2, g = 0, h = 0, c = 17, e = 0]
[f = 0, b = 30, a = 35, d = 2, g = 0, h = 0, c = 17, e = 0]
[f = 0, b = 5, a = 50, d = 2, g = 0, h = 0, c = 24, e = 0]
73682 results in total.