From 904094281b062aff3445ca41fec57e4cfd0f563d Mon Sep 17 00:00:00 2001 From: Matthew Sotoudeh Date: Tue, 10 Nov 2020 14:06:35 -0800 Subject: Initial code release --- examples/program_analysis/paper_demos/api1.after.txt | 14 ++++++++++++++ examples/program_analysis/paper_demos/api1.before.txt | 14 ++++++++++++++ examples/program_analysis/paper_demos/api2.after.txt | 14 ++++++++++++++ examples/program_analysis/paper_demos/api2.before.txt | 14 ++++++++++++++ examples/program_analysis/paper_demos/api3.after.txt | 0 examples/program_analysis/paper_demos/api3.before.txt | 14 ++++++++++++++ examples/program_analysis/paper_demos/bash.txt | 17 +++++++++++++++++ examples/program_analysis/paper_demos/docs.after.txt | 9 +++++++++ examples/program_analysis/paper_demos/docs.before.txt | 9 +++++++++ examples/program_analysis/paper_demos/fish.txt | 13 +++++++++++++ examples/program_analysis/paper_demos/gemm1.after.txt | 6 ++++++ examples/program_analysis/paper_demos/gemm1.before.txt | 6 ++++++ examples/program_analysis/paper_demos/gemm2.after.txt | 10 ++++++++++ examples/program_analysis/paper_demos/gemm2.before.txt | 10 ++++++++++ examples/program_analysis/paper_demos/gemm3.after.txt | 0 examples/program_analysis/paper_demos/gemm3.before.txt | 6 ++++++ examples/program_analysis/paper_demos/gemm4.bad.txt | 6 ++++++ 17 files changed, 162 insertions(+) create mode 100644 examples/program_analysis/paper_demos/api1.after.txt create mode 100644 examples/program_analysis/paper_demos/api1.before.txt create mode 100644 examples/program_analysis/paper_demos/api2.after.txt create mode 100644 examples/program_analysis/paper_demos/api2.before.txt create mode 100644 examples/program_analysis/paper_demos/api3.after.txt create mode 100644 examples/program_analysis/paper_demos/api3.before.txt create mode 100644 examples/program_analysis/paper_demos/bash.txt create mode 100644 examples/program_analysis/paper_demos/docs.after.txt create mode 100644 examples/program_analysis/paper_demos/docs.before.txt create mode 100644 examples/program_analysis/paper_demos/fish.txt create mode 100644 examples/program_analysis/paper_demos/gemm1.after.txt create mode 100644 examples/program_analysis/paper_demos/gemm1.before.txt create mode 100644 examples/program_analysis/paper_demos/gemm2.after.txt create mode 100644 examples/program_analysis/paper_demos/gemm2.before.txt create mode 100644 examples/program_analysis/paper_demos/gemm3.after.txt create mode 100644 examples/program_analysis/paper_demos/gemm3.before.txt create mode 100644 examples/program_analysis/paper_demos/gemm4.bad.txt (limited to 'examples/program_analysis/paper_demos') diff --git a/examples/program_analysis/paper_demos/api1.after.txt b/examples/program_analysis/paper_demos/api1.after.txt new file mode 100644 index 0000000..d4f6957 --- /dev/null +++ b/examples/program_analysis/paper_demos/api1.after.txt @@ -0,0 +1,14 @@ +#include +#include "cam.h" + +#define BUFFER_SIZE (1024 * 1024) +char buffer[BUFFER_SIZE]; + +void try_record_video() { + int result = cam_record_video(buffer, BUFFER_SIZE); + if (result == -4) { + printf("Could not record video.\n"); + } else { + printf("Recording video worked!\n"); + } +} diff --git a/examples/program_analysis/paper_demos/api1.before.txt b/examples/program_analysis/paper_demos/api1.before.txt new file mode 100644 index 0000000..0703da3 --- /dev/null +++ b/examples/program_analysis/paper_demos/api1.before.txt @@ -0,0 +1,14 @@ +#include +#include "cam.h" + +#define BUFFER_SIZE (1024 * 1024) +char buffer[BUFFER_SIZE]; + +void try_record_video() { + int result = cam_record_video(buffer, BUFFER_SIZE, RES_AUTO); + if (result == -1) { + printf("Could not record video.\n"); + } else { + printf("Recording video worked!\n"); + } +} diff --git a/examples/program_analysis/paper_demos/api2.after.txt b/examples/program_analysis/paper_demos/api2.after.txt new file mode 100644 index 0000000..340e681 --- /dev/null +++ b/examples/program_analysis/paper_demos/api2.after.txt @@ -0,0 +1,14 @@ +#include +#include "cam.h" + +#define BUFFER_SIZE (1024 * 1024) +char buffer[BUFFER_SIZE]; + +void try_record_audio() { + int result = cam_record_audio(buffer, BUFFER_SIZE); + if (result == -2) { + printf("Could not record audio.\n"); + } else { + printf("Recorded audio!\n"); + } +} diff --git a/examples/program_analysis/paper_demos/api2.before.txt b/examples/program_analysis/paper_demos/api2.before.txt new file mode 100644 index 0000000..f74c538 --- /dev/null +++ b/examples/program_analysis/paper_demos/api2.before.txt @@ -0,0 +1,14 @@ +#include +#include "cam.h" + +#define BUFFER_SIZE (1024 * 1024) +char buffer[BUFFER_SIZE]; + +void try_record_audio() { + int result = cam_record_audio(buffer, BUFFER_SIZE, RES_AUTO); + if (result == -5) { + printf("Could not record audio.\n"); + } else { + printf("Recorded audio!\n"); + } +} diff --git a/examples/program_analysis/paper_demos/api3.after.txt b/examples/program_analysis/paper_demos/api3.after.txt new file mode 100644 index 0000000..e69de29 diff --git a/examples/program_analysis/paper_demos/api3.before.txt b/examples/program_analysis/paper_demos/api3.before.txt new file mode 100644 index 0000000..cb8d731 --- /dev/null +++ b/examples/program_analysis/paper_demos/api3.before.txt @@ -0,0 +1,14 @@ +#include +#include "cam.h" + +#define BUFFER_SIZE (1024) +char buffer[BUFFER_SIZE]; + +void try_record_still() { + int result = cam_record_frame(buffer, BUFFER_SIZE, RES_AUTO); + if (result == -3) { + printf("Could not record audio.\n"); + } else { + printf("Recorded audio!\n"); + } +} diff --git a/examples/program_analysis/paper_demos/bash.txt b/examples/program_analysis/paper_demos/bash.txt new file mode 100644 index 0000000..083401c --- /dev/null +++ b/examples/program_analysis/paper_demos/bash.txt @@ -0,0 +1,17 @@ +int cd_builtin (list) WORD_LIST *list; /*@\color{red}{//B1} @*/ +{ + char *dirname, *cdpath, *path, *temp; +... + +struct builtin static_shell_builtins[] = { +... + { "cd", cd_builtin, ... }, /*@\color{red}{//B2} @*/ +... +struct builtin *shell_builtins = static_shell_builtins; /*@\color{red}{//B3} @*/ + +struct builtin * builtin_address_internal + (name, disabled_okay) + char *name; int disabled_okay; { /*@\color{red}{//B4} @*/ +... + j = shell_builtins[mid].name[0] - name[0]; +... diff --git a/examples/program_analysis/paper_demos/docs.after.txt b/examples/program_analysis/paper_demos/docs.after.txt new file mode 100644 index 0000000..e162420 --- /dev/null +++ b/examples/program_analysis/paper_demos/docs.after.txt @@ -0,0 +1,9 @@ +# CameraLib v2.0 +### `cam_record_video(buffer, buffer_size)` +Records video from the main camera into `buffer` until `buffer_size` bytes are reached. On error returns -4. + +### `cam_record_audio(buffer, buffer_size)` +Uses the main camera's microphone to record audio into `buffer` until `buffer_size` bytes have been recorded. On error returns -2. + +### `cam_record_frame(buffer, buffer_size)` +Uses the main camera to record a single image to `buffer`. Automatically sets the resolution to fit in `buffer_size`. On failure returns -6. diff --git a/examples/program_analysis/paper_demos/docs.before.txt b/examples/program_analysis/paper_demos/docs.before.txt new file mode 100644 index 0000000..1f10feb --- /dev/null +++ b/examples/program_analysis/paper_demos/docs.before.txt @@ -0,0 +1,9 @@ +# CameraLib v1.0 +### `cam_record_video(buffer, buffer_size, resolution)` +Records video from the main camera into `buffer` until `buffer_size` bytes are reached. On error returns -1. + +### `cam_record_audio(buffer, buffer_size, resolution)` +Uses the main camera's microphone to record audio into `buffer` until `buffer_size` bytes have been recorded. On error returns -5. + +### `cam_record_frame(buffer, buffer_size, resolution)` +Uses the main camera to record a single image to `buffer`. Automatically sets the resolution to fit in `buffer_size`. On failure returns -3. diff --git a/examples/program_analysis/paper_demos/fish.txt b/examples/program_analysis/paper_demos/fish.txt new file mode 100644 index 0000000..2b933f0 --- /dev/null +++ b/examples/program_analysis/paper_demos/fish.txt @@ -0,0 +1,13 @@ +int builtin_cd(parser_t &parser, io_streams_t &streams, wchar_t **argv) { /*@\color{red}{//F1} @*/ + const wchar_t *cmd = argv[0]; + int argc = builtin_count_args(argv); +... + +static const builtin_data_t builtin_datas[] = { +... + {L"cd", &builtin_cd, ...}, /*@\color{red}{//F2} @*/ +... + +static const builtin_data_t *builtin_lookup(const wcstring &name) { /*@\color{red}{//F3} @*/ + const builtin_data_t *array_end = builtin_datas + BUILTIN_COUNT; +... diff --git a/examples/program_analysis/paper_demos/gemm1.after.txt b/examples/program_analysis/paper_demos/gemm1.after.txt new file mode 100644 index 0000000..5d49a4c --- /dev/null +++ b/examples/program_analysis/paper_demos/gemm1.after.txt @@ -0,0 +1,6 @@ +assert(k > 0); +int outer = k * 100; +int inner = k * 10; +read_mat(outer, inner, &A); +read_mat(inner, outer, &B); +gemm_skinny(A, B, &C, outer, inner, outer); diff --git a/examples/program_analysis/paper_demos/gemm1.before.txt b/examples/program_analysis/paper_demos/gemm1.before.txt new file mode 100644 index 0000000..5ff9d2b --- /dev/null +++ b/examples/program_analysis/paper_demos/gemm1.before.txt @@ -0,0 +1,6 @@ +assert(k > 0); +int outer = k * 100; +int inner = k * 10; +read_mat(outer, inner, &A); +read_mat(inner, outer, &B); +gemm_large(A, B, &C, outer, inner, outer); diff --git a/examples/program_analysis/paper_demos/gemm2.after.txt b/examples/program_analysis/paper_demos/gemm2.after.txt new file mode 100644 index 0000000..19bb8aa --- /dev/null +++ b/examples/program_analysis/paper_demos/gemm2.after.txt @@ -0,0 +1,10 @@ +assert(k > 1); +int outer = k, A_cols = k / 2; +read_mat(outer, A_cols, &A); +read_mat(A_cols, outer, &B); +while (!done(A, B)) { + read_row(&A); + read_col(&B); + outer++; +} +gemm_skinny(A, B, &C, outer, A_cols, outer); diff --git a/examples/program_analysis/paper_demos/gemm2.before.txt b/examples/program_analysis/paper_demos/gemm2.before.txt new file mode 100644 index 0000000..6e0ab1c --- /dev/null +++ b/examples/program_analysis/paper_demos/gemm2.before.txt @@ -0,0 +1,10 @@ +assert(k > 1); +int outer = k, A_cols = k / 2; +read_mat(outer, A_cols, &A); +read_mat(A_cols, outer, &B); +while (!done(A, B)) { + read_row(&A); + read_col(&B); + outer++; +} +gemm_large(A, B, &C, outer, A_cols, outer); diff --git a/examples/program_analysis/paper_demos/gemm3.after.txt b/examples/program_analysis/paper_demos/gemm3.after.txt new file mode 100644 index 0000000..e69de29 diff --git a/examples/program_analysis/paper_demos/gemm3.before.txt b/examples/program_analysis/paper_demos/gemm3.before.txt new file mode 100644 index 0000000..3cd1072 --- /dev/null +++ b/examples/program_analysis/paper_demos/gemm3.before.txt @@ -0,0 +1,6 @@ +assert(k > 5); +int AB_rowcol = k; +int inner = k * k; +read_mat(AB_rowcol, inner, &A); +read_mat(inner, AB_rowcol, &B); +gemm_large(A, B, &C, AB_rowcol, inner, AB_rowcol); diff --git a/examples/program_analysis/paper_demos/gemm4.bad.txt b/examples/program_analysis/paper_demos/gemm4.bad.txt new file mode 100644 index 0000000..a57dc33 --- /dev/null +++ b/examples/program_analysis/paper_demos/gemm4.bad.txt @@ -0,0 +1,6 @@ +assert(k > 0); +int outer = k * 10; +int inner = k * 10; +read_mat(outer, inner, &A); +read_mat(inner, outer, &B); +gemm_large(A, B, &C); -- cgit v1.2.3