GaloisInc / ivory

The Ivory EDSL
http://ivorylang.org
BSD 3-Clause "New" or "Revised" License
393 stars 28 forks source link

Function pointer casting #83

Closed cblp closed 7 years ago

cblp commented 8 years ago

I'm trying to call a procedure and pass it a pointer to another procedure via some generic interface. In real life it may be qsort or any other procedure with callback. Here is a simplified example.

In C it works like so:

typedef void (* fun_t)(void *);

void print(uint32_t * p) {
    printf("%u\n", *p);
}

void apply(fun_t f, void * x) {
    f(x);
}

apply((fun_t)print, 42);

(checked with gcc -Wall -Wextra -Werror -ansi -pedantic)

Let's reproduce this in Ivory!

print :: Def ('[ConstRef s ('Stored Uint32)] ':-> ())
print = proc "print" $ \x -> body $
    call_ printf "%u\n" =<< deref x

type Fun s = ProcPtr ('[ConstRef s ('Stored Uint32)] ':-> ())

apply :: Def ('[Fun s, ConstRef s ('Stored Uint32)] ':-> ())
apply = proc "apply" $ \f x -> body $
    indirect_ f x

cmain :: Def ('[] ':-> Sint32)
cmain = proc "main" $ body $ do
    str <- local $ ival 42
    call_ apply (procPtr print) (constRef str)
    ret 0

Works good with concrete type uint32_t. Now let's generalize it to void *.

-- print proc is the same

type GenericRef s = ConstRef s ('Stored ())
type GenericFun s = ProcPtr ('[GenericRef s] ':-> ())

apply :: Def ('[GenericFun s, GenericRef s] ':-> ())
apply = proc "apply" $ \f x -> body $
    indirect_ f x

But we can't call_ apply (procPtr print) (constRef str), because Haskell can't unify Uint32 in print's type and () in apply's type.

In C we used type cast to solve this problem. Can we cast these types in Haskell/Ivory language?

We can't use safeCast, because there are no SafeCast instances for anything like pointer types. Looks like casting pointers in considered unsafe. Seem rational.

Let's try unsafe ivoryCast.

call_ apply (ivoryCast (procPtr print)) (ivoryCast str)

The cast for str works, but the first one throws an error:

No instance for (IvoryExpr (GenericFun s0))
    arising from a use of ‘ivoryCast’
In the second argument of ‘call_’, namely
    ‘(ivoryCast (procPtr print))’
In a stmt of a 'do' block:
    call_ apply (ivoryCast (procPtr print)) (ivoryCast str)
In the second argument of ‘($)’, namely
    ‘do { str <- local (ival 42 :: Init (Stored Uint32));
          call_ apply (ivoryCast (procPtr print)) (ivoryCast str);
          ret 0 }’

There is no IvoryExpr instance for ProcPtr!

Why? Because, unlike majority of Ivory types, ProcPtr is not a wrapper around Expr and so cannot be constructed by wrapping around Expr.

A strange thing

Under some assumptions, we can cast to a secondary function pointer in Ivory.

Assumption 1. Make apply function external.

apply :: Def ('[GenericFun s, GenericRef s] ':-> ())
apply = importProc "apply" "apply.h"

(Unfortunately, we can't implement it in Ivory, because there is no instance of IvoryStore neither for Def nor for ProcPtr.)

Assumption 2. Relax requirements of ivoryCast.

ivoryCast' :: forall a b . (IvoryVar a, IvoryExpr b) => a -> b
ivoryCast' x = wrapExpr (ExpSafeCast ty (unwrapExpr x))
  where ty = ivoryType (Proxy :: Proxy a)

Now we can use pointers to function pointers!

type GenericFun s = Ref s ('Stored (ProcPtr ('[GenericRef s] ':-> ())))

And Ivory generates the following code:

apply((void (**)(const void *)) print, (const void *) n_ref1);

The result is incorrect, but the IvoryExpr instance works as expected!

Is primary function pointer cast impossible in Ivory when the secondary one is possible?

cblp commented 8 years ago

The main question is: how to write type-safe generic C procedure calling passed in procedure via a type-erasured function pointer?

acfoltzer commented 8 years ago

@cblp thank you for bringing this up; this issue goes a bit deeper so it might be a while until we can hammer out a good design. (cc @elliottt @leepike)

leepike commented 8 years ago

FYI: associated pull request from @cblp: https://github.com/GaloisInc/ivory/pull/84

leepike commented 7 years ago

I believe this behavior is technically undefined behavior in C (e.g., see this StackOverflow question). Since we have proposed for Ivory to produce only well-defined C programs (when statically checkable), we should probably omit function pointer casts.