diff options
author | Xander <xander@biltopia.org> | 2023-07-13 00:26:49 +0200 |
---|---|---|
committer | Xander <xander@biltopia.org> | 2023-07-13 00:26:49 +0200 |
commit | e02a7e790650b31b713dde5c39ad6172c048f571 (patch) | |
tree | e06f29fbff44f9dcb44dc4c0c30dd58484069785 /kernel | |
parent | f44cb1fd2e58f0233dccdf8a1fac84e310857e7e (diff) | |
download | ats-os-e02a7e790650b31b713dde5c39ad6172c048f571.tar.xz ats-os-e02a7e790650b31b713dde5c39ad6172c048f571.zip |
int to string conversion implementation
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/interrupts/idt.dats | 4 | ||||
-rw-r--r-- | kernel/itoa.dats | 63 | ||||
-rw-r--r-- | kernel/output/print.dats | 10 |
3 files changed, 73 insertions, 4 deletions
diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats index ba6bb20..851a2b0 100644 --- a/kernel/interrupts/idt.dats +++ b/kernel/interrupts/idt.dats @@ -64,7 +64,7 @@ var idt : @[idt_entry_t][IDT_MAX_DESCRIPTORS] // The table var idtr : idtr_t // interrupt descriptor table register instance fun idt_set_descriptor {n : nat | n < IDT_MAX_DESCRIPTORS} (vector: int n, isr: uint64, flags: uint8) : void = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) + extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) // takeout proof UNSAFE: prval (pf, fpf) = __assert (addr@(idt)) val x = $UN.cast{uint64}(0xFFFF) val y = $UN.cast{uint64}(0xFFFFFFF) @@ -118,7 +118,7 @@ end implement idt_init() : void = let extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l) - prval (pf, fpf) = __assert (addr@(idtr)) + prval (pf, fpf) = __assert (addr@(idtr)) // takeout proof UNSAFE: in idtr.base := addr@(idt); idtr.limit := $UN.cast(8 * IDT_MAX_DESCRIPTORS); diff --git a/kernel/itoa.dats b/kernel/itoa.dats new file mode 100644 index 0000000..7557dac --- /dev/null +++ b/kernel/itoa.dats @@ -0,0 +1,63 @@ +#include "share/atspre_staload.hats" + +#define ATS_DYNLOADFLAG 0 + + +fun reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) : void = let + fun loop {i,j,n:nat | i < j && j < n} (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) : void = let + val tmp = p->[i] + in + p->[i] := p->[j]; + p->[j] := tmp; + if (i+1 < j-1) then + loop(pf | p, i+1,j-1) + end +in + if (n > 0) then + loop(pf | p, 0, n) +end + +local + +#define BUFFER_SIZE 50 + +staload UN = "prelude/SATS/unsafe.sats" + +extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) : [n : nat | n < BUFFER_SIZE] string n +extern praxi __assert {l:addr} (ptr: ptr (l)): vtakeout0 (@[char][BUFFER_SIZE]@l) +var buffer : @[char][BUFFER_SIZE] // Size should be BUFFER_SIZE + +in + +//TODO: make function better by handling to large number for buffer + +extern fun itoa {v,n:nat | n > 1 && n < 33 && v > 0} (value : int v, base : int n) : [k : nat | k < BUFFER_SIZE] string k +implement itoa(value,base) = let + prval (pf , fpf) = __assert(addr@buffer) // Get proofs UNSAFE: + + fun loop {n,i : nat | n > 0 && i < BUFFER_SIZE} {l:addr} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int n, i : size_t i): void = let + val r = n % base + val k = n / base + in + if (r >= 10) then + p->[i] := $UN.cast{char}(65 + (r - 10)) + else + p->[i] := $UN.cast{char}(48 + r); + + if (i + 2 < BUFFER_SIZE) then + if (k > 0) then + loop(pf | p, k, succ(i)) + else ( + p->[succ(i)] := '\0'; + reverse(pf | p, sz2i(i))) + end + + // Run loop + val () = loop(pf | addr@buffer, value, i2sz(0)); + val str = char_arr2string(buffer); // Convert to string UNSAFE: +in + let prval () = fpf(pf) in end; + str // Return string +end + +end diff --git a/kernel/output/print.dats b/kernel/output/print.dats index 22fe575..9b5def0 100644 --- a/kernel/output/print.dats +++ b/kernel/output/print.dats @@ -2,14 +2,20 @@ #define ATS_DYNLOADFLAG 0 + staload "kernel/output/writer.sats" +staload "kernel/itoa.dats" extern fun print_newline() : void -implement print_newline() : void = put_string("\n") +implement print_newline() = put_string("\n") extern fun assert_errmsg(b: bool, msg: string) : void -implement assert_errmsg(b: bool, msg: string) : void = put_string(msg) +implement assert_errmsg(b,msg) = if (~b) then put_string(msg) +extern fun print_int {n : nat | n > 0} (n : int n) : void +implement print_int(n) = put_string(itoa(n,10)) + overload print with put_string of 1 +overload print with print_int of 1 macdef assertloc(tf) = assert_errmsg (,(tf), $mylocation) |