diff --git a/regression/cbmc-java/assume1/Assume1.class b/regression/cbmc-java/assume1/Assume1.class new file mode 100644 index 00000000000..b9a49bc9971 Binary files /dev/null and b/regression/cbmc-java/assume1/Assume1.class differ diff --git a/regression/cbmc-java/assume1/Assume1.java b/regression/cbmc-java/assume1/Assume1.java new file mode 100644 index 00000000000..4de0afd025b --- /dev/null +++ b/regression/cbmc-java/assume1/Assume1.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class Assume1 +{ + static void foo(int x) + { + CProver.assume(x>3); + assert x>0; + } +} diff --git a/regression/cbmc-java/assume1/test.desc b/regression/cbmc-java/assume1/test.desc new file mode 100644 index 00000000000..1f80a1c1e86 --- /dev/null +++ b/regression/cbmc-java/assume1/test.desc @@ -0,0 +1,8 @@ +CORE +Assume1.class +--function Assume1.foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/assume2/Assume2.class b/regression/cbmc-java/assume2/Assume2.class new file mode 100644 index 00000000000..36e09875d7d Binary files /dev/null and b/regression/cbmc-java/assume2/Assume2.class differ diff --git a/regression/cbmc-java/assume2/Assume2.java b/regression/cbmc-java/assume2/Assume2.java new file mode 100644 index 00000000000..6991167bfb8 --- /dev/null +++ b/regression/cbmc-java/assume2/Assume2.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class Assume2 +{ + static void foo(int x) + { + CProver.assume(x>3); + assert x>4; + } +} diff --git a/regression/cbmc-java/assume2/test.desc b/regression/cbmc-java/assume2/test.desc new file mode 100644 index 00000000000..35a954116f8 --- /dev/null +++ b/regression/cbmc-java/assume2/test.desc @@ -0,0 +1,8 @@ +CORE +Assume2.class +--function Assume2.foo +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/assume3/Assume3.class b/regression/cbmc-java/assume3/Assume3.class new file mode 100644 index 00000000000..916ad4065fb Binary files /dev/null and b/regression/cbmc-java/assume3/Assume3.class differ diff --git a/regression/cbmc-java/assume3/Assume3.java b/regression/cbmc-java/assume3/Assume3.java new file mode 100644 index 00000000000..895deee9ca0 --- /dev/null +++ b/regression/cbmc-java/assume3/Assume3.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class Assume3 +{ + public static void main(String[] args) + { + CProver.assume(false); + assert false; + } +} diff --git a/regression/cbmc-java/assume3/test.desc b/regression/cbmc-java/assume3/test.desc new file mode 100644 index 00000000000..0ad8c00399f --- /dev/null +++ b/regression/cbmc-java/assume3/test.desc @@ -0,0 +1,8 @@ +CORE +Assume3.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/covered1/covered1.class b/regression/cbmc-java/covered1/covered1.class new file mode 100644 index 00000000000..7cb91496b7d Binary files /dev/null and b/regression/cbmc-java/covered1/covered1.class differ diff --git a/regression/cbmc-java/covered1/covered1.java b/regression/cbmc-java/covered1/covered1.java new file mode 100644 index 00000000000..018e65336a6 --- /dev/null +++ b/regression/cbmc-java/covered1/covered1.java @@ -0,0 +1,37 @@ +public class covered1 +{ + // this is a variable + int x=1; + //these are two, one line off the first + int y=2; + int z=3; + //this is part of static init + static int z0=0; + + //another non-static + int a; + int b; + static boolean odd; + + static + { + odd=(z0+1)%2==0; + } + + covered1(int a, int b) + { + this.a=a*b; + this.b=a+b; + if(this.a==a) + z0++; + else + odd=!odd; + } + // at the back + int z1=2; + int z2=3; + int z3=4; + // + static int z4=5; + int z5=5; +} diff --git a/regression/cbmc-java/covered1/test.desc b/regression/cbmc-java/covered1/test.desc new file mode 100644 index 00000000000..32af766bdb7 --- /dev/null +++ b/regression/cbmc-java/covered1/test.desc @@ -0,0 +1,19 @@ +CORE +covered1.class +--cover location --json-ui --show-properties +^EXIT=0$ +^SIGNAL=0$ +.*\"coveredLines\": \"22\",$ +.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$ +.*\"coveredLines\": \"26\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"29\",$ +.*\"coveredLines\": \"9,18\",$ +.*\"coveredLines\": \"18\",$ +.*\"coveredLines\": \"18\",$ +.*\"coveredLines\": \"18,35\",$ +-- +^warning: ignoring diff --git a/scripts/bash-autocomplete/.gitignore b/scripts/bash-autocomplete/.gitignore new file mode 100644 index 00000000000..1e0acedc4f2 --- /dev/null +++ b/scripts/bash-autocomplete/.gitignore @@ -0,0 +1 @@ +cbmc.sh diff --git a/scripts/bash-autocomplete/Readme.md b/scripts/bash-autocomplete/Readme.md new file mode 100644 index 00000000000..00101d99159 --- /dev/null +++ b/scripts/bash-autocomplete/Readme.md @@ -0,0 +1,31 @@ +# CBMC Autocomplete Scripts for Bash +This directory contains an autocomplete script for bash. +## Installation +1. Compile cbmc and + +2. `cd scripts/bash-autocomplete` + +3. `./extract-switches.sh` + +4. Put the following at the end of you in your `~/.bashrc`, with the directories adapted to your directory structure: + ```bash + cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh + if [ -f $cbmcautocomplete ]; then + . $cbmcautocomplete + fi + ``` +## Usage +As with the usual autocomplete in bash, start typing a switch to complete it, for example: +``` +cbmc --clas +``` +will complete to +``` +cbmc --classpath +``` + +## Features implemented + +* Completing all switches +* Completing values for `--cover`, `--mm` and `--arch` +* When completing a name of a file to analyze, only files with supported extensions are shown. diff --git a/scripts/bash-autocomplete/cbmc.sh.template b/scripts/bash-autocomplete/cbmc.sh.template new file mode 100644 index 00000000000..cbd64762b2d --- /dev/null +++ b/scripts/bash-autocomplete/cbmc.sh.template @@ -0,0 +1,43 @@ +#!/bin/bash +_cbmc_autocomplete() +{ + #list of all switches cbmc has. IMPORTANT: in the template file, this variable must be defined on line 5. + local switches="" + #word on which the cursor is + local cur=${COMP_WORDS[COMP_CWORD]} + #previous word (in case it is a switch with a parameter) + local prev=${COMP_WORDS[COMP_CWORD-1]} + + #check if the command before cursor is a switch that takes parameters, if yes, + #offer a choice of parameters + case "$prev" in + --cover) #for coverage we list the options explicitly + COMPREPLY=( $( compgen -W "assertion path branch location decision condition mcdc cover" -- $cur ) ) + return 0 + ;; + --mm) #for memory models we list the options explicitly + COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) ) + return 0 + ;; + --arch) #for architecture we list the options explicitly + COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) ) + return 0 + ;; + -I|--classpath|-cp|--outfile|--existing-coverage|--graphml-cex) + #a switch that takes a file parameter of which we don't know an extension + #TODO probably we can do more for -I, --classpath, -cp + _filedir + return 0 + ;; + esac + + #complete a switch from a standard list, if the parameter under cursor starts with a hyphen + if [[ "$cur" == -* ]]; then + COMPREPLY=( $( compgen -W "$switches" -- $cur ) ) + return 0 + fi + + #if none of the above applies, offer directories and files that we can analyze + _filedir "@(class|jar|cpp|cc|c\+\+|ii|cxx|c|i|gb)" +} +complete -F _cbmc_autocomplete cbmc diff --git a/scripts/bash-autocomplete/extract_switches.sh b/scripts/bash-autocomplete/extract_switches.sh new file mode 100755 index 00000000000..e000b469bea --- /dev/null +++ b/scripts/bash-autocomplete/extract_switches.sh @@ -0,0 +1,48 @@ +#!/bin/bash +echo "Compiling the helper file to extract the raw list of parameters from cbmc" +g++ -c -MMD -MP -std=c++11 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c -o tmp.o 2> pragma.txt + +retval=$? + +#clean up compiled files, we don't need them. +rm tmp.o 2> /dev/null +rm tmp.d 2> /dev/null + +#check if compilation went fine +if [ $retval -ne 0 ]; then + echo "Problem compiling the helper file, parameter list not extracted." + exit 1; +fi + +echo "Converting the raw parameter list to the format required by autocomplete scripts" +rawstring=`sed "s/^.*pragma message: \(.*\)/\1/" pragma.txt` +#delete pragma file, we won't need it +rm pragma.txt 2> /dev/null + +#now the main bit, convert from raw format to a proper list of switches +cleanstring=`( + #extract 2-hyphen switches, such as --foo + #grep for '(foo)' expressions, and then use sed to remove parantheses and put '--' at the start + (echo $rawstring | grep -o "([^)]*)" | sed "s/^.\(.*\).$/--\1/") ; + #extract 1-hyphen switches, such as -F + #use sed to remove all (foo) expressions, then you're left with switches and ':', so grep the colons out and then use sed to include the '-' + (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9]" | sed "s/\(.*\)/-\1/") + ) | tr '\n' ' '` + +#sanity check that there is only one line of output +if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then + echo "Problem converting the parameter list to the correct format, I was expecting one line but either got 0 or >2. This is likely to be an error in this conversion script." + exit 1; +fi + +#sanity check that there are no dangerous characters +echo $cleanstring | grep -q "[^a-zA-Z0-9 -]" +if [ $? -eq 0 ]; then + echo "Problem converting the parameter list to the correct format, illegal characters detected. This is likely to be an error in this conversion script." + exit 1; +fi + +echo "Injecting the parameter list to the autocomplete file." +sed "5 s/.*/ local switches=\"$cleanstring\"/" cbmc.sh.template > cbmc.sh + +rm pragma.txt 2> /dev/null diff --git a/scripts/bash-autocomplete/switch_extractor_helper.c b/scripts/bash-autocomplete/switch_extractor_helper.c new file mode 100644 index 00000000000..4d9cc2e56fe --- /dev/null +++ b/scripts/bash-autocomplete/switch_extractor_helper.c @@ -0,0 +1,3 @@ +#include "cbmc/cbmc_parse_options.h" + +#pragma message CBMC_OPTIONS diff --git a/src/Makefile b/src/Makefile index cc2a5831d8e..6d2c3f0a8fd 100644 --- a/src/Makefile +++ b/src/Makefile @@ -84,4 +84,12 @@ glucose-download: @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) @rm glucose-syrup.tgz -.PHONY: minisat2-download glucose-download +cprover-jar-build: + @echo "Building org.cprover.jar" + @(cd java_bytecode/library/; \ + mkdir -p target; \ + javac -d target/ `find src/ -name "*.java"`; \ + cd target; jar cf org.cprover.jar `find . -name "*.class"`; \ + mv org.cprover.jar ../../../) + +.PHONY: minisat2-download glucose-download cprover-jar-build diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index f2d17617ccd..ef64691b4a3 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -13,9 +13,12 @@ Date: May 2016 #include #include +#include +#include #include #include +#include #include "cover.h" @@ -32,6 +35,11 @@ class basic_blockst if(next_is_target || it->is_target()) block_count++; + const irep_idt &line=it->source_location.get_line(); + if(!line.empty()) + block_line_cover_map[block_count] + .insert(unsafe_string2unsigned(id2string(line))); + block_map[it]=block_count; if(!it->source_location.is_nil() && @@ -39,7 +47,26 @@ class basic_blockst source_location_map[block_count]=it->source_location; next_is_target= +#if 0 + // Disabled for being too messy it->is_goto() || it->is_function_call() || it->is_assume(); +#else + it->is_goto() || it->is_function_call(); +#endif + } + + // create list of covered lines as CSV string and set as property of source + // location of basic block, compress to ranges if applicable + format_number_ranget format_lines; + for(const auto &cover_set : block_line_cover_map) + { + assert(!cover_set.second.empty()); + std::vector + line_list{cover_set.second.begin(), cover_set.second.end()}; + + std::string covered_lines=format_lines(line_list); + source_location_map[cover_set.first] + .set_basic_block_covered_lines(covered_lines); } } @@ -51,6 +78,11 @@ class basic_blockst typedef std::map source_location_mapt; source_location_mapt source_location_map; + // map block numbers to set of line numbers + typedef std::map > + block_line_cover_mapt; + block_line_cover_mapt block_line_cover_map; + inline unsigned operator[](goto_programt::const_targett t) { return block_map[t]; @@ -299,7 +331,7 @@ std::set collect_mcdc_controlling_nested( const std::set &decisions) { // To obtain the 1st-level controlling conditions - std::set controlling = collect_mcdc_controlling(decisions); + std::set controlling=collect_mcdc_controlling(decisions); std::set result; // For each controlling condition, to check if it contains @@ -490,7 +522,7 @@ void remove_repetition(std::set &exprs) **/ for(auto &y : new_exprs) { - bool iden = true; + bool iden=true; for(auto &c : conditions) { std::set signs1=sign_of_expr(c, x); @@ -532,7 +564,7 @@ void remove_repetition(std::set &exprs) } // update the original ''exprs'' - exprs = new_exprs; + exprs=new_exprs; } /// To evaluate the value of expr ''src'', according to the atomic expr values @@ -667,7 +699,8 @@ bool is_mcdc_pair( if(diff_count==1) return true; - else return false; + else + return false; } /// To check if we can find the mcdc pair of the input ''expr_set'' regarding @@ -769,7 +802,8 @@ void minimize_mcdc_controlling( { controlling=new_controlling; } - else break; + else + break; } } @@ -1057,9 +1091,12 @@ void instrument_cover_goals( const std::set decisions=collect_decisions(i_it); std::set both; - std::set_union(conditions.begin(), conditions.end(), - decisions.begin(), decisions.end(), - inserter(both, both.end())); + std::set_union( + conditions.begin(), + conditions.end(), + decisions.begin(), + decisions.end(), + inserter(both, both.end())); const source_locationt source_location=i_it->source_location; @@ -1146,7 +1183,10 @@ void instrument_cover_goals( f_it->second.is_hidden()) continue; - instrument_cover_goals(symbol_table, f_it->second.body, criterion); + instrument_cover_goals( + symbol_table, + f_it->second.body, + criterion); } } diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index fa9ebf63359..7e67a6bf5b1 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -148,7 +148,8 @@ void dump_ct::operator()(std::ostream &os) // we don't want to dump in full all definitions; in particular // do not dump anonymous types that are defined in system headers - if((!tag_added || symbol.is_type) && ignore(symbol)) + if((!tag_added || symbol.is_type) && + system_symbols.is_symbol_internal_symbol(symbol, system_headers)) continue; bool inserted=symbols_sorted.insert(name_str).second; @@ -317,7 +318,7 @@ void dump_ct::convert_compound( ns.lookup(to_symbol_type(type).get_identifier()); DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol"); - if(!ignore(symbol)) + if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers)) convert_compound(symbol.type, unresolved, recursive, os); } else if(type.id()==ID_c_enum_tag) @@ -326,7 +327,7 @@ void dump_ct::convert_compound( ns.lookup(to_c_enum_tag_type(type).get_identifier()); DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol"); - if(!ignore(symbol)) + if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers)) convert_compound(symbol.type, unresolved, recursive, os); } else if(type.id()==ID_array || type.id()==ID_pointer) @@ -581,195 +582,6 @@ void dump_ct::convert_compound_enum( os << ";\n\n"; } -#define ADD_TO_SYSTEM_LIBRARY(v, header) \ - for(size_t i=0; isecond); - return true; - } - - if(use_all_headers && - has_prefix(file_str, "/usr/include/")) - { - if(file_str.find("/bits/")==std::string::npos) - { - // Do not include transitive includes of system headers! - std::string::size_type prefix_len=std::string("/usr/include/").size(); - system_headers.insert(file_str.substr(prefix_len)); - } - - return true; - } - - return false; -} - void dump_ct::cleanup_decl( code_declt &decl, std::list &local_static, diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index 255cb88677e..3c6fab3e652 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include class dump_ct { @@ -35,7 +36,7 @@ class dump_ct use_all_headers(use_all_headers) { if(use_system_headers) - init_system_library_map(); + system_symbols=system_library_symbolst(); } virtual ~dump_ct() @@ -57,9 +58,7 @@ class dump_ct std::set system_headers; - typedef std::unordered_map - system_library_mapt; - system_library_mapt system_library_map; + system_library_symbolst system_symbols; typedef std::unordered_map declared_enum_constants_mapt; @@ -89,7 +88,6 @@ class dump_ct std::string type_to_string(const typet &type); std::string expr_to_string(const exprt &expr); - bool ignore(const symbolt &symbol); bool ignore(const typet &type); static std::string indent(const unsigned n) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index b807b21dc9a..92995c74252 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -539,7 +539,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("interpreter")) { status() << "Starting interpreter" << eom; - interpreter(symbol_table, goto_functions); + interpreter(symbol_table, goto_functions, get_message_handler()); return 0; } diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index a66b408a3c9..6e2bd969e57 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -57,6 +57,7 @@ SRC = basic_blocks.cpp \ slice_global_inits.cpp \ string_abstraction.cpp \ string_instrumentation.cpp \ + system_library_symbols.cpp \ vcd_goto_trace.cpp \ wp.cpp \ write_goto_binary.cpp \ diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 4485aed5151..2e6921cb3de 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -51,9 +51,10 @@ void goto_trace_stept::output( case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break; case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break; case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break; - case goto_trace_stept::typet::FUNCTION_RETURN: - out << "FUNCTION RETURN"; break; - default: assert(false); + case goto_trace_stept::typet::FUNCTION_RETURN: out << "FUNCTION RETURN"; break; + default: + out << "unknown type: " << type << std::endl; + assert(false); } if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO) diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 4c8a3accc8a..16010145b61 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -174,6 +174,13 @@ class goto_tracet steps.push_back(step); } + // retrieves the final step in the trace for manipulation + // (used to fill a trace from code, hence non-const) + inline goto_trace_stept &get_last_step() + { + return steps.back(); + } + // delete all steps after (not including) s void trim_after(stepst::iterator s) { diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 8a5c23f1a62..1f9e22f485a 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -12,18 +12,65 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include +#include #include #include +#include +#include +#include +#include +#include #include "interpreter.h" #include "interpreter_class.h" +#include "remove_returns.h" + +const size_t interpretert::npos=std::numeric_limits::max(); void interpretert::operator()() +{ + status() << "0- Initialize:" << eom; + initialize(true); + try + { + status() << "Type h for help\n" << eom; + + while(!done) + command(); + + status() << total_steps << "- Program End.\n" << eom; + } + catch (const char *e) + { + error() << e << "\n" << eom; + } + + while(!done) + command(); +} + +/*******************************************************************\ + +Function: interpretert::initialize + + Inputs: + + Outputs: + + Purpose: Initializes the memory map of the interpreter and + [optionally] runs up to the entry point (thus doing + the cprover initialization) + +\*******************************************************************/ + +void interpretert::initialize(bool init) { build_memory_map(); + total_steps=0; const goto_functionst::function_mapt::const_iterator main_it=goto_functions.function_map.find(goto_functionst::entry_point()); @@ -35,36 +82,54 @@ void interpretert::operator()() if(!goto_function.body_available()) throw "main has no body"; - PC=goto_function.body.instructions.begin(); + pc=goto_function.body.instructions.begin(); function=main_it; done=false; - - while(!done) + if(init) { + stack_depth=call_stack.size()+1; show_state(); - command(); - if(!done) + step(); + while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos)) + { + show_state(); step(); + } + while(!done && (call_stack.size()==0)) + { + show_state(); + step(); + } + clear_input_flags(); + input_vars.clear(); } } +/// displays the current position of the pc and corresponding code void interpretert::show_state() { - std::cout << "\n----------------------------------------------------\n"; + if(!show) + return; + status() << "\n" + << total_steps+1 + << " ----------------------------------------------------\n"; - if(PC==function->second.body.instructions.end()) + if(pc==function->second.body.instructions.end()) { - std::cout << "End of function `" - << function->first << "'\n"; + status() << "End of function `" << function->first << "'\n"; } else function->second.body.output_instruction( - ns, function->first, std::cout, PC); + ns, + function->first, + status(), + pc); - std::cout << '\n'; + status() << eom; } +/// reads a user command and executes it. void interpretert::command() { #define BUFSIZE 100 @@ -76,42 +141,140 @@ void interpretert::command() } char ch=tolower(command[0]); - if(ch=='q') done=true; + else if(ch=='h') + { + status() + << "Interpreter help\n" + << "h: display this menu\n" + << "j: output json trace\n" + << "m: output memory dump\n" + << "o: output goto trace\n" + << "q: quit\n" + << "r: run until completion\n" + << "s#: step a number of instructions\n" + << "sa: step across a function\n" + << "so: step out of a function\n" + << eom; + } + else if(ch=='j') + { + jsont json_steps; + convert(ns, steps, json_steps); + ch=tolower(command[1]); + if(ch==' ') + { + std::ofstream file; + file.open(command+2); + if(file.is_open()) + { + json_steps.output(file); + file.close(); + return; + } + } + json_steps.output(result()); + } + else if(ch=='m') + { + ch=tolower(command[1]); + print_memory(ch=='i'); + } + else if(ch=='o') + { + ch=tolower(command[1]); + if(ch==' ') + { + std::ofstream file; + file.open(command+2); + if(file.is_open()) + { + steps.output(ns, file); + file.close(); + return; + } + } + steps.output(ns, result()); + } + else if(ch=='r') + { + ch=tolower(command[1]); + initialize(ch!='0'); + } + else if((ch=='s') || (ch==0)) + { + num_steps=1; + stack_depth=npos; + ch=tolower(command[1]); + if(ch=='e') + num_steps=npos; + else if(ch=='o') + stack_depth=call_stack.size(); + else if(ch=='a') + stack_depth=call_stack.size()+1; + else + { + num_steps=atoi(command+1); + if(num_steps==0) + num_steps=1; + } + while(!done && ((num_steps==npos) || ((num_steps--)>0))) + { + step(); + show_state(); + } + while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos)) + { + step(); + show_state(); + } + return; + } + show_state(); } +/// executes a single step and updates the program counter void interpretert::step() { - if(PC==function->second.body.instructions.end()) + total_steps++; + if(pc==function->second.body.instructions.end()) { if(call_stack.empty()) done=true; else { - PC=call_stack.top().return_PC; + pc=call_stack.top().return_pc; function=call_stack.top().return_function; - stack_pointer=call_stack.top().old_stack_pointer; + // TODO: this increases memory size quite quickly. + // Should check alternatives call_stack.pop(); } return; } - next_PC=PC; - next_PC++; + next_pc=pc; + next_pc++; - switch(PC->type) + steps.add_step(goto_trace_stept()); + goto_trace_stept &trace_step=steps.get_last_step(); + trace_step.thread_nr=thread_id; + trace_step.pc=pc; + switch(pc->type) { case GOTO: + trace_step.type=goto_trace_stept::GOTO; execute_goto(); break; case ASSUME: + trace_step.type=goto_trace_stept::ASSUME; execute_assume(); break; case ASSERT: + trace_step.type=goto_trace_stept::ASSERT; execute_assert(); break; @@ -120,38 +283,46 @@ void interpretert::step() break; case DECL: + trace_step.type=goto_trace_stept::DECL; execute_decl(); break; case SKIP: case LOCATION: + trace_step.type=goto_trace_stept::LOCATION; + break; case END_FUNCTION: + trace_step.type=goto_trace_stept::FUNCTION_RETURN; break; case RETURN: + trace_step.type=goto_trace_stept::FUNCTION_RETURN; if(call_stack.empty()) throw "RETURN without call"; // NOLINT(readability/throw) - if(PC->code.operands().size()==1 && + if(pc->code.operands().size()==1 && call_stack.top().return_value_address!=0) { - std::vector rhs; - evaluate(PC->code.op0(), rhs); + mp_vectort rhs; + evaluate(pc->code.op0(), rhs); assign(call_stack.top().return_value_address, rhs); } - next_PC=function->second.body.instructions.end(); + next_pc=function->second.body.instructions.end(); break; case ASSIGN: + trace_step.type=goto_trace_stept::ASSIGNMENT; execute_assign(); break; case FUNCTION_CALL: + trace_step.type=goto_trace_stept::FUNCTION_CALL; execute_function_call(); break; case START_THREAD: + trace_step.type=goto_trace_stept::SPAWN; throw "START_THREAD not yet implemented"; // NOLINT(readability/throw) case END_THREAD: @@ -159,44 +330,89 @@ void interpretert::step() break; case ATOMIC_BEGIN: + trace_step.type=goto_trace_stept::ATOMIC_BEGIN; throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw) case ATOMIC_END: + trace_step.type=goto_trace_stept::ATOMIC_END; throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw) case DEAD: - throw "DEAD not yet implemented"; // NOLINT(readability/throw) - + trace_step.type=goto_trace_stept::DEAD; + break; + case THROW: + trace_step.type=goto_trace_stept::GOTO; + while(!done && (pc->type!=CATCH)) + { + if(pc==function->second.body.instructions.end()) + { + if(call_stack.empty()) + done=true; + else + { + pc=call_stack.top().return_pc; + function=call_stack.top().return_function; + call_stack.pop(); + } + } + else + { + next_pc=pc; + next_pc++; + } + } + break; + case CATCH: + break; default: throw "encountered instruction with undefined instruction type"; } - - PC=next_PC; + pc=next_pc; } +/// executes a goto instruction void interpretert::execute_goto() { - if(evaluate_boolean(PC->guard)) + if(evaluate_boolean(pc->guard)) { - if(PC->targets.empty()) + if(pc->targets.empty()) throw "taken goto without target"; - if(PC->targets.size()>=2) + if(pc->targets.size()>=2) throw "non-deterministic goto encountered"; - next_PC=PC->targets.front(); + next_pc=pc->targets.front(); } } +/// executes side effects of 'other' instructions void interpretert::execute_other() { - const irep_idt &statement=PC->code.get_statement(); - + const irep_idt &statement=pc->code.get_statement(); if(statement==ID_expression) { - assert(PC->code.operands().size()==1); - std::vector rhs; - evaluate(PC->code.op0(), rhs); + assert(pc->code.operands().size()==1); + mp_vectort rhs; + evaluate(pc->code.op0(), rhs); + } + else if(statement==ID_array_set) + { + mp_vectort tmp, rhs; + evaluate(pc->code.op1(), tmp); + mp_integer address=evaluate_address(pc->code.op0()); + size_t size=get_size(pc->code.op0().type()); + while(rhs.size()code.get_statement()==ID_decl); + assert(pc->code.get_statement()==ID_decl); +} + +/*******************************************************************\ + +Function: interpretert::get_component_id + + Inputs: an object and a memory offset + + Outputs: + + Purpose: retrieves the member at offset + +\*******************************************************************/ + +irep_idt interpretert::get_component_id( + const irep_idt &object, + unsigned offset) +{ + const symbolt &symbol=ns.lookup(object); + const typet real_type=ns.follow(symbol.type); + if(real_type.id()!=ID_struct) + throw "request for member of non-struct"; + + const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet::componentst &components=struct_type.components(); + for(struct_typet::componentst::const_iterator it=components.begin(); + it!=components.end(); it++) + { + if(offset<=0) + return it->id(); + size_t size=get_size(it->type()); + offset-=size; + } + return object; +} + +/*******************************************************************\ + +Function: interpretert::get_type + + Inputs: + + Outputs: + + Purpose: returns the type object corresponding to id + +\*******************************************************************/ + +typet interpretert::get_type(const irep_idt &id) const +{ + dynamic_typest::const_iterator it=dynamic_types.find(id); + if(it==dynamic_types.end()) + return symbol_table.lookup(id).type; + return it->second; +} + +/*******************************************************************\ + +Function: interpretert::get_value + + Inputs: + + Outputs: + + Purpose: retrives the constant value at memory location offset + as an object of type type + +\*******************************************************************/ + +exprt interpretert::get_value( + const typet &type, + std::size_t offset, + bool use_non_det) +{ + const typet real_type=ns.follow(type); + if(real_type.id()==ID_struct) + { + exprt result=struct_exprt(real_type); + const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet::componentst &components=struct_type.components(); + + // Retrieve the values for the individual members + result.reserve_operands(components.size()); + for(struct_typet::componentst::const_iterator it=components.begin(); + it!=components.end(); it++) + { + size_t size=get_size(it->type()); + const exprt operand=get_value(it->type(), offset); + offset+=size; + result.copy_to_operands(operand); + } + return result; + } + else if(real_type.id()==ID_array) + { + // Get size of array + exprt result=array_exprt(to_array_type(real_type)); + const exprt &size_expr=static_cast(type.find(ID_size)); + size_t subtype_size=get_size(type.subtype()); + mp_integer mp_count; + to_integer(size_expr, mp_count); + unsigned count=integer2unsigned(mp_count); + + // Retrieve the value for each member in the array + result.reserve_operands(count); + for(unsigned i=0; i=0)) + return side_effect_expr_nondett(type); + mp_vectort rhs; + rhs.push_back(memory[offset].value); + return get_value(type, rhs); } +/*******************************************************************\ + + Function: interpretert::get_value + + Inputs: + + Outputs: + + Purpose: returns the value at offset in the form of type given a + memory buffer rhs which is typically a structured type + +\*******************************************************************/ + +exprt interpretert::get_value( + const typet &type, + mp_vectort &rhs, + std::size_t offset) +{ + const typet real_type=ns.follow(type); + assert(!rhs.empty()); + + if(real_type.id()==ID_struct) + { + exprt result=struct_exprt(real_type); + const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet::componentst &components=struct_type.components(); + + // Retrieve the values for the individual members + result.reserve_operands(components.size()); + for(const struct_union_typet::componentt &expr : components) + { + size_t size=get_size(expr.type()); + const exprt operand=get_value(expr.type(), rhs, offset); + offset+=size; + result.copy_to_operands(operand); + } + return result; + } + else if(real_type.id()==ID_array) + { + exprt result(ID_constant, type); + const exprt &size_expr=static_cast(type.find(ID_size)); + + // Get size of array + size_t subtype_size=get_size(type.subtype()); + mp_integer mp_count; + to_integer(size_expr, mp_count); + unsigned count=integer2unsigned(mp_count); + + // Retrieve the value for each member in the array + result.reserve_operands(count); + for(unsigned i=0; i object count " << memory.size() << eom; + throw "interpreter: reading from invalid pointer"; + } + else if(real_type.id()==ID_string) + { + // Strings are currently encoded by their irep_idt ID. + return constant_exprt( + irep_idt(rhs[offset].to_long(), 0), + type); + } + // Retrieve value of basic data type + return from_integer(rhs[offset], type); +} + +/// executes the assign statement at the current pc value void interpretert::execute_assign() { const code_assignt &code_assign= - to_code_assign(PC->code); + to_code_assign(pc->code); - std::vector rhs; + mp_vectort rhs; evaluate(code_assign.rhs(), rhs); if(!rhs.empty()) { mp_integer address=evaluate_address(code_assign.lhs()); - unsigned size=get_size(code_assign.lhs().type()); + size_t size=get_size(code_assign.lhs().type()); if(size!=rhs.size()) - std::cout << "!! failed to obtain rhs (" - << rhs.size() << " vs. " - << size << ")\n"; + error() << "!! failed to obtain rhs (" + << rhs.size() << " vs. " + << size << ")\n" + << eom; else + { + goto_trace_stept &trace_step=steps.get_last_step(); assign(address, rhs); + trace_step.full_lhs=code_assign.lhs(); + + // TODO: need to look at other cases on ssa_exprt + // (dereference should be handled on ssa) + if(ssa_exprt::can_build_identifier(trace_step.full_lhs)) + { + trace_step.lhs_object=ssa_exprt(trace_step.full_lhs); + } + trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs); + trace_step.lhs_object_value=trace_step.full_lhs_value; + } + } + else if(code_assign.rhs().id()==ID_side_effect) + { + side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs()); + if(side_effect.get_statement()==ID_nondet) + { + unsigned address=integer2unsigned(evaluate_address(code_assign.lhs())); + size_t size=get_size(code_assign.lhs().type()); + for(size_t i=0; i &rhs) + const mp_vectort &rhs) { - for(unsigned i=0; iguard)) + if(!evaluate_boolean(pc->guard)) throw "assumption failed"; } void interpretert::execute_assert() { - if(!evaluate_boolean(PC->guard)) - throw "assertion failed"; + if(!evaluate_boolean(pc->guard)) + { + if((target_assert==pc) || stop_on_assertion) + throw "program assertion reached"; + else if(show) + error() << "assertion failed at " << pc->location_number + << "\n" << eom; + } } void interpretert::execute_function_call() { const code_function_callt &function_call= - to_code_function_call(PC->code); + to_code_function_call(pc->code); // function to be called mp_integer a=evaluate_address(function_call.function()); @@ -270,8 +774,12 @@ void interpretert::execute_function_call() else if(a>=memory.size()) throw "out-of-range function call"; + // Retrieve the empty last trace step struct we pushed for this step + // of the interpreter run to fill it with the corresponding data + goto_trace_stept &trace_step=steps.get_last_step(); const memory_cellt &cell=memory[integer2size_t(a)]; const irep_idt &identifier=cell.identifier; + trace_step.identifier=identifier; const goto_functionst::function_mapt::const_iterator f_it= goto_functions.function_map.find(identifier); @@ -289,7 +797,7 @@ void interpretert::execute_function_call() return_value_address=0; // values of the arguments - std::vector > argument_values; + std::vector argument_values; argument_values.resize(function_call.arguments().size()); @@ -303,7 +811,7 @@ void interpretert::execute_function_call() call_stack.push(stack_framet()); stack_framet &frame=call_stack.top(); - frame.return_PC=next_PC; + frame.return_pc=next_pc; frame.return_function=function; frame.old_stack_pointer=stack_pointer; frame.return_value_address=return_value_address; @@ -315,24 +823,7 @@ void interpretert::execute_function_call() for(const auto &id : locals) { const symbolt &symbol=ns.lookup(id); - unsigned size=get_size(symbol.type); - - if(size!=0) - { - frame.local_map[id]=stack_pointer; - - for(unsigned i=0; i=memory.size()) - memory.resize(address+1); - memory[address].value=0; - memory[address].identifier=id; - memory[address].offset=i; - } - - stack_pointer+=size; - } + frame.local_map[id]=integer2unsigned(build_memory_map(id, symbol.type)); } // assign the arguments @@ -342,7 +833,7 @@ void interpretert::execute_function_call() if(argument_values.size()second.body.instructions.begin(); + next_pc=f_it->second.body.instructions.begin(); } else - throw "no body for "+id2string(identifier); + { + list_input_varst::iterator it= + function_input_vars.find(function_call.function().get(ID_identifier)); + if(it!=function_input_vars.end()) + { + mp_vectort value; + assert(!it->second.empty()); + assert(!it->second.front().return_assignments.empty()); + evaluate(it->second.front().return_assignments.back().value, value); + if(return_value_address>0) + { + assign(return_value_address, value); + } + it->second.pop_front(); + return; + } + if(show) + error() << "no body for "+id2string(identifier) << eom; + } } +/// Creates a memory map of all static symbols in the program void interpretert::build_memory_map() { // put in a dummy for NULL memory.resize(1); memory[0].offset=0; memory[0].identifier="NULL-OBJECT"; + memory[0].initialized=0; + + num_dynamic_objects=0; + dynamic_types.clear(); // now do regular static symbols for(const auto &s : symbol_table.symbols) @@ -376,7 +890,7 @@ void interpretert::build_memory_map() void interpretert::build_memory_map(const symbolt &symbol) { - unsigned size=0; + size_t size=0; if(symbol.type.id()==ID_code) { @@ -393,17 +907,110 @@ void interpretert::build_memory_map(const symbolt &symbol) memory.resize(address+size); memory_map[symbol.name]=address; - for(unsigned i=0; i(type.find(ID_size)); + mp_vectort computed_size; + evaluate(size_expr, computed_size); + if(computed_size.size()==1 && + computed_size[0]>=0) + { + result() << "Concretized array with size " << computed_size[0] + << eom; + return array_typet(type.subtype(), + constant_exprt::integer_constant(computed_size[0].to_ulong())); + } + else + { + error() << "Failed to concretize variable array" + << eom; + } + } + return type; +} + +/*******************************************************************\ + +Function: interpretert::build_memory_map + + Inputs: + + Outputs: Updtaes the memory map to include variable id if it does + not exist + + Purpose: Populates dynamic entries of the memory map + +\*******************************************************************/ + +mp_integer interpretert::build_memory_map( + const irep_idt &id, + const typet &type) +{ + typet alloc_type=concretize_type(type); + size_t size=get_size(alloc_type); + auto it=dynamic_types.find(id); + + if(it!=dynamic_types.end()) + { + unsigned offset=1; + unsigned address=memory_map[id]; + while(memory[address+offset].offset>0) offset++; + + // current size <= size already recorded + if(size<=offset) + return memory_map[id]; + } + + // The current size is bigger then the one previously recorded + // in the memory map + + if(size==0) + size=1; // This is a hack to create existence + + unsigned address=memory.size(); + memory.resize(address+size); + memory_map[id]=address; + dynamic_types.insert(std::pair(id, alloc_type)); + + for(size_t i=0; i>>>>>> fef1fed6b... update interpreter { if(type.id()==ID_struct) { @@ -427,7 +1034,7 @@ unsigned interpretert::get_size(const typet &type) const const union_typet::componentst &components= to_union_type(type).components(); - unsigned max_size=0; + size_t max_size=0; for(const auto &comp : components) { @@ -443,26 +1050,93 @@ unsigned interpretert::get_size(const typet &type) const { const exprt &size_expr=static_cast(type.find(ID_size)); - unsigned subtype_size=get_size(type.subtype()); + size_t subtype_size=get_size(type.subtype()); - mp_integer i; - if(!to_integer(size_expr, i)) - return subtype_size*integer2unsigned(i); - else - return subtype_size; + mp_vectort i; + evaluate(size_expr, i); + if(i.size()==1) + { + // Go via the binary representation to reproduce any + // overflow behaviour. + exprt size_const=from_integer(i[0], size_expr.type()); + mp_integer size_mp; + assert(!to_integer(size_const, size_mp)); + return subtype_size*integer2unsigned(size_mp); + } + return subtype_size; } else if(type.id()==ID_symbol) { return get_size(ns.follow(type)); } + return 1; +} + +/******************************************************************* \ + +Function: interpretert::get_value + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt interpretert::get_value(const irep_idt &id) +{ + // The dynamic type and the static symbol type may differ for VLAs, + // where the symbol carries a size expression and the dynamic type + // registry contains its actual length. + auto findit=dynamic_types.find(id); + typet get_type; + if(findit!=dynamic_types.end()) + get_type=findit->second; else - return 1; + get_type=symbol_table.lookup(id).type; + + symbol_exprt symbol_expr(id, get_type); + mp_integer whole_lhs_object_address=evaluate_address(symbol_expr); + + return get_value(get_type, integer2unsigned(whole_lhs_object_address)); } void interpreter( const symbol_tablet &symbol_table, - const goto_functionst &goto_functions) + const goto_functionst &goto_functions, + message_handlert &message_handler) { - interpretert interpreter(symbol_table, goto_functions); + interpretert interpreter( + symbol_table, + goto_functions, + message_handler); interpreter(); } + +/*******************************************************************\ + +Function: interpretert::print_memory + + Inputs: + + Outputs: + + Purpose: Prints the current state of the memory map + Since messaget mdofifies class members, print functions are nonconst + +\*******************************************************************/ + +void interpretert::print_memory(bool input_flags) +{ + for(size_t i=0; i(cell.initialized) << ")" + << eom; + debug() << eom; + } +} diff --git a/src/goto-programs/interpreter.h b/src/goto-programs/interpreter.h index 20113a54fc6..8d598852b1a 100644 --- a/src/goto-programs/interpreter.h +++ b/src/goto-programs/interpreter.h @@ -12,10 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_H #define CPROVER_GOTO_PROGRAMS_INTERPRETER_H +#include + #include "goto_functions.h" void interpreter( const symbol_tablet &symbol_table, - const goto_functionst &goto_functions); + const goto_functionst &goto_functions, + message_handlert &message_handler); #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_H diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 9938862bb92..562df8d6d1e 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -17,24 +17,93 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "goto_functions.h" +#include "goto_trace.h" +#include "json_goto_trace.h" +#include "util/message.h" -class interpretert +class interpretert:public messaget { public: interpretert( const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions): + const goto_functionst &_goto_functions, + message_handlert &_message_handler): + messaget(_message_handler), symbol_table(_symbol_table), ns(_symbol_table), - goto_functions(_goto_functions) + goto_functions(_goto_functions), + stop_on_assertion(false) { + show=true; } void operator()(); + void print_memory(bool input_flags); + + // An assertion that identifier 'id' carries value in some particular context. + // Used to record parameter (id) assignment (value) lists for function calls. + struct function_assignmentt + { + irep_idt id; + exprt value; + }; + + // A list of such assignments. + typedef std::vector function_assignmentst; + + typedef std::vector mp_vectort; + + // Maps an assignment id to the name of the parameter being assigned + typedef std::pair assignment_idt; + + // Identifies an expression before and after some change; + typedef std::pair diff_pairt; + + // Records a diff between an assignment pre and post conditions + typedef std::map side_effects_differencet; + + // A entry in the input_valuest map + typedef std::pair input_entryt; + + // List of the input variables with their corresponding initial values + typedef std::map input_valuest; + + // List of dynamically allocated symbols that are not in the symbol table + typedef std::map dynamic_typest; + + // An assignment list annotated with the calling context. + struct function_assignments_contextt + { + irep_idt calling_function; + function_assignmentst return_assignments; + function_assignmentst param_assignments; + }; + + // list_input_varst maps function identifiers onto a vector of [name = value] + // assignments per call to that function. + typedef std::list + function_assignments_contextst; + typedef std::map > + list_input_varst; + + const dynamic_typest &get_dynamic_types() { return dynamic_types; } protected: + struct trace_stack_entryt + { + irep_idt func_name; + mp_integer this_address; + irep_idt capture_symbol; + bool is_super_call; + std::vector param_values; + }; + typedef std::vector trace_stackt; + const symbol_tablet &symbol_table; + + // This is a cache so that we don't have to create it when a call needs it const namespacet ns; + const goto_functionst &goto_functions; typedef std::unordered_map memory_mapt; @@ -46,16 +115,40 @@ class interpretert irep_idt identifier; unsigned offset; mp_integer value; + // Initialized is annotated even during reads + // Set to 1 when written-before-read, -1 when read-before-written + mutable char initialized; }; typedef std::vector memoryt; - memoryt memory; + typedef std::map parameter_sett; + // mapping -> value + typedef std::pair struct_member_idt; + typedef std::map struct_valuest; + + + // The memory is being annotated/reshaped even during reads + // (ie to find a read-before-write location) thus memory + // properties need to be mutable to avoid making all calls nonconst + mutable memoryt memory; std::size_t stack_pointer; void build_memory_map(); void build_memory_map(const symbolt &symbol); - unsigned get_size(const typet &type) const; + mp_integer build_memory_map(const irep_idt &id, const typet &type); + typet concretize_type(const typet &type); + size_t get_size(const typet &type); + + irep_idt get_component_id(const irep_idt &object, unsigned offset); + typet get_type(const irep_idt &id) const; + exprt get_value( + const typet &type, + std::size_t offset=0, + bool use_non_det=false); + exprt get_value(const typet &type, mp_vectort &rhs, std::size_t offset=0); + exprt get_value(const irep_idt &id); + void step(); void execute_assert(); @@ -65,21 +158,26 @@ class interpretert void execute_function_call(); void execute_other(); void execute_decl(); + void clear_input_flags(); + + void allocate( + mp_integer address, + size_t size); void assign( mp_integer address, - const std::vector &rhs); + const mp_vectort &rhs); void read( mp_integer address, - std::vector &dest) const; + mp_vectort &dest) const; - void command(); + virtual void command(); class stack_framet { public: - goto_programt::const_targett return_PC; + goto_programt::const_targett return_pc; goto_functionst::function_mapt::const_iterator return_function; mp_integer return_value_address; memory_mapt local_map; @@ -87,27 +185,56 @@ class interpretert }; typedef std::stack call_stackt; + call_stackt call_stack; + input_valuest input_vars; + list_input_varst function_input_vars; goto_functionst::function_mapt::const_iterator function; - goto_programt::const_targett PC, next_PC; + goto_programt::const_targett pc, next_pc, target_assert; + goto_tracet steps; bool done; - - bool evaluate_boolean(const exprt &expr) const + bool show; + bool stop_on_assertion; + static const size_t npos; + size_t num_steps; + size_t total_steps; + + dynamic_typest dynamic_types; + int num_dynamic_objects; + size_t stack_depth; + int thread_id; + + bool evaluate_boolean(const exprt &expr) { - std::vector v; + mp_vectort v; evaluate(expr, v); if(v.size()!=1) throw "invalid boolean value"; return v.front()!=0; } + bool count_type_leaves( + const typet &source_type, + mp_integer &result); + + bool byte_offset_to_memory_offset( + const typet &source_type, + mp_integer byte_offset, + mp_integer &result); + + bool memory_offset_to_byte_offset( + const typet &source_type, + mp_integer cell_offset, + mp_integer &result); + void evaluate( const exprt &expr, - std::vector &dest) const; + mp_vectort &dest); - mp_integer evaluate_address(const exprt &expr) const; + mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false); + void initialize(bool init); void show_state(); }; diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 43a072cfaf4..a8da762a7ea 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -11,41 +11,366 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include +#include +#include #include "interpreter_class.h" +/// reads a memory address and loads it into the dest variable +/// marks cell as read before written if cell has never been written void interpretert::read( mp_integer address, - std::vector &dest) const + mp_vectort &dest) const { // copy memory region - for(auto &d : dest) + for(size_t i=0; i0) + cell.initialized=0; + } +} + +/*******************************************************************\ + +Function: interpretert::count_type_leaves + + Inputs: Type + + Outputs: Number of leaf primitive types; returns true on error + + Purpose: + +\*******************************************************************/ + +bool interpretert::count_type_leaves(const typet &ty, mp_integer &result) +{ + if(ty.id()==ID_struct) + { + result=0; + mp_integer subtype_count; + for(const auto &component : to_struct_type(ty).components()) + { + if(count_type_leaves(component.type(), subtype_count)) + return true; + result+=subtype_count; + } + return false; + } + else if(ty.id()==ID_array) + { + const auto &at=to_array_type(ty); + mp_vectort array_size_vec; + evaluate(at.size(), array_size_vec); + if(array_size_vec.size()!=1) + return true; + mp_integer subtype_count; + if(count_type_leaves(at.subtype(), subtype_count)) + return true; + result=array_size_vec[0]*subtype_count; + return false; + } + else + { + result=1; + return false; + } +} + +/*******************************************************************\ + +Function: interpretert::byte_offset_to_memory_offset + + Inputs: 'source_type', 'offset' (unit: bytes), + + Outputs: Offset into a vector of interpreter values; returns true on error + + Purpose: Supposing the caller has an mp_vector representing + a value with type 'source_type', this yields the offset into that + vector at which to find a value at *byte* address 'offset'. + We need this because the interpreter's memory map uses unlabelled + variable-width values -- for example, a C value { { 1, 2 }, 3, 4 } + of type struct { int x[2]; char y; unsigned long z; } + would be represented [1,2,3,4], with the source type needed alongside + to figure out which member is targeted by a byte-extract operation. + +\*******************************************************************/ + +bool interpretert::byte_offset_to_memory_offset( + const typet &source_type, + mp_integer offset, + mp_integer &result) +{ + if(source_type.id()==ID_struct) + { + const auto &st=to_struct_type(source_type); + const struct_typet::componentst &components=st.components(); + member_offset_iterator component_offsets(st, ns); + mp_integer previous_member_offsets=0; + for(; component_offsets->firstsecond!=-1 && + component_offsets->second<=offset; + ++component_offsets) + { + const auto &component_type=components[component_offsets->first].type(); + mp_integer component_byte_size=pointer_offset_size(component_type, ns); + if(component_byte_size<0) + return true; + if((component_offsets->second+component_byte_size)>offset) + { + mp_integer subtype_result; + bool ret=byte_offset_to_memory_offset( + component_type, + offset-(component_offsets->second), + subtype_result); + result=previous_member_offsets+subtype_result; + return ret; + } + else + { + mp_integer component_count; + if(count_type_leaves(component_type, component_count)) + return true; + previous_member_offsets+=component_count; + } + } + // Ran out of struct members, or struct contained a variable-length field. + return true; + } + else if(source_type.id()==ID_array) + { + const auto &at=to_array_type(source_type); + mp_vectort array_size_vec; + evaluate(at.size(), array_size_vec); + if(array_size_vec.size()!=1) + return true; + mp_integer array_size=array_size_vec[0]; + mp_integer elem_size_bytes=pointer_offset_size(at.subtype(), ns); + if(elem_size_bytes<=0) + return true; + mp_integer elem_size_leaves; + if(count_type_leaves(at.subtype(), elem_size_leaves)) + return true; + mp_integer this_idx=offset/elem_size_bytes; + if(this_idx>=array_size_vec[0]) + return true; + mp_integer subtype_result; + bool ret=byte_offset_to_memory_offset( + at.subtype(), + offset%elem_size_bytes, + subtype_result); + result=subtype_result+(elem_size_leaves*this_idx); + return ret; + } + else + { + result=0; + // Can't currently subdivide a primitive. + return offset!=0; + } +} + +/*******************************************************************\ + +Function: interpretert::memory_offset_to_byte_offset + + Inputs: An interpreter memory offset and the type to interpret that memory + + Outputs: The corresponding byte offset. Returns true on error + + Purpose: Similarly to the above, the interpreter's memory objects contain + mp_integers that represent variable-sized struct members. This + counts the size of type leaves to determine the byte offset + corresponding to a memory offset. + +\*******************************************************************/ + +bool interpretert::memory_offset_to_byte_offset( + const typet &source_type, + mp_integer cell_offset, + mp_integer &result) +{ + if(source_type.id()==ID_struct) + { + const auto &st=to_struct_type(source_type); + const struct_typet::componentst &components=st.components(); + member_offset_iterator offsets(st, ns); + mp_integer previous_member_sizes; + for(; offsets->firstsecond!=-1; ++offsets) + { + const auto &component_type=components[offsets->first].type(); + mp_integer component_count; + if(count_type_leaves(component_type, component_count)) + return true; + if(component_count>cell_offset) + { + mp_integer subtype_result; + bool ret=memory_offset_to_byte_offset( + component_type, + cell_offset, + subtype_result); + result=previous_member_sizes+subtype_result; + return ret; + } + else + { + cell_offset-=component_count; + mp_integer component_size=pointer_offset_size(component_type, ns); + if(component_size<0) + return true; + previous_member_sizes+=component_size; + } + } + // Ran out of members, or member of indefinite size + return true; + } + else if(source_type.id()==ID_array) + { + const auto &at=to_array_type(source_type); + mp_vectort array_size_vec; + evaluate(at.size(), array_size_vec); + if(array_size_vec.size()!=1) + return true; + mp_integer elem_size=pointer_offset_size(at.subtype(), ns); + if(elem_size==-1) + return true; + mp_integer elem_count; + if(count_type_leaves(at.subtype(), elem_count)) + return true; + mp_integer this_idx=cell_offset/elem_count; + if(this_idx>=array_size_vec[0]) + return true; + mp_integer subtype_result; + bool ret= + memory_offset_to_byte_offset(at.subtype(), + cell_offset%elem_count, + subtype_result); + result=subtype_result+(elem_size*this_idx); + return ret; + } + else + { + // Primitive type. + result=0; + return cell_offset!=0; } } void interpretert::evaluate( const exprt &expr, - std::vector &dest) const + mp_vectort &dest) { if(expr.id()==ID_constant) { if(expr.type().id()==ID_struct) { + dest.reserve(get_size(expr.type())); + bool error=false; + + forall_operands(it, expr) + { + if(it->type().id()==ID_code) + continue; + + size_t sub_size=get_size(it->type()); + if(sub_size==0) + continue; + + mp_vectort tmp; + evaluate(*it, tmp); + + if(tmp.size()==sub_size) + { + for(size_t i=0; itype().id()==ID_code) continue; - unsigned sub_size=get_size(it->type()); + size_t sub_size=get_size(it->type()); if(sub_size==0) continue; - std::vector tmp; + mp_vectort tmp; evaluate(*it, tmp); if(tmp.size()==sub_size) { - for(unsigned i=0; i tmp0, tmp1; + mp_vectort tmp0, tmp1; evaluate(expr.op0(), tmp0); evaluate(expr.op1(), tmp1); @@ -151,7 +671,7 @@ void interpretert::evaluate( forall_operands(it, expr) { - std::vector tmp; + mp_vectort tmp; evaluate(*it, tmp); if(tmp.size()==1 && tmp.front()!=0) @@ -170,20 +690,20 @@ void interpretert::evaluate( if(expr.operands().size()!=3) throw "if expects three operands"; - std::vector tmp0, tmp1, tmp2; + mp_vectort tmp0, tmp1; evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - evaluate(expr.op2(), tmp2); - if(tmp0.size()==1 && tmp1.size()==1 && tmp2.size()==1) + if(tmp0.size()==1) { - const mp_integer &op0=tmp0.front(); - const mp_integer &op1=tmp1.front(); - const mp_integer &op2=tmp2.front(); - - dest.push_back(op0!=0?op1:op2); + if(tmp0.front()!=0) + evaluate(expr.op1(), tmp1); + else + evaluate(expr.op2(), tmp1); } + if(tmp1.size()==1) + dest.push_back(tmp1.front()); + return; } else if(expr.id()==ID_and) @@ -195,7 +715,7 @@ void interpretert::evaluate( forall_operands(it, expr) { - std::vector tmp; + mp_vectort tmp; evaluate(*it, tmp); if(tmp.size()==1 && tmp.front()==0) @@ -214,7 +734,7 @@ void interpretert::evaluate( if(expr.operands().size()!=1) throw id2string(expr.id())+" expects one operand"; - std::vector tmp; + mp_vectort tmp; evaluate(expr.op0(), tmp); if(tmp.size()==1) @@ -228,7 +748,7 @@ void interpretert::evaluate( forall_operands(it, expr) { - std::vector tmp; + mp_vectort tmp; evaluate(*it, tmp); if(tmp.size()==1) result+=tmp.front(); @@ -260,7 +780,7 @@ void interpretert::evaluate( forall_operands(it, expr) { - std::vector tmp; + mp_vectort tmp; evaluate(*it, tmp); if(tmp.size()==1) { @@ -296,7 +816,7 @@ void interpretert::evaluate( if(expr.operands().size()!=2) throw "- expects two operands"; - std::vector tmp0, tmp1; + mp_vectort tmp0, tmp1; evaluate(expr.op0(), tmp0); evaluate(expr.op1(), tmp1); @@ -309,7 +829,7 @@ void interpretert::evaluate( if(expr.operands().size()!=2) throw "/ expects two operands"; - std::vector tmp0, tmp1; + mp_vectort tmp0, tmp1; evaluate(expr.op0(), tmp0); evaluate(expr.op1(), tmp1); @@ -322,7 +842,7 @@ void interpretert::evaluate( if(expr.operands().size()!=1) throw "unary- expects one operand"; - std::vector tmp0; + mp_vectort tmp0; evaluate(expr.op0(), tmp0); if(tmp0.size()==1) @@ -337,22 +857,130 @@ void interpretert::evaluate( dest.push_back(evaluate_address(expr.op0())); return; } + else if(expr.id()==ID_pointer_offset) + { + if(expr.operands().size()!=1) + throw "pointer_offset expects one operand"; + if(expr.op0().type().id()!=ID_pointer) + throw "pointer_offset expects a pointer operand"; + mp_vectort result; + evaluate(expr.op0(), result); + if(result.size()==1) + { + // Return the distance, in bytes, between the address returned + // and the beginning of the underlying object. + mp_integer address=result[0]; + if(address>0 && address0) + { + dest.insert(dest.end(), + extract_from.begin()+memory_offset.to_long(), + extract_from.begin()+(memory_offset+target_type_leaves).to_long()); + return; + } + } + } + } else if(expr.id()==ID_dereference || expr.id()==ID_index || expr.id()==ID_symbol || expr.id()==ID_member) { - mp_integer a=evaluate_address(expr); - dest.resize(get_size(expr.type())); - read(a, dest); - return; + mp_integer address=evaluate_address( + expr, + true); // fail quietly + if(address.is_zero() && expr.id()==ID_index) + { + // Try reading from a constant array: + mp_vectort idx; + evaluate(expr.op1(), idx); + if(idx.size()==1) + { + mp_integer read_from_index=idx[0]; + if(expr.op0().id()==ID_array) + { + const auto &ops=expr.op0().operands(); + assert(read_from_index.is_long()); + if(read_from_index>=0 && read_from_index tmp; + mp_vectort tmp; evaluate(expr.op0(), tmp); if(tmp.size()==1) @@ -378,38 +1006,50 @@ void interpretert::evaluate( dest.push_back(binary2integer(s, false)); return; } - else if(expr.type().id()==ID_bool) + else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool)) { dest.push_back(value!=0); return; } } } - else if(expr.id()==ID_ashr) + else if((expr.id()==ID_array) || (expr.id()==ID_array_of)) { - if(expr.operands().size()!=2) - throw "ashr expects two operands"; - - std::vector tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - - if(tmp0.size()==1 && tmp1.size()==1) - dest.push_back(tmp0.front()/power(2, tmp1.front())); - + forall_operands(it, expr) + { + evaluate(*it, dest); + } return; } - - std::cout << "!! failed to evaluate expression: " - << from_expr(ns, function->first, expr) - << '\n'; + else if(expr.id()==ID_nil) + { + dest.push_back(0); + return; + } + else if(expr.id()==ID_infinity) + { + if(expr.type().id()==ID_signedbv) + { + error() << "Infinite size arrays not supported" << eom; + return; + } + } + error() << "!! failed to evaluate expression: " + << from_expr(ns, function->first, expr) << "\n" + << expr.id() << "[" << expr.type().id() << "]" + << eom; } -mp_integer interpretert::evaluate_address(const exprt &expr) const +mp_integer interpretert::evaluate_address( + const exprt &expr, + bool fail_quietly) { if(expr.id()==ID_symbol) { - const irep_idt &identifier=expr.get(ID_identifier); + const irep_idt &identifier= + is_ssa_expr(expr) ? + to_ssa_expr(expr).get_original_name() : + expr.get(ID_identifier); interpretert::memory_mapt::const_iterator m_it1= memory_map.find(identifier); @@ -425,13 +1065,16 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const if(m_it2!=call_stack.top().local_map.end()) return m_it2->second; } + mp_integer address=memory.size(); + build_memory_map(to_symbol_expr(expr).get_identifier(), expr.type()); + return address; } else if(expr.id()==ID_dereference) { if(expr.operands().size()!=1) throw "dereference expects one operand"; - std::vector tmp0; + mp_vectort tmp0; evaluate(expr.op0(), tmp0); if(tmp0.size()==1) @@ -442,11 +1085,15 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const if(expr.operands().size()!=2) throw "index expects two operands"; - std::vector tmp1; + mp_vectort tmp1; evaluate(expr.op1(), tmp1); if(tmp1.size()==1) - return evaluate_address(expr.op0())+tmp1.front(); + { + auto base=evaluate_address(expr.op0(), fail_quietly); + if(!base.is_zero()) + return base+tmp1.front(); + } } else if(expr.id()==ID_member) { @@ -469,12 +1116,44 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const offset+=get_size(comp.type()); } - return evaluate_address(expr.op0())+offset; + auto base=evaluate_address(expr.op0(), fail_quietly); + if(!base.is_zero()) + return base+offset; } - - std::cout << "!! failed to evaluate address: " + else if(expr.id()==ID_byte_extract_little_endian || + expr.id()==ID_byte_extract_big_endian) + { + if(expr.operands().size()!=2) + throw "byte_extract should have two operands"; + mp_vectort extract_offset; + evaluate(expr.op1(), extract_offset); + mp_vectort extract_from; + evaluate(expr.op0(), extract_from); + if(extract_offset.size()==1 && !extract_from.empty()) + { + mp_integer memory_offset; + if(!byte_offset_to_memory_offset(expr.op0().type(), + extract_offset[0], memory_offset)) + return evaluate_address(expr.op0(), fail_quietly)+memory_offset; + } + } + else if(expr.id()==ID_if) + { + mp_vectort result; + if_exprt address_cond( + expr.op0(), + address_of_exprt(expr.op1()), + address_of_exprt(expr.op2())); + evaluate(address_cond, result); + if(result.size()==1) + return result[0]; + } + if(!fail_quietly) + { + error() << "!! failed to evaluate address: " << from_expr(ns, function->first, expr) - << '\n'; + << eom; + } return 0; } diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index a052a8aaecb..9afa3f99eba 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -109,6 +109,10 @@ void show_properties_json( json_properties.push_back(jsont()).make_object(); json_property["name"]=json_stringt(id2string(property_id)); json_property["class"]=json_stringt(id2string(property_class)); + if(!source_location.get_basic_block_covered_lines().empty()) + json_property["coveredLines"]= + json_stringt( + id2string(source_location.get_basic_block_covered_lines())); json_property["sourceLocation"]=json(source_location); json_property["description"]=json_stringt(id2string(description)); json_property["expression"]= diff --git a/src/goto-programs/system_library_symbols.cpp b/src/goto-programs/system_library_symbols.cpp new file mode 100644 index 00000000000..7e885a8f150 --- /dev/null +++ b/src/goto-programs/system_library_symbols.cpp @@ -0,0 +1,364 @@ +/*******************************************************************\ + +Module: Goto Programs + +Author: Thomas Kiley + +\*******************************************************************/ + +#include "system_library_symbols.h" +#include +#include +#include +#include + +system_library_symbolst::system_library_symbolst() +{ + init_system_library_map(); +} + +/*******************************************************************\ + +Function: system_library_symbolst::init_system_library_map + +Inputs: + +Outputs: + +Purpose: To generate a map of header file names -> list of symbols + The symbol names are reserved as the header and source files + will be compiled in to the goto program. + +\*******************************************************************/ + +void system_library_symbolst::init_system_library_map() +{ + // ctype.h + std::list ctype_syms= + { + "isalnum", "isalpha", "isblank", "iscntrl", "isdigit", "isgraph", + "islower", "isprint", "ispunct", "isspace", "isupper", "isxdigit", + "tolower", "toupper" + }; + add_to_system_library("ctype.h", ctype_syms); + + // fcntl.h + std::list fcntl_syms= + { + "creat", "fcntl", "open" + }; + add_to_system_library("fcntl.h", fcntl_syms); + + // locale.h + std::list locale_syms= + { + "setlocale" + }; + add_to_system_library("locale.h", locale_syms); + + // math.h + std::list math_syms= + { + "acos", "acosh", "asin", "asinh", "atan", "atan2", "atanh", + "cbrt", "ceil", "copysign", "cos", "cosh", "erf", "erfc", "exp", + "exp2", "expm1", "fabs", "fdim", "floor", "fma", "fmax", "fmin", + "fmod", "fpclassify", "fpclassifyl", "fpclassifyf", "frexp", + "hypot", "ilogb", "isfinite", "isinf", "isinff", "isinfl", + "isnan", "isnanf", "isnanl", "isnormal", "j0", "j1", "jn", + "ldexp", "lgamma", "llrint", "llround", "log", "log10", "log1p", + "log2", "logb", "lrint", "lround", "modf", "nan", "nearbyint", + "nextafter", "pow", "remainder", "remquo", "rint", "round", + "scalbln", "scalbn", "signbit", "sin", "sinh", "sqrt", "tan", + "tanh", "tgamma", "trunc", "y0", "y1", "yn" + }; + add_to_system_library("math.h", math_syms); + + // for some reason the math functions can sometimes be prefixed with + // a double underscore + std::list underscore_math_syms; + for(const irep_idt &math_sym : math_syms) + { + std::ostringstream underscore_id; + underscore_id << "__" << math_sym; + underscore_math_syms.push_back(irep_idt(underscore_id.str())); + } + add_to_system_library("math.h", underscore_math_syms); + + // pthread.h + std::list pthread_syms= + { + "pthread_cleanup_pop", "pthread_cleanup_push", + "pthread_cond_broadcast", "pthread_cond_destroy", + "pthread_cond_init", "pthread_cond_signal", + "pthread_cond_timedwait", "pthread_cond_wait", "pthread_create", + "pthread_detach", "pthread_equal", "pthread_exit", + "pthread_getspecific", "pthread_join", "pthread_key_delete", + "pthread_mutex_destroy", "pthread_mutex_init", + "pthread_mutex_lock", "pthread_mutex_trylock", + "pthread_mutex_unlock", "pthread_once", "pthread_rwlock_destroy", + "pthread_rwlock_init", "pthread_rwlock_rdlock", + "pthread_rwlock_unlock", "pthread_rwlock_wrlock", + "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared", + "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared", + "pthread_self", "pthread_setspecific", + /* non-public struct types */ + "tag-__pthread_internal_list", "tag-__pthread_mutex_s", + "pthread_mutex_t" + }; + add_to_system_library("pthread.h", pthread_syms); + + // setjmp.h + std::list setjmp_syms= + { + "_longjmp", "_setjmp", "longjmp", "longjmperror", "setjmp", + "siglongjmp", "sigsetjmp" + }; + add_to_system_library("setjmp.h", setjmp_syms); + + // stdio.h + std::list stdio_syms= + { + "asprintf", "clearerr", "fclose", "fdopen", "feof", "ferror", + "fflush", "fgetc", "fgetln", "fgetpos", "fgets", "fgetwc", + "fgetws", "fileno", "fopen", "fprintf", "fpurge", "fputc", + "fputs", "fputwc", "fputws", "fread", "freopen", "fropen", + "fscanf", "fseek", "fsetpos", "ftell", "funopen", "fwide", + "fwopen", "fwprintf", "fwrite", "getc", "getchar", "getdelim", + "getline", "gets", "getw", "getwc", "getwchar", "mkdtemp", + "mkstemp", "mktemp", "perror", "printf", "putc", "putchar", + "puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf", + "setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf", + "sprintf", "sscanf", "swprintf", "sys_errlist", + "sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc", + "vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf", + "vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf", + "vwprintf", "wprintf", + /* non-public struct types */ + "tag-__sFILE", "tag-__sbuf", // OS X + "tag-_IO_FILE", "tag-_IO_marker", // Linux + }; + add_to_system_library("stdio.h", stdio_syms); + + // stdlib.h + std::list stdlib_syms= + { + "abort", "abs", "atexit", "atof", "atoi", "atol", "atoll", + "bsearch", "calloc", "div", "exit", "free", "getenv", "labs", + "ldiv", "llabs", "lldiv", "malloc", "mblen", "mbstowcs", "mbtowc", + "qsort", "rand", "realloc", "srand", "strtod", "strtof", "strtol", + "strtold", "strtoll", "strtoul", "strtoull", "system", "wcstombs", + "wctomb" + }; + add_to_system_library("stdlib.h", stdlib_syms); + + // string.h + std::list string_syms= + { + "memset", "strcasecmp", "strcat", "strchr", "strcmp", "strcpy", + "strcspn", "strdup", "strerror", "strlen", "strncasecmp", + "strncat", "strncmp", "strncpy", "strpbrk", "strrchr", "strspn", + "strstr", "strtok" + }; + add_to_system_library("string.h", string_syms); + + // time.h + std::list time_syms= + { + "asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime", + "gmtime_r", "localtime", "localtime_r", "mktime", "strftime", + /* non-public struct types */ + "tag-timespec", "tag-timeval", "tag-tm" + }; + add_to_system_library("time.h", time_syms); + + // unistd.h + std::list unistd_syms= + { + "_exit", "access", "alarm", "chdir", "chown", "close", "dup", + "dup2", "execl", "execle", "execlp", "execv", "execve", "execvp", + "fork", "fpathconf", "getcwd", "getegid", "geteuid", "getgid", + "getgroups", "getlogin", "getpgrp", "getpid", "getppid", "getuid", + "isatty", "link", "lseek", "pathconf", "pause", "pipe", "read", + "rmdir", "setgid", "setpgid", "setsid", "setuid", "sleep", + "sysconf", "tcgetpgrp", "tcsetpgrp", "ttyname", "ttyname_r", + "unlink", "write" + }; + add_to_system_library("unistd.h", unistd_syms); + + // sys/select.h + std::list sys_select_syms= + { + "select", + /* non-public struct types */ + "fd_set" + }; + add_to_system_library("sys/select.h", sys_select_syms); + + // sys/socket.h + std::list sys_socket_syms= + { + "accept", "bind", "connect", + /* non-public struct types */ + "tag-sockaddr" + }; + add_to_system_library("sys/socket.h", sys_socket_syms); + + // sys/stat.h + std::list sys_stat_syms= + { + "fstat", "lstat", "stat", + /* non-public struct types */ + "tag-stat" + }; + add_to_system_library("sys/stat.h", sys_stat_syms); + + std::list fenv_syms= + { + "fenv_t", "fexcept_t", "feclearexcept", "fegetexceptflag", + "feraiseexcept", "fesetexceptflag", "fetestexcept", + "fegetround", "fesetround", "fegetenv", "feholdexcept", + "fesetenv", "feupdateenv" + }; + add_to_system_library("fenv.h", fenv_syms); + + std::list errno_syms= + { + "__error", "__errno_location", "__errno" + }; + add_to_system_library("errno.c", errno_syms); + + std::list noop_syms= + { + "__noop" + }; + add_to_system_library("noop.c", noop_syms); + +#if 0 + // sys/types.h + std::list sys_types_syms= + { + }; + add_to_system_library("sys/types.h", sys_types_syms); +#endif + + // sys/wait.h + std::list sys_wait_syms= + { + "wait", "waitpid" + }; + add_to_system_library("sys/wait.h", sys_wait_syms); +} + +/*******************************************************************\ + +Function: system_library_symbolst::add_to_system_library + +Inputs: + header_file - the name of the header file the symbol came from + symbols - a list of the names of the symbols in the header file + +Outputs: + +Purpose: To add the symbols from a specific header file to the + system library map. The symbol is used as the key so that + we can easily look up symbols. + +\*******************************************************************/ + +void system_library_symbolst::add_to_system_library( + irep_idt header_file, + std::list symbols) +{ + for(const irep_idt &symbol : symbols) + { + system_library_map[symbol]=header_file; + } +} + + +/*******************************************************************\ + +Function: system_library_symbolst::is_symbol_internal_symbol + +Inputs: + symbol - the symbol to check + +Outputs: True if the symbol is an internal symbol. If specific system + headers need to be included, the out_system_headers will contain + the headers. + +Purpose: To find out if a symbol is an internal symbol. + +\*******************************************************************/ + +bool system_library_symbolst::is_symbol_internal_symbol( + const symbolt &symbol, + std::set &out_system_headers) const +{ + const std::string &name_str=id2string(symbol.name); + + if(has_prefix(name_str, CPROVER_PREFIX) || + name_str=="__func__" || + name_str=="__FUNCTION__" || + name_str=="__PRETTY_FUNCTION__" || + name_str=="argc'" || + name_str=="argv'" || + name_str=="envp'" || + name_str=="envp_size'") + return true; + + // exclude nondet instructions + if(has_prefix(name_str, "nondet_")) + return true; + + if(has_prefix(name_str, "__VERIFIER")) + return true; + + if(has_suffix(name_str, "$object")) + return true; + + const std::string &file_str=id2string(symbol.location.get_file()); + + // don't dump internal GCC builtins + if(has_prefix(file_str, "gcc_builtin_headers_") && + has_prefix(name_str, "__builtin_")) + return true; + + if(name_str=="__builtin_va_start" || + name_str=="__builtin_va_end" || + symbol.name==ID_gcc_builtin_va_arg) + { + out_system_headers.insert("stdarg.h"); + return true; + } + + // don't dump asserts + else if(name_str=="__assert_fail" || + name_str=="_assert" || + name_str=="__assert_c99" || + name_str=="_wassert") + return true; + + const auto &it=system_library_map.find(symbol.name); + + if(it!=system_library_map.end()) + { + out_system_headers.insert(id2string(it->second)); + return true; + } + + if(use_all_headers && + has_prefix(file_str, "/usr/include/")) + { + if(file_str.find("/bits/")==std::string::npos) + { + // Do not include transitive includes of system headers! + std::string::size_type prefix_len=std::string("/usr/include/").size(); + out_system_headers.insert(file_str.substr(prefix_len)); + } + + return true; + } + + return false; +} diff --git a/src/goto-programs/system_library_symbols.h b/src/goto-programs/system_library_symbols.h new file mode 100644 index 00000000000..9438e052a76 --- /dev/null +++ b/src/goto-programs/system_library_symbols.h @@ -0,0 +1,38 @@ +/*******************************************************************\ + +Module: Goto Programs + +Author: Thomas Kiley + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H +#define CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H + +#include +#include +#include +#include + +class symbolt; + +class system_library_symbolst +{ +public: + system_library_symbolst(); + + bool is_symbol_internal_symbol( + const symbolt &symbol, + std::set &out_system_headers) const; + +private: + void init_system_library_map(); + + void add_to_system_library( + irep_idt header_file, + std::list symbols); + + std::map system_library_map; +}; + +#endif // CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index b0b296c9cfd..6da2bad7129 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1070,6 +1070,25 @@ codet java_bytecode_convert_methodt::convert_instructions( get_message_handler()); } } + // replace calls to CProver.assume + else if(statement=="invokestatic" && + id2string(arg0.get(ID_identifier))== + "java::org.cprover.CProver.assume:(Z)V") + { + const code_typet &code_type=to_code_type(arg0.type()); + // sanity check: function has the right number of args + assert(code_type.parameters().size()==1); + + exprt operand = pop(1)[0]; + // we may need to adjust the type of the argument + if(operand.type()!=bool_typet()) + operand.make_typecast(bool_typet()); + + c=code_assumet(operand); + source_locationt loc=i_it->source_location; + loc.set_function(method_id); + c.add_source_location()=loc; + } else if(statement=="invokeinterface" || statement=="invokespecial" || statement=="invokevirtual" || diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java new file mode 100644 index 00000000000..72c3eeb1d70 --- /dev/null +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -0,0 +1,11 @@ +package org.cprover; + +public final class CProver +{ + public static boolean enableAssume=true; + public static void assume(boolean condition) + { + if(enableAssume) + throw new RuntimeException("Cannot execute program with CProver.assume()"); + } +} diff --git a/src/util/Makefile b/src/util/Makefile index d5030ef2a48..cff6340e044 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -17,6 +17,7 @@ SRC = arith_tools.cpp \ find_symbols.cpp \ fixedbv.cpp \ format_constant.cpp \ + format_number_range.cpp \ fresh_symbol.cpp \ get_base_name.cpp \ get_module.cpp \ diff --git a/src/util/format_number_range.cpp b/src/util/format_number_range.cpp new file mode 100644 index 00000000000..cca3bbf154c --- /dev/null +++ b/src/util/format_number_range.cpp @@ -0,0 +1,122 @@ +/*******************************************************************\ + +Module: Format vector of numbers into a compressed range + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include +#include +#include + +#include "format_number_range.h" + +/*******************************************************************\ + +Function: format_number_range::operator() + + Inputs: vector of numbers + + Outputs: string of compressed number range representation + + Purpose: create shorter representation for output + +\*******************************************************************/ + +std::string format_number_ranget::operator()(std::vector &numbers) +{ + std::string number_range; + std::sort(numbers.begin(), numbers.end()); + unsigned end_number=numbers.back(); + if(numbers.front()==end_number) + number_range=std::to_string(end_number); // only single number + else + { + bool next=true; + bool first=true; + bool range=false; + unsigned start_number=numbers.front(); + unsigned last_number=start_number; + + for(const auto &number : numbers) + { + if(next) + { + next=false; + start_number=number; + last_number=number; + } + // advance one forward + else + { + if(number==last_number+1 && !(number==end_number)) + { + last_number++; + if(last_number>start_number+1) + range=true; + } + // end this block range + else + { + if(first) + first=false; + else + number_range+=","; + if(last_number>start_number) + { + if(range) + { + if(number==end_number && number==last_number+1) + number_range+= + std::to_string(start_number)+"-"+std::to_string(end_number); + else if(number==end_number) + number_range+= + std::to_string(start_number)+"-"+std::to_string(last_number)+ + ","+std::to_string(end_number); + else + number_range+= + std::to_string(start_number)+"-"+std::to_string(last_number); + } + else + { + if(number!=end_number) + number_range+= + std::to_string(start_number)+","+std::to_string(last_number); + else + { + if(start_number+1==last_number && last_number+1==number) + number_range+= + std::to_string(start_number)+"-"+std::to_string(end_number); + else + number_range+= + std::to_string(start_number)+ + ","+std::to_string(last_number)+ + ","+std::to_string(end_number); + } + } + start_number=number; + last_number=number; + range=false; + continue; + } + else + { + if(number!=end_number) + number_range+=std::to_string(start_number); + else + number_range+=std::to_string(start_number)+","+ + std::to_string(end_number); + start_number=number; + last_number=number; + range=false; + continue; // already set next start number + } + next=true; + } + } + } + } + assert(!number_range.empty()); + return number_range; +} diff --git a/src/util/format_number_range.h b/src/util/format_number_range.h new file mode 100644 index 00000000000..7ff016e9c4d --- /dev/null +++ b/src/util/format_number_range.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: Format vector of numbers into a compressed range + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_FORMAT_NUMBER_RANGE_H +#define CPROVER_UTIL_FORMAT_NUMBER_RANGE_H + +#include +#include + +class format_number_ranget +{ +public: + std::string operator()(std::vector &); +}; + +#endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e31eceb1e98..77568e3d5d6 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -810,6 +810,7 @@ IREP_ID_ONE(cprover_string_to_upper_case_func) IREP_ID_ONE(cprover_string_trim_func) IREP_ID_ONE(cprover_string_value_of_func) IREP_ID_ONE(array_replace) +IREP_ID_ONE(basic_block_covered_lines) #undef IREP_ID_ONE #undef IREP_ID_TWO diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index 980284ffcd8..e79d58f63e9 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -18,6 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "mp_arith.h" #include "arith_tools.h" +typedef BigInt::ullong_t ullong_t; // NOLINT(readability/identifiers) +typedef BigInt::llong_t llong_t; // NOLINT(readability/identifiers) + mp_integer operator>>(const mp_integer &a, const mp_integer &b) { mp_integer power=::power(2, b); @@ -207,3 +210,277 @@ unsigned integer2unsigned(const mp_integer &n) assert(ull <= std::numeric_limits::max()); return (unsigned)ull; } + +/*******************************************************************\ + +Function: bitwise_or + + Inputs: + + Outputs: + + Purpose: bitwise or + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_or(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()|b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_and + + Inputs: + + Outputs: + + Purpose: bitwise and + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_and(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()&b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_xor + + Inputs: + + Outputs: + + Purpose: bitwise xor + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()^b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_neg + + Inputs: + + Outputs: + + Purpose: bitwise negation + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_neg(const mp_integer &a) +{ + ullong_t result=~a.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: arith_left_shift + + Inputs: + + Outputs: + + Purpose: arithmetic left shift + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer arith_left_shift( + const mp_integer &a, + const mp_integer &b, + std::size_t true_size) +{ + ullong_t shift=b.to_ulong(); + if(shift>true_size && a!=mp_integer(0)) + throw "shift value out of range"; + + llong_t result=a.to_long()<true_size) + throw "shift value out of range"; + + llong_t sign=(1<<(true_size-1))&number; + llong_t pad=(sign==0) ? 0 : ~((1<<(true_size-shift))-1); + llong_t result=(number >> shift)|pad; + return result; +} + +/*******************************************************************\ + +Function: logic_left_shift + + Inputs: + + Outputs: + + Purpose: logic left shift + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer logic_left_shift( + const mp_integer &a, + const mp_integer &b, + std::size_t true_size) +{ + ullong_t shift=b.to_ulong(); + if(shift>true_size && a!=mp_integer(0)) + throw "shift value out of range"; + llong_t result=a.to_long()<true_size) + throw "shift value out of range"; + + ullong_t result=((ullong_t)a.to_long()) >> shift; + return result; +} + +/*******************************************************************\ + +Function: rotate_right + + Inputs: + + Outputs: + + Purpose: rotates right (MSB=LSB) + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer rotate_right( + const mp_integer &a, + const mp_integer &b, + std::size_t true_size) +{ + ullong_t number=a.to_ulong(); + ullong_t shift=b.to_ulong(); + if(shift>true_size) + throw "shift value out of range"; + + ullong_t revShift=true_size-shift; + ullong_t filter=1<<(true_size-1); + ullong_t result=(number >> shift)|((number<true_size) + throw "shift value out of range"; + + ullong_t revShift=true_size-shift; + ullong_t filter=1<<(true_size-1); + ullong_t result=((number<> revShift); + return result; +} diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index eede5855b75..7cc4dd7dfad 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -21,6 +21,28 @@ typedef BigInt mp_integer; std::ostream &operator<<(std::ostream &, const mp_integer &); mp_integer operator>>(const mp_integer &, const mp_integer &); mp_integer operator<<(const mp_integer &, const mp_integer &); +mp_integer bitwise_or(const mp_integer &, const mp_integer &); +mp_integer bitwise_and(const mp_integer &, const mp_integer &); +mp_integer bitwise_xor(const mp_integer &, const mp_integer &); +mp_integer bitwise_neg(const mp_integer &); + +mp_integer arith_left_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer arith_right_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer logic_left_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer logic_right_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer rotate_right( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer rotate_left( + const mp_integer &, const mp_integer &, std::size_t true_size); const std::string integer2string(const mp_integer &, unsigned base=10); const mp_integer string2integer(const std::string &, unsigned base=10); @@ -29,5 +51,6 @@ const mp_integer binary2integer(const std::string &, bool is_signed); mp_integer::ullong_t integer2ulong(const mp_integer &); std::size_t integer2size_t(const mp_integer &); unsigned integer2unsigned(const mp_integer &); +const mp_integer mp_zero=string2integer("0"); #endif // CPROVER_UTIL_MP_ARITH_H diff --git a/src/util/source_location.h b/src/util/source_location.h index 4186f3e35e2..95bef820ae9 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -75,6 +75,11 @@ class source_locationt:public irept return get(ID_java_bytecode_index); } + const irep_idt &get_basic_block_covered_lines() const + { + return get(ID_basic_block_covered_lines); + } + void set_file(const irep_idt &file) { set(ID_file, file); @@ -130,6 +135,11 @@ class source_locationt:public irept set(ID_java_bytecode_index, index); } + void set_basic_block_covered_lines(const irep_idt &covered_lines) + { + return set(ID_basic_block_covered_lines, covered_lines); + } + void set_hide() { set(ID_hide, true); diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index feb37fe84ca..77f2c43bbb5 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -67,6 +67,19 @@ static void build_ssa_identifier_rec( assert(false); } +/// Used to determine whether or not an identifier can be built +/// before trying and getting an exception +bool ssa_exprt::can_build_identifier(const exprt &expr) +{ + if(expr.id()==ID_symbol) + return true; + else if(expr.id()==ID_member || + expr.id()==ID_index) + return can_build_identifier(expr.op0()); + else + return false; +} + std::pair ssa_exprt::build_identifier( const exprt &expr, const irep_idt &l0, diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 61cbc566ef1..63e6dfaf7d7 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -65,7 +65,7 @@ class ssa_exprt:public symbol_exprt const irep_idt get_l1_object_identifier() const { - #if 0 + #if 1 return get_l1_object().get_identifier(); #else // the above is the clean version, this is the fast one, using @@ -135,6 +135,10 @@ class ssa_exprt:public symbol_exprt const irep_idt &l0, const irep_idt &l1, const irep_idt &l2); + + /* Used to determine whether or not an identifier can be built + * before trying and getting an exception */ + static bool can_build_identifier(const exprt &src); }; /*! \brief Cast a generic exprt to an \ref ssa_exprt diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e2ed2ad433d..c8a92a89b1f 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3287,6 +3287,17 @@ class member_exprt:public exprt { return op0(); } + + // Retrieves the object(symbol) this member corresponds to + inline const symbol_exprt &symbol() const + { + const exprt &op=op0(); + if(op.id()==ID_member) + { + return static_cast(op).symbol(); + } + return to_symbol_expr(op); + } }; /*! \brief Cast a generic exprt to a \ref member_exprt