Skip to content

Commit

Permalink
delete wrapper functions in owi.c
Browse files Browse the repository at this point in the history
  • Loading branch information
Laplace-Demon committed Jun 17, 2024
1 parent 6231a52 commit 5a78349
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 50 deletions.
7 changes: 2 additions & 5 deletions src/libc/include/owi.h
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
#ifndef _OWI_H
#define _OWI_H

void *owi_malloc(void *base, unsigned int size) __attribute__((import_module("summaries"))) __attribute__((import_name("malloc")));
void *owi_malloc(void *base, unsigned int size) __attribute__((import_module("summaries"))) __attribute__((import_name("alloc")));

void owi_free(void *) __attribute__((import_module("summaries"))) __attribute__((import_name("free")));
void owi_free(void *) __attribute__((import_module("summaries"))) __attribute__((import_name("dealloc")));

char owi_i8(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("i8_symbol")));

Expand All @@ -19,7 +19,4 @@ double owi_f64(void) __attribute__((import_module("symbolic"))) __attribute__((i
void owi_assume(int c) __attribute__((import_module("symbolic"))) __attribute__((import_name("assume")));
void owi_assert(int c) __attribute__((import_module("symbolic"))) __attribute__((import_name("assert")));

int and_(int, int);
int or_(int, int);

#endif
57 changes: 12 additions & 45 deletions src/libc/src/owi.c
Original file line number Diff line number Diff line change
@@ -1,58 +1,25 @@
#include <owi.h>

__attribute__((import_module("summaries"), import_name("alloc"))) void *
__owi_alloc(void *, unsigned int);
owi_malloc(void *, unsigned int);
__attribute__((import_module("summaries"), import_name("dealloc"))) void
__owi_dealloc(void *);
owi_free(void *);

__attribute__((import_module("symbolic"), import_name("i8_symbol"))) char __i8(void);
__attribute__((import_module("symbolic"), import_name("i8_symbol"))) char
owi_i8(void);
__attribute__((import_module("symbolic"), import_name("i32_symbol"))) int
__i32(void);
owi_i32(void);
__attribute__((import_module("symbolic"), import_name("i64_symbol"))) long long
__i64(void);
owi_i64(void);
__attribute__((import_module("symbolic"), import_name("f32_symbol"))) float
__f32(void);
owi_f32(void);
__attribute__((import_module("symbolic"), import_name("f64_symbol"))) double
__f64(void);
owi_f64(void);

__attribute__((import_module("symbolic"), import_name("assume"))) void
__owi_assume(int);
owi_assume(int);
__attribute__((import_module("symbolic"), import_name("assert"))) void
__owi_assert(int);
owi_assert(int);

void *owi_malloc(void *base, unsigned int size) { return __owi_alloc(base, size); }
void owi_free(void *base) { __owi_dealloc(base); }

char owi_i8(void) { return __i8(); };
int owi_i32(void) { return __i32(); }
long long owi_i64(void) { return __i64(); }
float owi_f32(void) { return __f32(); }
double owi_f64(void) { return __f64(); }


void owi_assume(int c) { __owi_assume(c); }
void owi_assert(int c) { __owi_assert(c); }

void assume(int) __attribute__((weak, alias("owi_assume")));

int and_(int a, int b) {
__asm__ __volatile__("local.get 0;"
"i32.const 0;"
"i32.ne;"
"local.get 1;"
"i32.const 0;"
"i32.ne;"
"i32.and;"
"return;");
}

int or_(int a, int b) {
__asm__ __volatile__("local.get 0;"
"i32.const 0;"
"i32.ne;"
"local.get 1;"
"i32.const 0;"
"i32.ne;"
"i32.or;"
"return;");
}
__attribute__((weak, import_module("symbolic"), import_name("assume"))) void
assume(int);

0 comments on commit 5a78349

Please sign in to comment.