From d24c79f76c4b1d6edfcdcd8e1f44359907f2bdc3 Mon Sep 17 00:00:00 2001 From: Christoph Kirsch Date: Mon, 1 Jun 2020 12:18:16 +0200 Subject: [PATCH] Printing unsigned integers properly --- examples/int-max-min.c | 8 +-- examples/local.c | 2 +- selfie.c | 109 +++++++++++++++++++++++------------------ tools/modeler.c | 2 +- tools/monster.c | 34 ++++++------- 5 files changed, 83 insertions(+), 72 deletions(-) diff --git a/examples/int-max-min.c b/examples/int-max-min.c index 99f1d99a..6ed0397a 100644 --- a/examples/int-max-min.c +++ b/examples/int-max-min.c @@ -3,24 +3,20 @@ // libcstar procedures for printing void init_library(); void print(uint64_t* s); +void print_unsigned_integer(uint64_t n); void print_integer(uint64_t n); void print_hexadecimal(uint64_t n, uint64_t a); void print_octal(uint64_t n, uint64_t a); void print_binary(uint64_t n, uint64_t a); void println(); -uint64_t UINT64_MAX; - -uint64_t INT64_MAX; -uint64_t INT64_MIN; - uint64_t main() { // initialize selfie's libcstar library init_library(); // print UINT64_MAX in decimal print("UINT64_MAX in decimal: "); - print_integer(UINT64_MAX); + print_unsigned_integer(UINT64_MAX); println(); // print UINT64_MAX in hexadecimal diff --git a/examples/local.c b/examples/local.c index 21c8c5ab..da93a5a0 100644 --- a/examples/local.c +++ b/examples/local.c @@ -7,7 +7,7 @@ uint64_t f(uint64_t x) { uint64_t main() { uint64_t x; - + x = 0; x = x + 1; diff --git a/selfie.c b/selfie.c index f26fd1db..ee332c1e 100644 --- a/selfie.c +++ b/selfie.c @@ -136,7 +136,7 @@ void string_reverse(char* s); uint64_t string_compare(char* s, char* t); uint64_t atoi(char* s); -char* itoa(uint64_t n, char* s, uint64_t b, uint64_t a); +char* itoa(uint64_t n, char* s, uint64_t b, uint64_t d, uint64_t a); uint64_t fixed_point_ratio(uint64_t a, uint64_t b, uint64_t f); uint64_t fixed_point_percentage(uint64_t r, uint64_t f); @@ -148,6 +148,7 @@ void println(); void print_character(uint64_t c); void print_string(char* s); +void print_unsigned_integer(uint64_t n); void print_integer(uint64_t n); void unprint_integer(uint64_t n); void print_hexadecimal(uint64_t n, uint64_t a); @@ -1941,14 +1942,14 @@ uint64_t atoi(char* s) { return n; } -char* itoa(uint64_t n, char* s, uint64_t b, uint64_t a) { +char* itoa(uint64_t n, char* s, uint64_t b, uint64_t d, uint64_t a) { // assert: b in {2,4,8,10,16} uint64_t i; uint64_t sign; - // the conversion of the integer n to an ASCII string in s with - // base b and alignment a begins with the leftmost digit in s + // conversion of the integer n to an ASCII string in s with base b, + // sign d, and alignment a begins with the leftmost digit in s i = 0; // for now assuming n is positive @@ -1958,15 +1959,15 @@ char* itoa(uint64_t n, char* s, uint64_t b, uint64_t a) { store_character(s, 0, '0'); i = 1; - } else if (signed_less_than(n, 0)) { - if (b == 10) { - // n is represented as two's complement - // convert n to a positive number but remember the sign - n = -n; - - sign = 1; - } - } + } else if (d) + if (signed_less_than(n, 0)) + if (b == 10) { + // n is represented as two's complement + // convert n to a positive number but remember the sign + n = -n; + + sign = 1; + } while (n != 0) { if (n % b > 9) @@ -2132,12 +2133,16 @@ void print_string(char* s) { put_character(CHAR_DOUBLEQUOTE); } +void print_unsigned_integer(uint64_t n) { + print(itoa(n, integer_buffer, 10, 0, 0)); +} + void print_integer(uint64_t n) { - print(itoa(n, integer_buffer, 10, 0)); + print(itoa(n, integer_buffer, 10, 1, 0)); } void unprint_integer(uint64_t n) { - n = string_length(itoa(n, integer_buffer, 10, 0)); + n = string_length(itoa(n, integer_buffer, 10, 1, 0)); while (n > 0) { put_character(CHAR_BACKSPACE); @@ -2147,15 +2152,15 @@ void unprint_integer(uint64_t n) { } void print_hexadecimal(uint64_t n, uint64_t a) { - print(itoa(n, integer_buffer, 16, a)); + print(itoa(n, integer_buffer, 16, 0, a)); } void print_octal(uint64_t n, uint64_t a) { - print(itoa(n, integer_buffer, 8, a)); + print(itoa(n, integer_buffer, 8, 0, a)); } void print_binary(uint64_t n, uint64_t a) { - print(itoa(n, integer_buffer, 2, a)); + print(itoa(n, integer_buffer, 2, 0, a)); } uint64_t print_format0(char* s, uint64_t i) { @@ -2206,6 +2211,10 @@ uint64_t print_format1(char* s, uint64_t i, char* a) { } else if (load_character(s, i + 1) == 'c') { put_character((uint64_t) a); + return i + 2; + } else if (load_character(s, i + 1) == 'u') { + print_unsigned_integer((uint64_t) a); + return i + 2; } else if (load_character(s, i + 1) == 'd') { print_integer((uint64_t) a); @@ -2217,11 +2226,17 @@ uint64_t print_format1(char* s, uint64_t i, char* a) { if (p < 10) { // the character at i + 2 is in fact a digit - print_integer((uint64_t) a / ten_to_the_power_of(p)); + if (load_character(s, i + 3) == 'u') + print_unsigned_integer((uint64_t) a / ten_to_the_power_of(p)); + else if (load_character(s, i + 3) == 'd') + print_integer((uint64_t) a / ten_to_the_power_of(p)); + else + // precision only supported for %u and %d + return i + 4; if (p > 0) { // using integer_buffer here is ok since we are not using print_integer - itoa((uint64_t) a % ten_to_the_power_of(p), integer_buffer, 10, 0); + itoa((uint64_t) a % ten_to_the_power_of(p), integer_buffer, 10, 0, 0); p = p - string_length(integer_buffer); put_character('.'); @@ -2409,7 +2424,7 @@ void print_symbol(uint64_t symbol) { } void print_line_number(char* message, uint64_t line) { - printf4("%s: %s in %s in line %d: ", selfie_name, message, source_name, (char*) line); + printf4("%s: %s in %s in line %u: ", selfie_name, message, source_name, (char*) line); } void syntax_error_message(char* message) { @@ -4881,22 +4896,22 @@ void selfie_compile() { compile_cstar(); - printf4("%s: %d characters read in %d lines and %d comments\n", selfie_name, + printf4("%s: %u characters read in %u lines and %u comments\n", selfie_name, (char*) number_of_read_characters, (char*) line_number, (char*) number_of_comments); - printf4("%s: with %d(%.2d%%) characters in %d actual symbols\n", selfie_name, + printf4("%s: with %u(%.2u%%) characters in %u actual symbols\n", selfie_name, (char*) (number_of_read_characters - number_of_ignored_characters), (char*) fixed_point_percentage(fixed_point_ratio(number_of_read_characters, number_of_read_characters - number_of_ignored_characters, 4), 4), (char*) number_of_scanned_symbols); - printf4("%s: %d global variables, %d procedures, %d string literals\n", selfie_name, + printf4("%s: %u global variables, %u procedures, %u string literals\n", selfie_name, (char*) number_of_global_variables, (char*) number_of_procedures, (char*) number_of_strings); - printf6("%s: %d calls, %d assignments, %d while, %d if, %d return\n", selfie_name, + printf6("%s: %u calls, %u assignments, %u while, %u if, %u return\n", selfie_name, (char*) number_of_calls, (char*) number_of_assignments, (char*) number_of_while, @@ -4916,11 +4931,11 @@ void selfie_compile() { entry_point = ELF_ENTRY_POINT; - printf3("%s: symbol table search time was %d iterations on average and %d in total\n", selfie_name, + printf3("%s: symbol table search time was %u iterations on average and %u in total\n", selfie_name, (char*) (total_search_time / number_of_searches), (char*) total_search_time); - printf4("%s: %d bytes generated with %d instructions and %d bytes of data\n", selfie_name, + printf4("%s: %u bytes generated with %u instructions and %u bytes of data\n", selfie_name, (char*) binary_length, (char*) (code_length / INSTRUCTIONSIZE), (char*) (binary_length - code_length)); @@ -5275,7 +5290,7 @@ uint64_t get_total_percentage_of_nops() { } void print_instruction_counter(uint64_t total, uint64_t counter, char* mnemonics) { - printf3("%s: %d(%.2d%%)", + printf3("%s: %u(%.2u%%)", mnemonics, (char*) counter, (char*) fixed_point_percentage(fixed_point_ratio(total, counter, 4), 4)); @@ -5285,7 +5300,7 @@ void print_instruction_counter_with_nops(uint64_t total, uint64_t counter, uint6 print_instruction_counter(total, counter, mnemonics); if (run) - printf1("[%.2d%%]", (char*) fixed_point_percentage(fixed_point_ratio(counter, nops, 4), 4)); + printf1("[%.2u%%]", (char*) fixed_point_percentage(fixed_point_ratio(counter, nops, 4), 4)); } void print_instruction_counters() { @@ -5719,7 +5734,7 @@ void selfie_output(char* filename) { exit(EXITCODE_IOERROR); } - printf5("%s: %d bytes with %d instructions and %d bytes of data written into %s\n", selfie_name, + printf5("%s: %u bytes with %u instructions and %u bytes of data written into %s\n", selfie_name, (char*) (ELF_HEADER_LEN + binary_length), (char*) (code_length / INSTRUCTIONSIZE), (char*) (binary_length - code_length), @@ -5800,7 +5815,7 @@ void selfie_load() { if (signed_less_than(0, number_of_read_bytes)) { // check if we are really at EOF if (read(fd, binary_buffer, SIZEOFUINT64) == 0) { - printf5("%s: %d bytes with %d instructions and %d bytes of data loaded from %s\n", + printf5("%s: %u bytes with %u instructions and %u bytes of data loaded from %s\n", selfie_name, (char*) (ELF_HEADER_LEN + binary_length), (char*) (code_length / INSTRUCTIONSIZE), @@ -5854,7 +5869,7 @@ void implement_exit(uint64_t* context) { set_exit_code(context, sign_shrink(signed_int_exit_code, SYSCALL_BITWIDTH)); - printf4("%s: %s exiting with exit code %d and %.2dMB mallocated memory\n", selfie_name, + printf4("%s: %s exiting with exit code %d and %.2uMB mallocated memory\n", selfie_name, get_name(context), (char*) sign_extend(get_exit_code(context), SYSCALL_BITWIDTH), (char*) fixed_point_ratio(get_program_break(context) - get_original_break(context), MEGABYTE, 2)); @@ -5909,7 +5924,7 @@ void implement_read(uint64_t* context) { size = *(get_regs(context) + REG_A2); if (debug_read) - printf4("%s: trying to read %d bytes from file with descriptor %d into buffer at virtual address %p\n", selfie_name, + printf4("%s: trying to read %u bytes from file with descriptor %u into buffer at virtual address %p\n", selfie_name, (char*) size, (char*) fd, (char*) vbuffer); @@ -5971,7 +5986,7 @@ void implement_read(uint64_t* context) { set_pc(context, get_pc(context) + INSTRUCTIONSIZE); if (debug_read) - printf3("%s: actually read %d bytes from file with descriptor %d\n", selfie_name, + printf3("%s: actually read %u bytes from file with descriptor %u\n", selfie_name, (char*) read_total, (char*) fd); @@ -6030,7 +6045,7 @@ void implement_write(uint64_t* context) { size = *(get_regs(context) + REG_A2); if (debug_write) - printf4("%s: trying to write %d bytes from buffer at virtual address %p into file with descriptor %d\n", selfie_name, + printf4("%s: trying to write %u bytes from buffer at virtual address %p into file with descriptor %u\n", selfie_name, (char*) size, (char*) vbuffer, (char*) fd); @@ -6092,7 +6107,7 @@ void implement_write(uint64_t* context) { set_pc(context, get_pc(context) + INSTRUCTIONSIZE); if (debug_write) - printf3("%s: actually wrote %d bytes into file with descriptor %d\n", selfie_name, + printf3("%s: actually wrote %u bytes into file with descriptor %u\n", selfie_name, (char*) written_total, (char*) fd); @@ -6208,7 +6223,7 @@ void implement_openat(uint64_t* context) { *(get_regs(context) + REG_A0) = fd; if (debug_open) - printf5("%s: opened file %s with flags %x and mode %o returning file descriptor %d\n", selfie_name, + printf5("%s: opened file %s with flags %x and mode %o returning file descriptor %u\n", selfie_name, filename_buffer, (char*) flags, (char*) mode, @@ -6395,7 +6410,7 @@ uint64_t* do_switch(uint64_t* from_context, uint64_t* to_context, uint64_t timeo (char*) from_context, (char*) to_context); if (timer != TIMEROFF) - printf1(" to execute %d instructions", (char*) timer); + printf1(" to execute %u instructions", (char*) timer); println(); } @@ -6576,7 +6591,7 @@ void store_virtual_memory(uint64_t* table, uint64_t vaddr, uint64_t data) { void print_code_line_number_for_instruction(uint64_t address, uint64_t offset) { if (code_line_number != (uint64_t*) 0) - printf1("(~%d)", (char*) *(code_line_number + (address - offset) / INSTRUCTIONSIZE)); + printf1("(~%u)", (char*) *(code_line_number + (address - offset) / INSTRUCTIONSIZE)); } void print_code_context_for_instruction(uint64_t address) { @@ -7203,7 +7218,7 @@ void undo_ecall() { void print_data_line_number() { if (data_line_number != (uint64_t*) 0) - printf1("(~%d)", (char*) *(data_line_number + (pc - code_length) / REGISTERSIZE)); + printf1("(~%u)", (char*) *(data_line_number + (pc - code_length) / REGISTERSIZE)); } void print_data_context(uint64_t data) { @@ -7315,7 +7330,7 @@ void selfie_disassemble(uint64_t verbose) { output_name = (char*) 0; output_fd = 1; - printf5("%s: %d characters of assembly with %d instructions and %d bytes of data written into %s\n", selfie_name, + printf5("%s: %u characters of assembly with %u instructions and %u bytes of data written into %s\n", selfie_name, (char*) number_of_written_characters, (char*) (code_length / INSTRUCTIONSIZE), (char*) (binary_length - code_length), @@ -7768,7 +7783,7 @@ uint64_t print_per_instruction_counter(uint64_t total, uint64_t* counters, uint6 // CAUTION: we reset counter to avoid reporting it again *(counters + a / INSTRUCTIONSIZE) = 0; - printf3(",%d(%.2d%%)@%x", (char*) c, (char*) fixed_point_percentage(fixed_point_ratio(total, c, 4), 4), (char*) a); + printf3(",%u(%.2u%%)@%x", (char*) c, (char*) fixed_point_percentage(fixed_point_ratio(total, c, 4), 4), (char*) a); print_code_line_number_for_instruction(a, 0); return c; @@ -7780,13 +7795,13 @@ uint64_t print_per_instruction_counter(uint64_t total, uint64_t* counters, uint6 } void print_per_instruction_profile(char* message, uint64_t total, uint64_t* counters) { - printf3("%s%s%d", selfie_name, message, (char*) total); + printf3("%s%s%u", selfie_name, message, (char*) total); print_per_instruction_counter(total, counters, print_per_instruction_counter(total, counters, print_per_instruction_counter(total, counters, UINT64_MAX))); println(); } void print_profile() { - printf5("%s: summary: %d executed instructions [%.2d%% nops] and %.2dMB(%.2d%%) mapped memory\n", selfie_name, + printf5("%s: summary: %u executed instructions [%.2u%% nops] and %.2uMB(%.2u%%) mapped memory\n", selfie_name, (char*) get_total_number_of_instructions(), (char*) get_total_percentage_of_nops(), (char*) fixed_point_ratio(pused(), MEGABYTE, 2), @@ -8301,7 +8316,7 @@ uint64_t handle_system_call(uint64_t* context) { // TODO: exit only if all contexts have exited return EXIT; } else { - printf2("%s: unknown system call %d\n", selfie_name, (char*) a7); + printf2("%s: unknown system call %u\n", selfie_name, (char*) a7); set_exit_code(context, EXITCODE_UNKNOWNSYSCALL); @@ -8417,7 +8432,7 @@ uint64_t mixter(uint64_t* to_context, uint64_t mix) { uint64_t timeout; uint64_t* from_context; - printf2("mixter (%d%% mipster/%d%% hypster)\n", (char*) mix, (char*) (100 - mix)); + printf2("mixter (%u%% mipster/%u%% hypster)\n", (char*) mix, (char*) (100 - mix)); mslice = TIMESLICE; @@ -8647,7 +8662,7 @@ uint64_t selfie_run(uint64_t machine) { boot_loader(current_context); - printf3("%s: selfie executing %s with %dMB physical memory on ", selfie_name, + printf3("%s: selfie executing %s with %uMB physical memory on ", selfie_name, binary_name, (char*) (page_frame_memory / MEGABYTE)); diff --git a/tools/modeler.c b/tools/modeler.c index b1431d99..05946fba 100644 --- a/tools/modeler.c +++ b/tools/modeler.c @@ -2157,7 +2157,7 @@ uint64_t selfie_model() { output_name = (char*) 0; output_fd = 1; - printf3("%s: %d characters of model formulae written into %s\n", selfie_name, + printf3("%s: %u characters of model formulae written into %s\n", selfie_name, (char*) number_of_written_characters, model_name); diff --git a/tools/monster.c b/tools/monster.c index d0dbfede..f567f222 100644 --- a/tools/monster.c +++ b/tools/monster.c @@ -298,7 +298,7 @@ void implement_symbolic_exit(uint64_t* context) { print_code_context_for_instruction(pc); if (debug_merge) - printf1(" -> exiting context: %d", (char*) context); + printf1(" -> exiting context: %u", (char*) context); print("\n(check-sat)\n(get-model)\n(pop 1)\n"); } @@ -828,7 +828,7 @@ void constrain_beq() { if (debug_merge) { print("; a new context was created at "); print_code_context_for_instruction(pc); - printf4(" -> active context: %d, waiting context: %d (merge locations: %x, %x)\n", (char*) current_context, (char*) waiting_context, (char*) get_merge_location(current_context), (char*) get_merge_location(waiting_context)); + printf4(" -> active context: %u, waiting context: %u (merge locations: %x, %x)\n", (char*) current_context, (char*) waiting_context, (char*) get_merge_location(current_context), (char*) get_merge_location(waiting_context)); } // check if a context is waiting to be merged @@ -1116,7 +1116,7 @@ uint64_t handle_symbolic_system_call(uint64_t* context) { // TODO: exit only if all contexts have exited return EXIT; } else { - printf2("%s: unknown system call %d\n", selfie_name, (char*) a7); + printf2("%s: unknown system call %u\n", selfie_name, (char*) a7); set_exit_code(context, EXITCODE_UNKNOWNSYSCALL); @@ -1148,7 +1148,7 @@ uint64_t handle_symbolic_timer(uint64_t* context) { printf1("; timeout in ", path_condition); print_code_context_for_instruction(pc); if (debug_merge) - printf1(" -> timed out context: %d", (char*) context); + printf1(" -> timed out context: %u", (char*) context); println(); return EXIT; @@ -1217,7 +1217,7 @@ char* bv_constant(uint64_t value) { string = string_alloc(5 + 20 + 4); // 64-bit numbers require up to 20 decimal digits - sprintf1(string, "(_ bv%d 64)", (char*) value); + sprintf1(string, "(_ bv%u 64)", (char*) value); return string; } @@ -1227,7 +1227,7 @@ char* bv_variable(uint64_t bits) { string = string_alloc(10 + 2); // up to 64-bit variables require up to 2 decimal digits - sprintf1(string, "(_ BitVec %d)", (char*) bits); + sprintf1(string, "(_ BitVec %u)", (char*) bits); return string; } @@ -1237,7 +1237,7 @@ char* bv_zero_extension(uint64_t bits) { string = string_alloc(15 + 2); // up to 64-bit variables require up to 2 decimal digits - sprintf1(string, "(_ zero_extend %d)", (char*) (CPUBITWIDTH - bits)); + sprintf1(string, "(_ zero_extend %u)", (char*) (CPUBITWIDTH - bits)); return string; } @@ -1254,9 +1254,9 @@ char* smt_variable(char* prefix, uint64_t bits) { svar = string_alloc(string_length(prefix) + 20); // 64-bit numbers require up to 20 decimal digits - sprintf2(svar, "%s%d", prefix, (char*) variable_version); + sprintf2(svar, "%s%u", prefix, (char*) variable_version); - printf2("(declare-fun %s () (_ BitVec %d)); variable for ", svar, (char*) bits); + printf2("(declare-fun %s () (_ BitVec %u)); variable for ", svar, (char*) bits); print_code_context_for_instruction(pc); println(); @@ -1429,7 +1429,7 @@ void merge(uint64_t* active_context, uint64_t* mergeable_context, uint64_t locat print_code_context_for_instruction(location); if (debug_merge) - printf2(" -> active context: %d, mergeable context: %d", (char*) active_context, (char*) mergeable_context); + printf2(" -> active context: %u, mergeable context: %u", (char*) active_context, (char*) mergeable_context); println(); @@ -1939,7 +1939,7 @@ uint64_t compare_call_stacks(uint64_t* active_context, uint64_t* mergeable_conte entry_mergeable = get_call_stack(mergeable_context); if (debug_merge) - printf1("; Call stack of active context (%d):\n", (char*) active_context); + printf1("; Call stack of active context (%u):\n", (char*) active_context); while(entry_active) { @@ -1951,7 +1951,7 @@ uint64_t compare_call_stacks(uint64_t* active_context, uint64_t* mergeable_conte } if (debug_merge) - printf1("; Call stack of mergeable context (%d):\n", (char*) mergeable_context); + printf1("; Call stack of mergeable context (%u):\n", (char*) mergeable_context); while(entry_mergeable) { @@ -2024,8 +2024,8 @@ void monster(uint64_t* to_context) { printf1("; SMT-LIB formulae generated by %s for\n", selfie_name); printf1("; RISC-V code obtained from %s with\n", binary_name); - if (max_execution_depth) printf1("; %d", (char*) max_execution_depth); else print("; unbounded"); - printf1(" execution depth, branching limit of %d, and merging", (char*) beq_limit); + if (max_execution_depth) printf1("; %u", (char*) max_execution_depth); else print("; unbounded"); + printf1(" execution depth, branching limit of %u, and merging", (char*) beq_limit); if (merge_enabled) print(" enabled\n\n"); else print(" disabled\n\n"); print("(set-option :produce-models true)\n"); @@ -2037,7 +2037,7 @@ void monster(uint64_t* to_context) { while (1) { if (debug_merge) if (from_context != (uint64_t*) 0) - printf4("; switching from context %d to context %d (merge locations: %x, %x)\n", + printf4("; switching from context %u to context %u (merge locations: %x, %x)\n", (char*) from_context, (char*) to_context, (char*) get_merge_location(from_context), (char*) get_merge_location(to_context)); @@ -2167,7 +2167,7 @@ uint64_t selfie_run_symbolically() { boot_loader(current_context); - printf3("%s: monster symbolically executing %s with %dMB physical memory\n", selfie_name, + printf3("%s: monster symbolically executing %s with %uMB physical memory\n", selfie_name, binary_name, (char*) (page_frame_memory / MEGABYTE)); @@ -2189,7 +2189,7 @@ uint64_t selfie_run_symbolically() { print_profile(); - printf3("%s: %d characters of SMT-LIB formulae written into %s\n", selfie_name, + printf3("%s: %u characters of SMT-LIB formulae written into %s\n", selfie_name, (char*) number_of_written_characters, smt_name);