-
Notifications
You must be signed in to change notification settings - Fork 13
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
c77d1e6
commit 72122dc
Showing
26 changed files
with
14,756 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,124 @@ | ||
genc/genc-qoiconv | ||
genc/genc-qoibench | ||
genc/stainless.c | ||
genc/stainless.h | ||
output/ | ||
|
||
# Stainless | ||
/bin/stainless-* | ||
.stainless-cache/ | ||
.stainless.conf | ||
.stainless-external-tests/ | ||
.stainless-package-standalone/ | ||
|
||
# Vim | ||
*.swp | ||
|
||
# emacs | ||
*~ | ||
|
||
# Ripgrep | ||
.rgignore | ||
|
||
# ensime | ||
.ensime | ||
.ensime_cache | ||
|
||
# sbt | ||
target | ||
/project/build | ||
project/project | ||
/stainless | ||
/.test-history | ||
/out-classes | ||
|
||
# synthesis | ||
derivation*.dot | ||
|
||
# stainless | ||
last.log | ||
*.last | ||
*.table | ||
*.log | ||
smt-sessions/ | ||
tip-sessions/ | ||
pri-sessions/ | ||
stainless.out/ | ||
repairs.dat | ||
tmp | ||
stainless-stack-trace.txt | ||
|
||
#eclipse | ||
.cache | ||
.classpath | ||
.project | ||
.settings/ | ||
.worksheet/ | ||
|
||
#intellij | ||
.idea | ||
Leon.eml | ||
Leon.iml | ||
*.iml | ||
/.idea_modules | ||
|
||
#scripts | ||
out-classes | ||
|
||
#z3 | ||
.z3-trace | ||
|
||
#travis | ||
/travis/builds | ||
|
||
# Windows | ||
/cvc4.exe | ||
/libz3.dll | ||
/libz3.lib | ||
/msvcp100.dll | ||
/msvcr100.dll | ||
/scalaz3.dll | ||
/scalaz3.lib | ||
/vcomp100.dll | ||
/z3.exe | ||
/libz3java.dll | ||
/libz3java.lib | ||
|
||
# Coq files | ||
*# | ||
.#* | ||
*.aux | ||
*.glob | ||
*.vo | ||
*.v.d | ||
verif*.v | ||
.lia.cache | ||
.nia.cache | ||
.coqdeps.d | ||
*.vok | ||
*.vos | ||
slc-lib/.Makefile.d | ||
slc-lib/Makefile | ||
slc-lib/Makefile.conf | ||
|
||
# metals and VSCode | ||
.vscode | ||
.metals | ||
.bsp | ||
project/metals.sbt | ||
null | ||
.bloop/ | ||
project/.bloop/ | ||
project/project/ | ||
.bsp | ||
|
||
# ripgrep | ||
.rgignore | ||
|
||
# C files | ||
*.out | ||
|
||
# LZW GenC benchmarks files | ||
input.txt | ||
decoded.txt | ||
encoded.txt |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
.PHONY: genc | ||
|
||
CC=gcc # Clang seems to not be able to eliminate tail-calls present in decodeLoop and encodeLoop | ||
# For, macOS users, gcc is an alias to clang, make sure to have gcc installed! | ||
CFLAGS=-O3 | ||
|
||
all: genc genc-qoibench genc-qoiconv | ||
|
||
stainless.c: | ||
stainless-dotty ../verified/common.scala ../verified/decoder.scala ../verified/encoder.scala \ | ||
--genc -J-Xms10G -J-Xss20M | ||
|
||
genc: stainless.c | ||
|
||
genc-qoibench: stainless.c genc-qoibench.c genc-bridge.c | ||
|
||
genc-qoiconv: stainless.c genc-qoiconv.c genc-bridge.c | ||
|
||
clean: | ||
rm -f genc-qoibench genc-qoiconv stainless.c stainless.h |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,78 @@ | ||
#include <stdio.h> | ||
#include "stainless.h" | ||
#include "genc-bridge.h" | ||
|
||
int genc_qoi_decode(void *data, size_t length, void **pixels, int *w, int *h, int *channels) { | ||
OptionMut_DecodedResult decoded_res = decode((array_int8) { .data = data, .length = length }, length); | ||
if (decoded_res.tag == tag_SomeMut_DecodedResult) { | ||
*pixels = decoded_res.value.SomeMut_DecodedResult_v.v.pixels.data; | ||
*w = decoded_res.value.SomeMut_DecodedResult_v.v.w; | ||
*h = decoded_res.value.SomeMut_DecodedResult_v.v.h; | ||
*channels = decoded_res.value.SomeMut_DecodedResult_v.v.chan; | ||
return 1; | ||
} else { | ||
return 0; | ||
} | ||
} | ||
|
||
int genc_qoi_encode(void *pixels, int w, int h, int channels, void **data, size_t *length) { | ||
OptionMut_EncodedResult encoded_res = encode((array_int8) { .data = pixels, .length = w * h * channels }, w, h, channels); | ||
if (encoded_res.tag == tag_SomeMut_EncodedResult) { | ||
*data = encoded_res.value.SomeMut_EncodedResult_v.v.encoded.data; | ||
*length = encoded_res.value.SomeMut_EncodedResult_v.v.length; | ||
return 1; | ||
} else { | ||
return 0; | ||
} | ||
} | ||
|
||
int genc_qoi_read(const char *filename, void **pixels, int *w, int *h, int *channels) { | ||
FILE *f = fopen(filename, "rb"); | ||
|
||
if (!f) { | ||
return 0; | ||
} | ||
|
||
fseek(f, 0, SEEK_END); | ||
long size = ftell(f); | ||
if (size <= 0) { | ||
fclose(f); | ||
return 0; | ||
} | ||
fseek(f, 0, SEEK_SET); | ||
|
||
int8_t *data = malloc(size); | ||
if (!data) { | ||
fclose(f); | ||
return 0; | ||
} | ||
|
||
size_t bytes_read = fread(data, 1, size, f); | ||
fclose(f); | ||
if (bytes_read != size) { | ||
return 0; | ||
} | ||
|
||
int res = genc_qoi_decode(data, size, pixels, w, h, channels); | ||
free(data); | ||
return res; | ||
} | ||
|
||
int genc_qoi_write(const char *filename, void *pixels, int w, int h, int channels) { | ||
void *data; | ||
size_t length; | ||
int enc_res = genc_qoi_encode(pixels, w, h, channels, &data, &length); | ||
if (!enc_res) { | ||
return 0; | ||
} | ||
|
||
FILE *f = fopen(filename, "wb"); | ||
if (!f) { | ||
return 0; | ||
} | ||
|
||
size_t written = fwrite(data, 1, length, f); | ||
fclose(f); | ||
free(data); | ||
return written == length; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
#include <stdint.h> | ||
|
||
int genc_qoi_decode(void *data, size_t length, void **pixels, int *w, int *h, int *channels); | ||
|
||
int genc_qoi_encode(void *pixels, int w, int h, int channels, void **data, size_t *length); | ||
|
||
int genc_qoi_read(const char *filename, void **pixels, int *w, int *h, int *channels); | ||
|
||
int genc_qoi_write(const char *filename, void *pixels, int w, int h, int channels); |
Oops, something went wrong.