Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

test: Add goblint static analyser. #2597

Merged
merged 1 commit into from
Jan 25, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ jobs:
analysis:
strategy:
matrix:
tool: [autotools, clang-tidy, compcert, cppcheck, doxygen, infer, misra, tcc, tokstyle]
tool: [autotools, clang-tidy, compcert, cppcheck, doxygen, goblint, infer, misra, tcc, tokstyle]
runs-on: ubuntu-latest
steps:
- name: Set up Docker Buildx
Expand Down
8 changes: 8 additions & 0 deletions other/docker/goblint/BUILD.bazel
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
load("@rules_cc//cc:defs.bzl", "cc_library")

cc_library(
name = "sodium",
testonly = True,
srcs = ["sodium.c"],
deps = ["@libsodium"],
)
26 changes: 26 additions & 0 deletions other/docker/goblint/Dockerfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
FROM ghcr.io/goblint/analyzer:latest

RUN apt-get update && \
DEBIAN_FRONTEND="noninteractive" apt-get install -y --no-install-recommends \
libsodium-dev \
tcc \
&& apt-get clean \
&& rm -rf /var/lib/apt/lists/*

WORKDIR /work
COPY auto_tests/ /work/auto_tests/
COPY testing/ /work/testing/
COPY toxav/ /work/toxav/
COPY toxcore/ /work/toxcore/
COPY toxencryptsave/ /work/toxencryptsave/
COPY third_party/ /work/third_party/

COPY other/make_single_file /work/other/
COPY other/docker/goblint/sodium.c /work/other/docker/goblint/

RUN other/make_single_file -core auto_tests/tox_new_test.c other/docker/goblint/sodium.c > analysis.c
# Try compiling+linking just to make sure we have all the fake functions.
RUN tcc analysis.c

COPY other/docker/goblint/analysis.json /work/other/docker/goblint/
RUN /opt/goblint/analyzer/bin/goblint --conf /work/other/docker/goblint/analysis.json analysis.c
43 changes: 43 additions & 0 deletions other/docker/goblint/analysis.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
{
"ana": {
"activated": [
"base","mallocWrapper","escape","mutex","mutexEvents","access","assert","expRelation"
],
"arrayoob": true,
"wp": true,
"apron": {
"strengthening": true
},
"base": {
"structs" : {
"domain" : "combined-sk"
},
"arrays": {
"domain": "partitioned"
}
},
"malloc": {
"wrappers": [
"mem_balloc",
"mem_alloc",
"mem_valloc",
"mem_vrealloc"
]
}
},
"warn": {
"behavior": false,
"call": false,
"integer": true,
"float": false,
"race": false,
"deadcode": false,
"unsound": false,
"imprecise": false,
"success": false,
"unknown": false
},
"exp": {
"earlyglobs": true
}
}
5 changes: 5 additions & 0 deletions other/docker/goblint/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#!/bin/sh

set -eux
BUILD=goblint
docker build -t "toxchat/c-toxcore:$BUILD" -f "other/docker/$BUILD/Dockerfile" .
112 changes: 112 additions & 0 deletions other/docker/goblint/sodium.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
#include <sodium.h>

#include <string.h>

int crypto_sign_keypair(unsigned char *pk, unsigned char *sk)
{
memset(pk, 0, 32);
memset(sk, 0, 32);
return 0;
}
int crypto_sign_ed25519_pk_to_curve25519(unsigned char *curve25519_pk,
const unsigned char *ed25519_pk)
{
memset(curve25519_pk, 0, 32);
return 0;
}
int crypto_sign_ed25519_sk_to_curve25519(unsigned char *curve25519_sk,
const unsigned char *ed25519_sk)
{
memset(curve25519_sk, 0, 32);
return 0;
}
void sodium_memzero(void * const pnt, const size_t len)
{
memset(pnt, 0, len);
}
int sodium_mlock(void * const addr, const size_t len)
{
return 0;
}
int sodium_munlock(void * const addr, const size_t len)
{
return 0;
}
int crypto_verify_32(const unsigned char *x, const unsigned char *y)
{
return memcmp(x, y, 32);
}
int crypto_verify_64(const unsigned char *x, const unsigned char *y)
{
return memcmp(x, y, 64);
}
int crypto_sign_detached(unsigned char *sig, unsigned long long *siglen_p,
const unsigned char *m, unsigned long long mlen,
const unsigned char *sk)
{
return 0;
}
int crypto_sign_verify_detached(const unsigned char *sig,
const unsigned char *m,
unsigned long long mlen,
const unsigned char *pk)
{
return 0;
}
int crypto_box_beforenm(unsigned char *k, const unsigned char *pk,
const unsigned char *sk)
{
memset(k, 0, 32);
return 0;
}
int crypto_box_afternm(unsigned char *c, const unsigned char *m,
unsigned long long mlen, const unsigned char *n,
const unsigned char *k)
{
memset(c, 0, 32);
return 0;
}
int crypto_box_open_afternm(unsigned char *m, const unsigned char *c,
unsigned long long clen, const unsigned char *n,
const unsigned char *k)
{
return 0;
}
int crypto_scalarmult_curve25519_base(unsigned char *q,
const unsigned char *n)
{
memset(q, 0, 32);
return 0;
}
int crypto_auth(unsigned char *out, const unsigned char *in,
unsigned long long inlen, const unsigned char *k)
{
return 0;
}
int crypto_auth_verify(const unsigned char *h, const unsigned char *in,
unsigned long long inlen, const unsigned char *k)
{
return 0;
}
int crypto_hash_sha256(unsigned char *out, const unsigned char *in,
unsigned long long inlen)
{
return 0;
}
int crypto_hash_sha512(unsigned char *out, const unsigned char *in,
unsigned long long inlen)
{
return 0;
}
void randombytes(unsigned char * const buf, const unsigned long long buf_len)
{
memset(buf, 0, buf_len);
}
uint32_t randombytes_uniform(const uint32_t upper_bound)
{
return upper_bound;
}
int sodium_init(void)
{
return 0;
}
Loading