git.iko.soy/Idris-dev
on master help sign in
Start high level C FFI support
commit6bf2318c1a2f86d836c3bf4aa9af3e0c17986a38 authorNiklas Larsson <niklas@mm.st> dateSat 13 Feb 2016, 18:45 (11 years ago) parent504187b
10 files changed+235−2
compare with master
unifiedsplit
libs/contrib/CFFI.idr+4 libs/contrib/CFFI/Memory.idr+48 libs/contrib/CFFI/Types.idr+96 libs/contrib/Data/HList.idr+13 libs/contrib/contrib.ipkg+4−2 test/ffi008/expected test/ffi008/ffi008.c+9 test/ffi008/ffi008.h+14 test/ffi008/ffi008.idr+43 test/ffi008/run+4
libs/contrib/CFFI.idrnew file+4
@@ -0,0 +1,4 @@
1+module CFFI
2+
3+import public CFFI.Types
4+import public CFFI.Memory
libs/contrib/CFFI/Memory.idrnew file+48
@@ -0,0 +1,48 @@
1+||| Machinery for interfacing with C.
2+module CFFI.Memory
3+
4+import CFFI.Types
5+
6+%include C "memory.h"
7+
8+%access public export
9+%default partial
10+
11+data CPtr = CPt Ptr Int CType
12+
13+malloc : Int -> IO Ptr
14+malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
15+
16+mfree : Ptr -> IO ()
17+mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
18+
19+alloc : CType -> IO CPtr
20+alloc t = return $ CPt !(malloc (sizeOf t)) 0 t
21+
22+free : CPtr -> IO ()
23+free (CPt p _ _) = mfree p
24+
25+ctype : CPtr -> CType
26+ctype (CPt _ _ t) = t
27+
28+get : (p : CPtr) -> IO (translate (ctype p))
29+get (CPt p o I8) = prim_peek8 p o
30+get (CPt p o I16) = prim_peek16 p o
31+get (CPt p o I32) = prim_peek32 p o
32+get (CPt p o I64) = prim_peek64 p o
33+get (CPt p o FLOAT) = prim_peek32 p o
34+get (CPt p o DOUBLE) = cast $ prim_peek64 p o
35+get (CPt p o PTR) = prim_peekPtr p o
36+
37+
38+put : (p : CPtr) -> (translate (ctype p)) -> IO ()
39+put _ _ = putStrLn "putting"
40+
41+-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
42+
43+field : CPtr -> (i : Nat) -> CPtr
44+field (Cpt p o arr@(ARRAY n t)) = CPt p (o + index i (offsets arr)) t
45+field (Cpt p o (UNION xs)) = CPt p o (index i xs)
46+field (Cpt p o st@(STRUCT xs)) = CPt p (o + index i (offsets st)) (index i xs)
47+field (Cpt p o ps@(PACKEDSTRUCT xs)) = CPt p (o + index i (offsets st)) (index i xs)
48+field p Z = p
libs/contrib/CFFI/Types.idrnew file+96
@@ -0,0 +1,96 @@
1+||| Types for interfacing with C.
2+module CFFI.Types
3+
4+import Data.Vect
5+import Data.HList
6+
7+%access public export
8+%default partial
9+
10+||| An universe of C types.
11+data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
12+ | ARRAY Int CType | STRUCT (List CType) | UNION (List CType)
13+ | PACKEDSTRUCT (List CType)
14+
15+translate : CType -> Type
16+translate I8 = Bits8
17+translate I16 = Bits16
18+translate I32 = Bits32
19+translate I64 = Bits64
20+translate FLOAT = Bits32
21+translate DOUBLE = Double
22+translate PTR = Ptr
23+translate (ARRAY n t) = Vect (toNat n) (translate t)
24+translate (STRUCT xs) = HList (map translate xs)
25+translate (UNION xs) = HList (map translate xs)
26+translate (PACKEDSTRUCT xs) = HList (map translate xs)
27+
28+mutual
29+ sizeOf : CType -> Int
30+ sizeOf I8 = 1
31+ sizeOf I16 = 2
32+ sizeOf I32 = 4
33+ sizeOf I64 = 8
34+ sizeOf FLOAT = 4
35+ sizeOf DOUBLE = 8
36+ sizeOf PTR = prim__sizeofPtr
37+ sizeOf (ARRAY n t) = n * sizeOf t
38+ sizeOf (STRUCT xs) = sizeOfStruct xs
39+ sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
40+ sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
41+
42+ alignOf : CType -> Int
43+ alignOf I8 = 1
44+ alignOf I16 = 2
45+ alignOf I32 = 4
46+ alignOf I64 = prim__sizeofPtr
47+ alignOf FLOAT = 4
48+ alignOf DOUBLE = prim__sizeofPtr
49+ alignOf PTR = prim__sizeofPtr
50+ alignOf (ARRAY n t) = alignOf t
51+ alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
52+ alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
53+ alignOf (PACKEDSTRUCT xs) = 1
54+
55+ offsetsStruct : List CType -> List Int
56+ offsetsStruct xs = offsets' xs [] 0
57+ where
58+ offsets' : List CType -> List Int -> Int -> List Int
59+ offsets' [] acc _ = reverse acc
60+ offsets' (x::xs) ys curr = let a = alignOf x
61+ padding = let c = curr `mod` a
62+ in if c == 0 then 0 else a - c
63+ off = curr + padding
64+ in offsets' xs (off::ys) (off + sizeOf x)
65+
66+ sizeOfStruct : List CType -> Int
67+ sizeOfStruct xs = case (reverse xs, reverse (offsetsStruct xs)) of
68+ ([], _) => 0
69+ (x::_, y::_) => let end = y + sizeOf x
70+ endPadding = let c = end `mod` align in
71+ if c == 0 then 0 else align - c
72+ in end + endPadding
73+ where
74+ align : Int
75+ align = foldl (\acc, x => max acc $ alignOf x) 1 xs
76+
77+fields : CType -> Nat
78+fields (STRUCT xs) = length xs
79+fields (PACKEDSTRUCT xs) = length xs
80+fields (UNION xs) = length xs
81+fields (ARRAY n _) = toNat n
82+fields _ = 1
83+
84+offsetsPacked : List CType -> List Int
85+offsetsPacked xs = offsets' xs [] 0
86+ where
87+ offsets' : List CType -> List Int -> Int -> List Int
88+ offsets' [] acc _ = reverse acc
89+ offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
90+
91+offsets : CType -> List Int
92+offsets (STRUCT xs) = offsetsStruct xs
93+offsets (PACKEDSTRUCT xs) = offsetsPacked xs
94+offsets (UNION xs) = replicate (length xs) 0
95+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n]]
96+offsets _ = [0]
libs/contrib/Data/HList.idrnew file+13
@@ -0,0 +1,13 @@
1+||| A heterogenous list
2+module Data.HList
3+
4+%access public export
5+
6+data HList : List Type -> Type where
7+ Nil : HList []
8+ (::) : a -> HList xs -> HList (a :: xs)
9+
10+||| Extract an element from an HList
11+index : (i : Nat) -> HList ts -> {auto ok : InBounds i ts } -> List.index i ts
12+index Z (x::xs) {ok} = x
13+index (S j) (x::xs) {ok = InLater p}= index j xs
libs/contrib/contrib.ipkg+4−2
@@ -1,7 +1,9 @@
11package contrib
22
33opts = "--nobasepkgs --total -i ../prelude -i ../base"
4−modules = Control.Algebra,
4+modules = CFFI, CFFI.Types, CFFI.Memory,
5+
6+ Control.Algebra,
57 Control.Algebra.Lattice, Control.Algebra.VectorSpace,
68 Control.Algebra.NumericInstances,
79 Control.Isomorphism.Primitives,
@@ -11,7 +13,7 @@ modules = Control.Algebra,
1113 Classes.Verified,
1214
1315 Data.Fun, Data.Rel,
14− Data.Hash,
16+ Data.Hash, Data.HList,
1517 Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,
1618 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,
1719 Data.ZZ, Data.Sign,
test/ffi008/expectednew file

