on master help sign in
Merge pull request #3429 from jfdm/fail-when-ffi-is-partial-applied

Make C codegen fail more.

commitc8303b2c8c60acf7230ef8c8c657c00b2e6c43f3 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateFri 16 Sep 2016, 07:47 (10 years ago) parentdad4d42b9a7352
8 files changed+154−8
src/IRTS/CodegenC.hs+1 test/TestData.hs+10−8 test/ffi009/Bad.idr+36 test/ffi009/Good.idr+37 test/ffi009/expected+1 test/ffi009/ffi009.c+44 test/ffi009/ffi009.h+20 test/ffi009/run+5
src/IRTS/CodegenC.hs+1
@@ -340,6 +340,7 @@ bcc i (FOREIGNCALL l rty (FStr fn) args)
340340 = indent i ++
341341 c_irts (toFType rty) (creg l ++ " = ")
342342 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
343+bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."
343344bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
344345bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
345346-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
test/TestData.hs+10−8
@@ -114,14 +114,16 @@ testFamiliesData = [
114114 ( 8, ANY ),
115115 ( 9, ANY )]),
116116 ("ffi", "FFI",
117− [ ( 1, ANY ),
118− ( 2, ANY ),
119− ( 3, ANY ),
120− ( 4, ANY ),
121− ( 5, ANY ),
122− ( 6, C_CG ),
123− ( 7, C_CG ),
124− ( 8, C_CG )]),
117+ [ ( 1, ANY )
118+ , ( 2, ANY )
119+ , ( 3, ANY )
120+ , ( 4, ANY )
121+ , ( 5, ANY )
122+ , ( 6, C_CG )
123+ , ( 7, C_CG )
124+ , ( 8, C_CG )
125+ , ( 9, C_CG )
126+ ]),
125127 ("folding", "Folding",
126128 [ ( 1, ANY )]),
127129 ("idrisdoc", "Idris documentation",
test/ffi009/Bad.idrnew file+36
@@ -0,0 +1,36 @@
1+module Bad
2+
3+%include c "ffi009.h"
4+
5+private
6+get_allocation_size : Ptr -> IO Int
7+get_allocation_size = foreign FFI_C "get_allocation_size" (Ptr -> IO Int)
8+
9+-- [ NOTE ]
10+--
11+-- As `commen_call` is a partial function and not inline, Idris should complain.
12+
13+private
14+common_call : String -> Int -> IO ManagedPtr
15+common_call f l = do
16+ ptr <- foreign FFI_C
17+ f
18+ (Int -> IO Ptr)
19+ l
20+ len <- get_allocation_size ptr
21+ pure (prim__registerPtr ptr len)
22+
23+func_foo : IO ManagedPtr
24+func_foo = common_call "foo" 4
25+
26+func_bar : IO ManagedPtr
27+func_bar = common_call "bar" 8
28+
29+
30+namespace Main
31+ main : IO ()
32+ main = do
33+ foo <- func_foo
34+ bar <- func_bar
35+
36+ printLn "I should not be seen."
test/ffi009/Good.idrnew file+37
@@ -0,0 +1,37 @@
1+module Good
2+
3+%include c "ffi009.h"
4+
5+private
6+get_allocation_size : Ptr -> IO Int
7+get_allocation_size = foreign FFI_C "get_allocation_size" (Ptr -> IO Int)
8+
9+-- [ NOTE ]
10+--
11+-- As `commen_call` is a partial function and not inline, Idris should complain.
12+
13+private
14+%inline
15+common_call : String -> Int -> IO ManagedPtr
16+common_call f l = do
17+ ptr <- foreign FFI_C
18+ f
19+ (Int -> IO Ptr)
20+ l
21+ len <- get_allocation_size ptr
22+ pure (prim__registerPtr ptr len)
23+
24+func_foo : IO ManagedPtr
25+func_foo = common_call "foo" 4
26+
27+func_bar : IO ManagedPtr
28+func_bar = common_call "bar" 8
29+
30+
31+namespace Main
32+ main : IO ()
33+ main = do
34+ foo <- func_foo
35+ bar <- func_bar
36+
37+ printLn "I should be seen."
test/ffi009/expectednew file+1
@@ -0,0 +1 @@
1+"I should be seen."
test/ffi009/ffi009.cnew file+44
@@ -0,0 +1,44 @@
1+#include "ffi009.h"
2+
3+
4+Vect* foo(int length)
5+{
6+ return new_empty_vect(length);
7+}
8+
9+Vect* bar(int length)
10+{
11+ return new_empty_vect(length * 2);
12+}
13+
14+
15+Vect* new_empty_vect(int l)
16+{
17+ unsigned char* vect;
18+
19+ vect = malloc(sizeof(unsigned char) * l);
20+
21+ if (vect == NULL){
22+ free(vect);
23+ return NULL;
24+ }
25+
26+ Vect* v = malloc(sizeof(Vect));
27+
28+ if (v==NULL){
29+ free(vect);
30+ free(v);
31+ return NULL;
32+ }
33+
34+ v->value = vect;
35+ v->length = l;
36+
37+ return v;
38+}
39+
40+
41+int get_allocation_size(Vect* v)
42+{
43+ return sizeof(Vect) + v->length;
44+}
test/ffi009/ffi009.hnew file+20
@@ -0,0 +1,20 @@
1+#ifndef FFI009_H
2+#define FFI009_H
3+
4+#include <idris_rts.h>
5+
6+
7+typedef struct
8+{
9+ unsigned char* value;
10+ int length;
11+} Vect;
12+
13+int get_allocation_size(Vect* v);
14+
15+Vect* new_empty_vect(int length);
16+
17+Vect* foo(int length);
18+Vect* bar(int length);
19+
20+#endif /* FFI009_H */
test/ffi009/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ Bad.idr -o bad --cg-opt "ffi009.c" --cg-opt "-fno-strict-overflow"
3+${IDRIS:-idris} $@ Good.idr -o good --cg-opt "ffi009.c"
4+./good
5+rm -f *.ibc good