Test env to develop FILO filesystem drivers in Ada
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..c4a847d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/result
diff --git a/default.adc b/default.adc
new file mode 100644
index 0000000..c4a1e03
--- /dev/null
+++ b/default.adc
@@ -0,0 +1 @@
+pragma SPARK_Mode (On);
diff --git a/default.gpr b/default.gpr
new file mode 100644
index 0000000..7437fd5
--- /dev/null
+++ b/default.gpr
@@ -0,0 +1,14 @@
+project Default is
+
+ for Main use ("main");
+ for Source_Dirs use ("src");
+
+ package Builder is
+ for Global_Configuration_Pragmas use "default.adc";
+ end Builder;
+
+ package Compiler is
+ for Switches ("Ada") use ("-gnat2022");
+ end Compiler;
+
+end Default;
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..6cb0bac
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,40 @@
+with import <nixpkgs> { };
+
+stdenv.mkDerivation rec {
+ pname = "spark_fs_drivers";
+ version = "0.0.0";
+
+ src = ./.;
+
+ nativeBuildInputs = [
+ gnat
+ gprbuild
+ spark2014
+ z3
+ ];
+
+ gprFile = "default.gpr";
+
+ dontConfigure = true;
+
+ buildPhase = ''
+ runHook preBuild
+
+ gprbuild -P ${gprFile}
+ gnatprove -P ${gprFile} --prover=z3
+
+ runHook postBuild
+ '';
+
+ installPhase = ''
+ runHook preInstall
+
+ mkdir -p $out/bin
+ gprinstall --prefix=$out ${gprFile} \
+ --no-project \
+ --no-manifest \
+ --mode=usage
+
+ runHook postInstall
+ '';
+}
diff --git a/src/a.out b/src/a.out
new file mode 100755
index 0000000..f410633
--- /dev/null
+++ b/src/a.out
Binary files differ
diff --git a/src/fs-filo.adb b/src/fs-filo.adb
new file mode 100644
index 0000000..3280b34
--- /dev/null
+++ b/src/fs-filo.adb
@@ -0,0 +1,22 @@
+package body FS.FILO is
+
+ procedure Read
+ (Buffer : in out Buffer_Type;
+ Offset : in Natural;
+ Bytes_Read: out Natural)
+ is
+ Sector_Size : constant Natural := 512;
+ Sector : constant Interfaces.C.unsigned_long := Offset / Sector_Size;
+ Byte_Offset : constant Interfaces.C.unsigned_long := Offset rem Sector_Size;
+ Byte_Len : constant Interfaces.C.unsigned_long := Buffer'Length;
+ begin
+
+ Bytes_Read := C_devread
+ (sector => Sector,
+ byte_offset => Byte_Offset,
+ byte_len => Byte_Len,
+ buf => Buffer'Address);
+ end Read;
+
+end FS.FILO;
+
diff --git a/src/fs-filo.ads b/src/fs-filo.ads
new file mode 100644
index 0000000..43b6cef
--- /dev/null
+++ b/src/fs-filo.ads
@@ -0,0 +1,31 @@
+with Interfaces.C;
+
+package FS.FILO is
+
+ Procedure Read
+ (Buffer : in out Buffer_Type;
+ Offset : in Natural;
+ Success : out Boolean);
+
+private
+
+ function C_devread
+ (sector : Interfaces.C.unsigned_long;
+ byte_offset : Interfaces.C.unsigned_long;
+ byte_len : Interfaces.C.unsigned_long;
+ buf : ... )
+ return Interfaces.C.int
+ with
+ SPARK_Mode => Off,
+ Import => True,
+ Conversion => C;
+
+
+end FS.FILO;
+
+
+
+-- int mount (void)
+-- int read (char* buf, int len)
+-- int dir (char *dirname)
+-- void close (void) // not implemented
diff --git a/src/fs.ads b/src/fs.ads
new file mode 100644
index 0000000..3ea5a69
--- /dev/null
+++ b/src/fs.ads
@@ -0,0 +1,5 @@
+package FS is
+
+ type Buffer is array (Natural range <>) of Unsigned_8;
+
+end FS;
diff --git a/src/fs.c b/src/fs.c
new file mode 100644
index 0000000..271662a
--- /dev/null
+++ b/src/fs.c
@@ -0,0 +1,62 @@
+
+#include <stdio.h>
+
+#include "fs.h"
+
+FILE* block_device = NULL
+size_t device_size = 0;
+
+
+int devopen(const char* name, int* reopen)
+{
+ block_device = fopen(name, "rwb");
+ if (!block_device) {
+ return 0;
+ }
+ fseek(block_device, 0, SEEK_END)
+ return 1;
+}
+
+
+void devclose(void)
+{
+ if (block_device)
+ fclose(block_device);
+ block_device = NULL;
+ device_size = 0;
+}
+
+int devread(unsigned long sector, unsigned long byte_offset, unsigned long byte_len, void *buf)
+{
+ if (!block_device) {
+ fprintf(stdcerr, "devread: Device not open.\n");
+ return 0;
+ }
+
+ const unsigned long offset = sector * 512 + byte_offset;
+ if (offset + byte_len > device_size)
+ fprintf(stdcerr, "devread: Attempt to read beyond device.\n");
+ return 0;
+ }
+
+ if fseek(block_device, sector * 512 + byte_offset, SEEK_SET);
+ if (fread(buf, byte_len, 1, block_device) != byte_len) {
+ fprintf(stdcerr, "devread: Failed to read from device.\n");
+ return 0;
+ }
+ return 1;
+}
+
+
+
+//void dev_set_partition(unsigned long start, unsigned long size);
+//void dev_get_partition(unsigned long *start, unsigned long *size);
+
+//int file_open(const char *filename);
+//int file_read(void *buf, unsigned long len);
+//unsigned long file_seek(unsigned long offset);
+//unsigned long file_size(void);
+//void file_set_size(unsigned long size);
+//void file_close(void);
+
+#endif /* FS_H */
diff --git a/src/fs.h b/src/fs.h
new file mode 100644
index 0000000..cf7f003
--- /dev/null
+++ b/src/fs.h
@@ -0,0 +1,39 @@
+#ifndef FS_H
+#define FS_H
+
+/** devopen
+ * @param name Filename to be used as blockdevice
+ * @param reopen Unused, set NULL
+ * @return 1 on success, 0 on failure !CAUTION
+ */
+int devopen(const char *name, int *reopen);
+
+/** devclose
+ */
+void devclose(void);
+
+/** devread
+ * @param sector 512 byte sector of the block device
+ * @param byte_offset Offset in the block
+ * @param byte_len Buffer length
+ * @param buf Buffer
+ * @return 1 on sucess, 0 on failure !CAUTION
+ */
+int devread(unsigned long sector, unsigned long byte_offset,
+ unsigned long byte_len, void *buf);
+
+
+
+
+
+void dev_set_partition(unsigned long start, unsigned long size);
+void dev_get_partition(unsigned long *start, unsigned long *size);
+
+int file_open(const char *filename);
+int file_read(void *buf, unsigned long len);
+unsigned long file_seek(unsigned long offset);
+unsigned long file_size(void);
+void file_set_size(unsigned long size);
+void file_close(void);
+
+#endif /* FS_H */
diff --git a/src/main.c b/src/main.c
new file mode 100644
index 0000000..91a40d7
--- /dev/null
+++ b/src/main.c
@@ -0,0 +1,22 @@
+#include <stdio.h>
+
+
+int main(int argc, char* argv[])
+{
+ if (argc != 2) {
+ fprintf(stdcerr, "Use %s /path/to/filesystem\n", argv[0]);
+ return -1;
+ }
+
+ if (devopen(argv[1], NULL) != 1) {
+ fprintf(stdcerr, "Faild to open %s\n", argv[1]);
+ return -1;
+ }
+
+ // TODO
+
+
+ devclose();
+ return 0;
+}
+