Browse files

Added some network libraries and bit twiddling

  • Loading branch information...
1 parent 3b14e79 commit 1ede34ed14df41f1a64c930acca8a373822199b3 Edwin Brady committed May 27, 2011
Showing with 949 additions and 0 deletions.
  1. +7 −0 Makefile
  2. +434 −0 bittwiddle.c
  3. +67 −0 bittwiddle.h
  4. +306 −0 bittwiddle.idr
  5. +85 −0 bounded.idr
  6. +50 −0 so_what.idr
View
7 Makefile
@@ -0,0 +1,7 @@
+CFLAGS = -g `epic -includedirs`
+
+go: bittwiddle.o
+ idris ResIO.idr
+
+bittwiddle.o: bittwiddle.h bittwiddle.c
+
View
434 bittwiddle.c
@@ -0,0 +1,434 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/types.h>
+#include <sys/socket.h>
+#include <netinet/in.h>
+#include <arpa/inet.h>
+#include <netdb.h>
+#include <unistd.h>
+#include <fcntl.h>
+#include <errno.h>
+
+#include <bittwiddle.h>
+#include <closure.h>
+
+PACKET newPacket(int length) {
+ int words = length >> 5;
+ if ((length & 31)!=0) words++; // Need one more if it's not exactly aligned
+// printf("%d words\n", words);
+ PACKET p = EMALLOC(words*sizeof(word32));
+ memset(p, words*sizeof(word32), 0);
+ return p;
+}
+
+void dump_binary(int x)
+{
+ unsigned int z, i;
+ for (z = 1 << 31, i=1; z > 0; z >>= 1, i++)
+ {
+ putchar(((x & z) == z) ? '1' : '0');
+ if (i%8==0) putchar(' ');
+ }
+}
+
+void dumpPacket(PACKET p, int length) {
+ int i;
+ int words = length >> 5;
+ if ((length & 31)!=0) words++; // Need one more if it's not exactly aligned
+
+ for (i=0; i<words; ++i) {
+ printf("%x \t", p[i]);
+ dump_binary(p[i]);
+ printf("\n");
+ }
+ printf("\n");
+}
+
+word32 setnbits(word32 v, int startoff, int endoff, int data) {
+// printf("Setting %d, %d to %d\n", startoff, endoff, data);
+// printf("%x\n", v);
+ // Clear the bits in v from startoff to endoff.
+ word32 two_m = (0xffffffff << (32-startoff)) ^ 0xffffffff;
+ word32 two_n = (0xffffffff << (32-endoff)) ^ 0xffffffff;
+
+ // Right, (two_m - two_n) is now ones in the position we want to clear.
+ // So, flip it, to make it zeros we want to clear, ones elsewhere,
+ // then AND v with it to pick out the bits we want to keep.
+
+ v = v & ((two_m - two_n) ^ 0xffffffff);
+
+ // Put the data in the right place (from startbit to endbit, all other
+ // bits zero).
+ word32 nv = data << (32-endoff);
+
+// printf("%x\n", nv);
+// printf("%x\n", v | nv);
+
+ // Put nv in the right place in v.
+ return (v | nv);
+}
+
+
+
+word32 getnbits(word32 v, int startbit, int endbit) {
+// printf("Getting %d, %d\n", startbit, endbit);
+ return (v << startbit) >> (startbit + (32-endbit));
+}
+
+void setPacketByte(PACKET p, int b, int data) {
+ p[b] = data;
+}
+
+void setPacketBits(PACKET p, int start, int end, int data) {
+ int startb = start >> 5; // Word the start bits are in
+ int endb = end >> 5; // Word the end bits are in
+
+ int startoff = start & 31; // Offset of start bits in that word
+ int endoff = (end & 31)+1; // Offset of end bits in that word
+
+ if (startb==endb) { // In the same word, easy...
+ p[startb] = setnbits(p[startb], startoff, endoff, data);
+ } else {
+ // Set the least significant 32-[startoff] bits of p[startb] to
+ // [data] >> [endoff].
+ p[startb] = setnbits(p[startb], startoff, 32, data >> endoff);
+
+ // Set the most significant [endoff] bits of p[endb] to the least
+ // significant [endoff] bits of [data].
+ p[endb] = setnbits(p[endb], 0, endoff,
+ (data << (32 - endoff)) >> (32 - endoff));
+ }
+}
+
+void setPacketString(PACKET p, int start, char* s, int l, char t) {
+ int i;
+ while(*s!=t && (l!=0)) {
+ setPacketBits(p, start, start+7, (int)(*s));
+ start+=8;
+ ++s;
+ --l;
+ }
+}
+
+int getPacketByte(PACKET p, int b) {
+ return p[b];
+}
+
+int getPacketBits(PACKET p, int start, int end) {
+ int startb = start >> 5; // Word the start bits are in
+ int endb = end >> 5; // Word the end bits are in
+
+ int startoff = start & 31; // Offset of start bits in that word
+ int endoff = 1 + (end & 31); // Offset of end bits in that word
+ int rv;
+
+ if (startb==endb) {
+ rv = getnbits(p[startb], startoff, endoff);
+ } else {
+ int startn = getnbits(p[startb], startoff, 32);
+ int endn = getnbits(p[endb], 0, endoff);
+ rv = (startn << endoff) + endn;
+ }
+// printf("%d to %d is %d\n", start, end, rv);
+ return rv;
+}
+
+// Now some network code
+
+int isReadable(int sd, int timeOut) { // milliseconds
+ fd_set socketReadSet;
+ FD_ZERO(&socketReadSet);
+ FD_SET(sd,&socketReadSet);
+ struct timeval tv;
+ if (timeOut) {
+ tv.tv_sec = timeOut / 1000;
+ tv.tv_usec = (timeOut % 1000) * 1000;
+ } else {
+ tv.tv_sec = 0;
+ tv.tv_usec = 0;
+ } // if
+ if (select(sd+1,&socketReadSet,0,0,&tv) == -1) {
+ printf("READ ERROR!\n");
+ return 0;
+ } // if
+ return FD_ISSET(sd,&socketReadSet) != 0;
+} /* isReadable */
+
+void* net_UDP_clientSocket(char* server, int port) {
+ Connection* con = (Connection*)EMALLOC(sizeof(Connection));
+ int s;
+ struct sockaddr_in si_me, si_other;
+
+ if ((s=socket(AF_INET, SOCK_DGRAM, 0))==-1) {
+ printf("FAIL 1\n");
+ return NULL;
+ }
+
+ memset((char *) &si_other, 0, sizeof(si_other));
+ si_other.sin_family = AF_INET;
+ si_other.sin_port = htons(port);
+
+ if (inet_aton(server, &si_other.sin_addr)==0) {
+ printf("FAIL 2\n");
+ return NULL;
+ }
+
+ // Bind, so we can receive replies.
+ si_me.sin_family = AF_INET;
+ si_me.sin_port = htons(0);
+ si_me.sin_addr.s_addr = htonl(INADDR_ANY);
+
+ if (bind(s, (struct sockaddr*)&si_me, sizeof(si_me))<0) {
+ return NULL;
+ }
+
+ con->sock = s;
+ con->addr = si_other;
+
+// printf("Opened client socket %d\n", s);
+ return con;
+}
+
+void* net_UDP_serverSocket(int port) {
+ Connection* con = (Connection*)EMALLOC(sizeof(Connection));
+ int s;
+ struct sockaddr_in si_me;
+
+ if ((s=socket(AF_INET, SOCK_DGRAM, 0))==-1) {
+ return NULL;
+ }
+
+ memset((char *) &si_me, 0, sizeof(si_me));
+ si_me.sin_family = AF_INET;
+ si_me.sin_port = htons(port);
+ si_me.sin_addr.s_addr = htonl(INADDR_ANY);
+ if (bind(s, (struct sockaddr*)&si_me, sizeof(si_me))==-1) {
+ return NULL;
+ }
+
+ con->sock = s;
+ con->addr = si_me;
+
+// printf("Opened server socket %d\n", s);
+ return con;
+}
+
+void* net_TCP_socket(char* server, int port) {
+ Connection* con = (Connection*)EMALLOC(sizeof(Connection));
+ int s;
+ struct sockaddr_in addr;
+ struct hostent *hostinfo;
+
+ if ((s=socket(AF_INET, SOCK_STREAM, 0))==-1) {
+ printf("FAIL 1\n");
+ return NULL;
+ }
+
+ hostinfo = gethostbyname(server);
+ if (hostinfo == NULL) {
+ printf("FAIL 2\n");
+ return NULL;
+ }
+ addr.sin_family = AF_INET;
+ addr.sin_addr = *(struct in_addr *)hostinfo->h_addr;
+ addr.sin_port = htons(port);
+
+ if (connect(s, (struct sockaddr *)(&addr),
+ sizeof(struct sockaddr_in)) == -1) {
+ printf("FAIL 3 %s\n", strerror(errno));
+ return NULL;
+ }
+
+ con->sock = s;
+ con->addr = addr;
+
+// printf("Opened client socket %d\n", s);
+ return con;
+}
+
+void* net_TCP_listen(int port, int maxcon)
+{
+ Connection* con = (Connection*)EMALLOC(sizeof(Connection));
+ int sock;
+ struct sockaddr_in name;
+
+ sock = socket(PF_INET, SOCK_STREAM, getprotobyname("tcp")->p_proto);
+ name.sin_family = AF_INET;
+
+/* int val = 1;
+ setsockopt(sock, SOL_SOCKET, SO_REUSEADDR, &val, sizeof(int));
+ fcntl(sock, F_SETFL, O_NONBLOCK);
+*/
+
+ name.sin_port = htons(port);
+ name.sin_addr.s_addr = htonl(INADDR_ANY);
+
+ if (bind(sock, (struct sockaddr *)(&name), sizeof(struct sockaddr_in))) {
+ printf("BIND FAIL\n");
+ return NULL;
+ }
+ if (listen(sock, maxcon)) {
+ printf("LISTEN FAIL\n");
+ return NULL;
+ }
+
+ con->sock = sock;
+ con->addr = name;
+ return con;
+}
+
+void* net_TCP_accept(void* s_in) {
+ Connection* con_in = (Connection*)s_in;
+ Connection* con = (Connection*)EMALLOC(sizeof(Connection));
+
+ struct sockaddr_in addr;
+ socklen_t len = sizeof(struct sockaddr_in);
+
+ int client = accept(con_in->sock, (struct sockaddr*)&addr, &len);
+ if (client==-1) {
+ printf("ACCEPT FAIL\n");
+ return NULL;
+ }
+
+ con->sock = client;
+ con->addr = addr;
+ return (void*)con;
+}
+
+void net_closeSocket(void* s) {
+ close(((Connection*)s)->sock);
+}
+
+
+int net_sendUDP(void* conn, char* server, int port, VAL stuff) {
+ VAL pkt = GETPTR(PROJECT(stuff,0));
+ int len = GETINT(PROJECT(stuff,1));
+ int words = len >> 5;
+ if ((len & 31)!=0) ++words;
+
+ Connection* c = (Connection*)conn;
+ int s = c->sock;
+ struct sockaddr_in other = c->addr;
+ memset((char *) &other, 0, sizeof(other));
+ other.sin_family = AF_INET;
+ other.sin_port = htons(port);
+ if (inet_aton(server, &other.sin_addr)==0) {
+ return -1;
+ }
+
+ if (sendto(s, pkt, words*sizeof(word32), 0, (struct sockaddr*)&other,
+ sizeof(other))==-1) {
+ return -1;
+ }
+ return 0;
+}
+
+void* net_recvUDP(void* conn) {
+ struct sockaddr_in other;
+ Connection* c = (Connection*)conn;
+ int s = c->sock;
+ socklen_t slen = sizeof(other);
+ struct sockaddr_in me = c->addr;
+
+ // TMP HACK: 512 should be enough for the purposes of this experiment...
+ // Do it properly some time.
+ word32* buf = (word32*)EMALLOC(512*sizeof(word32));
+
+// printf("Waiting to receive\n");
+
+ int error;
+// while (!isReadable(s,100)) printf(".\n");
+
+ if (!isReadable(s, 1000)) {
+ printf("Nothing\n");
+ return NULL;
+ }
+
+ int recvlen = recvfrom(s, buf, 512*sizeof(word32), 0, (struct sockaddr *)&other, &slen);
+
+ if (recvlen==-1) {
+ return NULL;
+ }
+
+ printf("Received %d bytes from %s:UDP%u\n",
+ recvlen,inet_ntoa(other.sin_addr),
+ ntohs(other.sin_port));
+
+ Recv* r = (Recv*)EMALLOC(sizeof(Recv));
+ r->buf = CONSTRUCTOR2(0, MKPTR(buf), MKINT(recvlen << 3));
+ r->server = inet_ntoa(other.sin_addr);
+ r->port = ntohs(other.sin_port);
+
+ return (void*)r;
+}
+
+int net_sendTCP(void* conn, VAL stuff) {
+ VAL pkt = GETPTR(PROJECT(stuff,0));
+ int len = GETINT(PROJECT(stuff,1));
+ int words = len >> 5;
+ if ((len & 31)!=0) ++words;
+
+ Connection* c = (Connection*)conn;
+ int s = c->sock;
+
+ if (send(s, pkt, words*sizeof(word32), 0)==-1) {
+ return -1;
+ }
+ return 0;
+}
+
+void* net_recvTCP(void* conn) {
+ Connection* c = (Connection*)conn;
+ int s = c->sock;
+ struct sockaddr_in me = c->addr;
+
+ // TMP HACK: 512 should be enough for the purposes of this experiment...
+ // Do it properly some time.
+ word32* buf = (word32*)EMALLOC(512*sizeof(word32));
+
+// printf("Waiting to receive\n");
+
+ int error;
+// while (!isReadable(s,100)) printf(".\n");
+
+ if (!isReadable(s, 1000)) {
+ printf("Nothing\n");
+ return NULL;
+ }
+
+ int recvlen = recv(s, buf, 512*sizeof(word32), 0);
+
+ if (recvlen==-1) {
+ return NULL;
+ }
+
+ printf("Received %d bytes from %s:%u\n",
+ recvlen,inet_ntoa(me.sin_addr),
+ ntohs(me.sin_port));
+
+ Recv* r = (Recv*)EMALLOC(sizeof(Recv));
+ r->buf = CONSTRUCTOR2(0, MKPTR(buf), MKINT(recvlen << 3));
+ r->server = inet_ntoa(me.sin_addr);
+ r->port = ntohs(me.sin_port);
+
+ return (void*)r;
+}
+
+
+VAL get_recvBuf(void* recv) {
+ return ((Recv*)recv)->buf;
+}
+
+char* get_recvServer(void* recv) {
+ return ((Recv*)recv)->server;
+}
+
+int get_recvPort(void* recv) {
+ return ((Recv*)recv)->port;
+}
+
+int nullPtr(void *ptr) {
+ return ptr==NULL;
+}
+
View
67 bittwiddle.h
@@ -0,0 +1,67 @@
+#ifndef _BITTWIDDLE_H
+#define _BITTWIDDLE_H
+
+#include <stdint.h>
+#include <closure.h>
+#include <sys/types.h>
+#include <sys/socket.h>
+#include <netinet/in.h>
+#include <arpa/inet.h>
+#include <unistd.h>
+#include <fcntl.h>
+#include <errno.h>
+
+typedef uint32_t word32;
+
+///////// Packet data
+
+typedef word32* PACKET;
+
+PACKET newPacket(int length);
+void dumpPacket(PACKET p, int length);
+
+void setPacketByte(PACKET p, int b, int data);
+void setPacketBits(PACKET p, int start, int end, int data);
+
+void setPacketString(PACKET p, int start, char* string, int l, char t);
+
+int getPacketByte(PACKET p, int b);
+int getPacketBits(PACKET p, int start, int end);
+
+//// Code for sending packets across a wire
+
+// Anything waiting on a socket?
+int isReadable(int sd, int timeOut);
+
+typedef struct {
+ int sock;
+ struct sockaddr_in addr;
+} Connection;
+
+typedef struct {
+ VAL buf;
+ unsigned port;
+ char* server;
+} Recv;
+
+// Open sockets
+void* net_UDP_serverSocket(int port);
+void* net_UDP_clientSocket(char* server, int port);
+void* net_TCP_socket(char* server, int port);
+void* net_TCP_listen(int port, int maxcon);
+void* net_TCP_accept(void* s_in);
+void net_closeSocket(void* s);
+
+int net_sendUDP(void* conn, char* server, int port, VAL stuff);
+void* net_recvUDP(void* conn);
+
+int net_sendTCP(void* conn, VAL stuff);
+void* net_recvTCP(void* conn);
+
+VAL get_recvPacket(void* recv);
+char* get_recvServer(void* recv);
+int get_recvPort(void* recv);
+
+int nullPtr(void *ptr);
+
+#endif
View
306 bittwiddle.idr
@@ -0,0 +1,306 @@
+include "so_what.idr";
+include "bounded.idr";
+
+%include "bittwiddle.h"
+%lib "bittwiddle.o"
+
+-- First, the primitive versions using unsafe C call evilness.
+
+data RawPacket = RPkt Ptr Int;
+
+f_newPacket = mkForeign (FFun "newPacket"
+ (Cons FInt Nil) FPtr); [%eval]
+f_dumpPacket = mkForeign (FFun "dumpPacket"
+ (Cons FPtr (Cons FInt Nil)) FUnit); [%eval]
+f_setPacketBits = mkForeign (FFun "setPacketBits"
+ (Cons FPtr (Cons FInt (Cons FInt (Cons FInt Nil))))
+ FUnit); [%eval]
+f_getPacketBits = mkForeign (FFun "getPacketBits"
+ (Cons FPtr (Cons FInt (Cons FInt Nil)))
+ FInt); [%eval]
+
+f_setPacketString = mkForeign (FFun "setPacketString"
+ (Cons FPtr (Cons FInt (Cons FStr
+ (Cons FInt (Cons FInt Nil)))))
+ FUnit); [%eval]
+
+newPacket : Int -> IO RawPacket;
+newPacket l = do { p <- f_newPacket l;
+ return (RPkt p l); };
+
+dumpPacket : RawPacket -> IO ();
+dumpPacket (RPkt p l) = f_dumpPacket p l;
+
+setPacketBits : RawPacket -> Int -> Int -> Int -> IO ();
+setPacketBits (RPkt p l) s e dat = f_setPacketBits p s e dat;
+
+getPacketBits : RawPacket -> Int -> Int -> IO Int;
+getPacketBits (RPkt p l) s e = f_getPacketBits p s e;
+
+-- Yes, it's just 'elem'. Need type classes...
+
+validOption : Int -> List Int -> Bool;
+validOption x Nil = False;
+validOption x (Cons y ys) = if x==y then True else (validOption x ys);
+
+
+
+data Option : Int -> List Int -> Set where
+ Opt : (x:Bounded w) -> (so (validOption (value x) xs)) -> Option w xs;
+
+ovalue : Option i xs -> Int;
+ovalue (Opt (BInt v _) _) = v;
+
+bvalue : Option i xs -> Bounded i;
+bvalue (Opt b _) = b;
+
+getField : RawPacket -> (start:Int) -> (end:Int) -> so (end>=start) ->
+ Maybe (Bounded (1 << (end-start)));
+getField (RPkt pkt len) start end _
+ = if ((start<=len) && (end<=len)) then
+ (Just
+ (BInt (unsafePerformIO (getPacketBits (RPkt pkt len) start (end-1)))
+ (unsafeCoerce oh))) -- It's from C, we need to trust it...
+ else Nothing;
+
+-- These really need proofs that there is space in the packet rep. It's okay
+-- if we go through the DSL interface though.
+
+setField : RawPacket -> (start:Int) -> (end:Int) ->
+ Bounded (1 << (end-start)) -> IO ();
+setField pkt start end (BInt v _) = setPacketBits pkt start (end-1) v;
+
+setString : RawPacket -> (start:Int) -> String -> IO ();
+setString (RPkt pkt len) start v = f_setPacketString pkt start v (-1) 0;
+
+setStringn : RawPacket -> (start:Int) -> String -> Int -> IO ();
+setStringn (RPkt pkt len) start v slen
+ = f_setPacketString pkt start v slen 0;
+
+-- Maybe better as a primitive in C?
+
+getString' : RawPacket -> Int -> String -> Maybe String;
+getString' pkt pos acc with getField pkt pos (pos+8) (ltAdd 8 oh) {
+ | Just vin = let v = value vin in
+ if (v==0) then (Just (strRev acc)) else
+ (getString' pkt (pos+8) (strCons (__intToChar v) acc));
+ | Nothing = Nothing;
+}
+
+getString : RawPacket -> Int -> Maybe String;
+getString pkt pos = getString' pkt pos "";
+
+getStringn' : RawPacket -> Int -> String -> Nat -> Maybe String;
+getStringn' pkt pos acc (S k) with getField pkt pos (pos+8) (ltAdd 8 oh) {
+ | Just vin = let v = value vin in
+ if (v==0) then (Just (strRev acc)) else
+ (getStringn' pkt (pos+8) (strCons (__intToChar v) acc) k);
+ | Nothing = Nothing;
+}
+getStringn' pkt pos acc O = Just (strRev acc);
+
+getStringn : RawPacket -> Int -> Int -> Maybe String;
+getStringn pkt pos len = getStringn' pkt pos "" (intToNat len);
+
+{-
+getTextString' : RawPacket -> Int -> Int -> String -> Maybe String;
+getTextString' pkt pos prev acc with getField pkt pos (pos+8) (ltAdd 8 oh) {
+ | Just vin = let v = value vin in
+ let end = prev=='\r' && v == '\n')foo in
+ let newstr = strCons (__intToChar v) acc in
+ if end then (Just (strRev newstr)) else
+ (getTextString' pkt (pos+8) v newstr);
+
+ if (v=='\n') then (Just (strRev acc)) else
+ (getTextString' pkt (pos+8) v (strCons (__intToChar v) acc));
+ | Nothing = Nothing;
+}
+
+getTextString : RawPacket -> Int -> Maybe String;
+getTextString pkt pos = getTextString' pkt pos 0 "";
+-}
+
+boundFin : Bounded (1 << (natToInt x)) -> Fin (power (S (S O)) (S x));
+
+-- This arises from some C, which we can't prove anything about...
+-- so we'll just have to trust it.
+
+{-
+so_it_is proof {
+ %intro;
+ %refine __Prove_Anything;
+ %qed;
+};
+-}
+
+-- Some networking glue
+
+f_clientSocket = mkForeign (FFun "net_UDP_clientSocket"
+ (Cons FStr (Cons FInt Nil)) FPtr); [%eval]
+f_serverSocket = mkForeign (FFun "net_UDP_serverSocket"
+ (Cons FInt Nil) FPtr); [%eval]
+f_tcpSocket = mkForeign (FFun "net_TCP_socket"
+ (Cons FStr (Cons FInt Nil)) FPtr); [%eval]
+f_tcpListen = mkForeign (FFun "net_TCP_listen"
+ (Cons FInt (Cons FInt Nil)) FPtr); [%eval]
+f_tcpAccept = mkForeign (FFun "net_TCP_accept"
+ (Cons FPtr Nil) FPtr); [%eval]
+f_closeSocket = mkForeign (FFun "net_closeSocket"
+ (Cons FPtr Nil) FUnit); [%eval]
+
+
+f_sendUDP = mkForeign (FFun "net_sendUDP"
+ (Cons FPtr (Cons FStr (Cons FInt (Cons (FAny RawPacket) Nil))))
+ FInt); [%eval]
+f_recvUDP = mkForeign (FFun "net_recvUDP"
+ (Cons FPtr Nil) FPtr); [%eval]
+
+f_sendTCP = mkForeign (FFun "net_sendTCP"
+ (Cons FPtr (Cons (FAny RawPacket) Nil))
+ FInt); [%eval]
+f_recvTCP = mkForeign (FFun "net_recvTCP"
+ (Cons FPtr Nil) FPtr); [%eval]
+
+f_recvBuf = mkForeign (FFun "get_recvBuf"
+ (Cons FPtr Nil) (FAny RawPacket)); [%eval]
+f_recvServer = mkForeign (FFun "get_recvServer"
+ (Cons FPtr Nil) FStr); [%eval]
+f_recvPort = mkForeign (FFun "get_recvPort"
+ (Cons FPtr Nil) FInt); [%eval]
+
+f_nullPtr = mkForeign (FFun "nullPtr" (Cons FPtr Nil) FInt); [%eval]
+
+nullPtr : Ptr -> Bool;
+nullPtr ptr = unsafePerformIO (
+ do { p <- f_nullPtr ptr;
+ return (if_then_else (p==1) True False);
+ });
+
+data Socket = mkCon Ptr | noCon;
+
+data Recv = mkRecv RawPacket String Int;
+
+getRawPacket : Recv -> RawPacket;
+getRawPacket (mkRecv pkt _ _) = pkt;
+
+-- FIXME: Opening a socket might fail! Will return a null pointer if so.
+
+clientSocket : String -> Int -> IO Socket;
+clientSocket server port = do {
+ sock <- f_clientSocket server port;
+ if (nullPtr sock) then (return noCon) else
+ (return (mkCon sock)); };
+
+serverSocket : Int -> IO Socket;
+serverSocket port = do {
+ sock <- f_serverSocket port;
+ if (nullPtr sock) then (return noCon) else
+ (return (mkCon sock)); };
+
+TCPConnect : String -> Int -> IO Socket;
+TCPConnect server port = do {
+ sock <- f_tcpSocket server port;
+ if (nullPtr sock) then (return noCon) else
+ (return (mkCon sock)); };
+
+TCPListen : Int -> Int -> IO Socket;
+TCPListen port maxcon = do {
+ sock <- f_tcpListen port maxcon;
+ if (nullPtr sock) then (return noCon) else
+ (return (mkCon sock)); };
+
+TCPAccept : Socket -> IO Socket;
+TCPAccept noCon = return noCon;
+TCPAccept (mkCon s) = do {
+ sock <- f_tcpAccept s;
+ if (nullPtr sock) then (return noCon) else
+ (return (mkCon sock)); };
+
+closeSocket : Socket -> IO ();
+closeSocket noCon = return II;
+closeSocket (mkCon s) = f_closeSocket s;
+
+sendTo : Socket -> String -> Int -> RawPacket -> IO ();
+sendTo noCon _ _ _ = return II;
+sendTo (mkCon c) server port dat
+ = do { v <- f_sendUDP c server port dat;
+ return II; };
+
+doMkRecv : Bool -> Ptr -> IO (Maybe Recv);
+doMkRecv True _ = return Nothing;
+doMkRecv False rcv = do {
+ buf <- f_recvBuf rcv;
+ server <- f_recvServer rcv;
+ port <- f_recvPort rcv;
+ return (Just (mkRecv buf server port));
+};
+
+recvFrom : Socket -> IO (Maybe Recv);
+recvFrom noCon = return Nothing;
+recvFrom (mkCon c) = do {
+ rcv <- f_recvUDP c;
+ doMkRecv (nullPtr rcv) rcv;
+};
+
+send : Socket -> RawPacket -> IO ();
+send noCon dat = return II;
+send (mkCon c) dat = do { v <- f_sendTCP c dat;
+ return II; };
+
+recv : Socket -> IO (Maybe Recv);
+recv noCon = return Nothing;
+recv (mkCon c) = do {
+ rcv <- f_recvTCP c;
+ doMkRecv (nullPtr rcv) rcv;
+};
+
+{-
+x = 20;
+y = 64;
+
+main : IO ();
+main = do { putStrLn (showInt (x << 2));
+ putStrLn (showInt (y >> 3));
+ };
+-}
+
+{-
+
+-- Fin version, abandonded...
+
+Word = \n => Fin (power (S (S O)) n);
+Word32 = Word (intToNat 32);
+
+-- Given an n+m+p bit number, pull out the m bits in the middle.
+-- (i.e. call getBits' with n and m-1). We know that getBits' returns
+-- a number with the right bounds, but it's external so we'll have to
+-- cheat with the type!
+
+getBits : (n:Nat) -> (m:Nat) ->
+ Word (plus (plus n m) p) ->
+ Word m;
+getBits n m num with getBits' (mkInt32 (finToInt num))
+ (natToInt n) ((natToInt m)-1) {
+ | x ?= intToFin (getInt32 x); [getBitsHack]
+}
+
+setBits : (n:Nat) -> (m:Nat) ->
+ Word (plus (plus n m) p) ->
+ Word m ->
+ Word (plus (plus n m) p);
+setBits n m num newnum with setBits' (mkInt32 (finToInt num))
+ (natToInt n) ((natToInt m)-1)
+ (finToInt newnum) {
+ | x ?= intToFin (getInt32 x); [setBitsHack]
+}
+
+-- We can do this as long as the external C code is correct. (Uh oh...)
+getBitsHack proof {
+ %intro; %believe value; %qed;
+};
+
+setBitsHack proof {
+ %intro; %believe value; %qed;
+};
+
+-}
View
85 bounded.idr
@@ -0,0 +1,85 @@
+include "so_what.idr";
+
+-- Idris doesn't have unsigned integers, which would make this easier.
+-- We assume here that Int just means unsigned.
+-- TODO: Add Unsigned ints (call it 'Word'?)
+
+Unsigned = Int; -- HACK :)
+
+data Bounded : Int -> Set where
+ BInt : (x:Unsigned) -> (so (x<i)) -> Bounded i;
+
+syntax bounded x = BInt x [ tryproof %intro; %decide isThatSo; %qed ];
+
+value : Bounded i -> Unsigned; [inline]
+value (BInt v _) = v;
+
+boundProof : (b:Bounded i) -> so ((value b) < i);
+boundProof (BInt _ p) = p;
+
+charToBounded : Char -> Bounded 256;
+charToBounded x = BInt (__charToInt x) (__Prove_Anything _ _ oh); -- Of course it is ;)
+
+Word : Unsigned -> Set;
+Word n = Bounded (1 << n);
+
+infixl 8 :+: ;
+infixl 6 :<:, :<=:, :>:, :>=: ;
+
+-- modulo addition
+
+mod_bound : Unsigned -> Bounded n;
+mod_bound {n} x = BInt (mod x n) (__Prove_Anything _ _ oh); -- guaranteed by %
+
+(:+:) : Bounded n -> Bounded n -> Bounded n;
+(:+:) x y = mod_bound (value x + value y);
+
+blift : (Unsigned -> Unsigned -> Bool) -> Bounded n -> Bounded m -> Bool;
+blift op x y = op (value x) (value y);
+
+(:<:) : Bounded n -> Bounded m -> Bool;
+(:<:) = blift (<) ;
+
+(:<=:) : Bounded n -> Bounded m -> Bool;
+(:<=:) = blift (<=) ;
+
+(:>:) : Bounded n -> Bounded m -> Bool;
+(:>:) = blift (>) ;
+
+(:>=:) : Bounded n -> Bounded m -> Bool;
+(:>=:) = blift (>=) ;
+
+data Window : (seq_width:Unsigned) -> Set where
+ MkWin : Word n -> Word n -> Window n;
+
+using (bottom: Word n, top : Word n, x : Word n) {
+
+ data InWindow : Word n -> Window n -> Set where
+ InNormal : (so (bottom :<: top)) -> -- no wrap around
+ (so (x :>: bottom && x :<=: top)) ->
+ (InWindow x (MkWin bottom top))
+ | InWrapped : (so (bottom :>=: top)) -> -- must have wrapped
+ (so (x :<=: top || x :>: bottom)) ->
+ (InWindow x (MkWin bottom top));
+}
+
+advance : (old: Window n) -> (last_ack : Word n) -> (win_size : Word n) ->
+ InWindow last_ack old -> Window n;
+advance (MkWin bottom top) last_ack win_size p
+ = MkWin (last_ack :+: BInt 1 ?adv1) (last_ack :+: BInt 1 ?adv2 :+: win_size);
+
+{-- some cheating is required again because we don't have unsigned ints!
+ These are okay under the assumption that we never use a negative n in
+ Word n and Window n --}
+
+adv1 proof {
+ %intro;
+ %fill (__Prove_Anything _ _ oh);
+ %qed;
+};
+
+adv2 proof {
+ %intro;
+ %fill (__Prove_Anything _ _ oh);
+ %qed;
+};
View
50 so_what.idr
@@ -0,0 +1,50 @@
+
+-- Some proofs about primitive operations - we just have to trust these.
+
+-- Not that this is actually true if x+y overflows! Whole thing works
+-- under the assumption that it doesn't.
+
+ltAdd : (y:Int) -> (so (y>0)) -> so (x+y >= x);
+ltAdd y = __Prove_Anything _ _ oh;
+
+addSub : (x:Int) -> (y:Int) -> (x = ((y + x) - y));
+addSub x y = __Suspend_Disbelief ((y+x)-y) x;
+
+check : (T:Bool) -> Either (so T) (so (not T));
+check True = Left oh;
+check False = Right oh;
+
+unsafeCoerce : {a:Set} -> {b:Set} -> a -> b;
+unsafeCoerce a ?= a; [doCoerce]
+
+doCoerce proof {
+ %intro;
+ %rewrite __Suspend_Disbelief X0 X;
+ %refine value;
+ %qed;
+};
+
+isThatSo : (x:Bool) -> Tactic;
+isThatSo x = TTry (TFill oh)
+ (TTry TTrivial
+ (TFail "Not so!"));
+
+so_and : so x -> so y -> so (x && y);
+so_and oh oh = oh;
+
+so_orL : so x -> so (x || y);
+so_orL oh = oh;
+
+so_orR : so x -> so (y || x);
+so_orR oh = ?do_so_orR;
+do_so_orR proof {
+ %intro x;
+ %rewrite <- or_commutes x True;
+ %refine oh;
+ %qed;
+};
+
+syntax mk_so = [tryproof %intro; %decide isThatSo; %qed];
+syntax bounded x = BInt x mk_so;
+
+

0 comments on commit 1ede34e

Please sign in to comment.