No changes to the content.

test/ffi008/ffi008.cnew file+9
@@ -0,0 +1,9 @@
1+#include "ffi008.h"
2+
3+int size1(void) {
4+ return sizeof(struct test1);
5+}
6+
7+int size2(void) {
8+ return sizeof(struct test2);
9+}
test/ffi008/ffi008.hnew file+14
@@ -0,0 +1,14 @@
1+#include <stdint.h>
2+
3+struct test1 {
4+ int8_t a;
5+ int64_t b;
6+};
7+
8+struct test2 {
9+ int32_t a;
10+ int16_t b;
11+};
12+
13+int size1(void);
14+int size2(void);
test/ffi008/ffi008.idrnew file+43
@@ -0,0 +1,43 @@
1+module Main
2+
3+import CFFI
4+import Data.Vect
5+
6+%include C "ffi008.h"
7+
8+size1 : IO Int
9+size1 = foreign FFI_C "size1" (IO Int)
10+
11+
12+size2 : IO Int
13+size2 = foreign FFI_C "size2" (IO Int)
14+
15+test1 : CType
16+test1 = STRUCT [I8, I64]
17+
18+test2 : CType
19+test2 = STRUCT [I32, I16]
20+
21+test3 : CType
22+test3 = STRUCT [I8, I8, I8, I64]
23+
24+test4 : CType
25+test4 = PACKEDSTRUCT [I8, I8, I8, I64]
26+
27+printMore : IO ()
28+printMore = do
29+ p <- alloc I8
30+ a <- get p
31+ free p
32+ printLn !size1
33+ printLn !size2
34+ printLn $ fields test3
35+ printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
36+ printLn $ sizeOf (ARRAY 67 I32)
37+ printLn $ sizeOf test3
38+
39+main : IO ()
40+main = do
41+ printLn $ sizeOf test1 == !size1
42+ printLn $ sizeOf test2 == !size2
43+ printMore
test/ffi008/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ ffi008.idr -o ffi008 -p contrib --cg-opt "ffi008.c"
3+./ffi008
4+rm -f ffi008 *.ibc