From a7c0673d65ed362ec297a7cb429b1fbf5d62e511 Mon Sep 17 00:00:00 2001 From: johnfxgalea Date: Fri, 18 Nov 2016 18:07:52 +0000 Subject: [PATCH] Support for va_args Update main.c Fixed Indentation in tests Fixed some indentation and va_arg search Arranged test desc for test "va_args_7" Further code arrangements Removed spaces Removed more spaces Included further code arrangements and refactoring. Update path_symex.cpp Added comment regarding va_arg identifier construction. --- regression/symex/va_args_1/main.c | 37 +++++++ regression/symex/va_args_1/test.desc | 8 ++ regression/symex/va_args_10/main.c | 41 ++++++++ regression/symex/va_args_10/test.desc | 8 ++ regression/symex/va_args_2/main.c | 35 +++++++ regression/symex/va_args_2/test.desc | 8 ++ regression/symex/va_args_3/main.c | 34 ++++++ regression/symex/va_args_3/test.desc | 8 ++ regression/symex/va_args_4/main.c | 38 +++++++ regression/symex/va_args_4/test.desc | 8 ++ regression/symex/va_args_5/main.c | 35 +++++++ regression/symex/va_args_5/test.desc | 6 ++ regression/symex/va_args_6/main.c | 34 ++++++ regression/symex/va_args_6/test.desc | 6 ++ regression/symex/va_args_7/main.c | 23 ++++ regression/symex/va_args_7/test.desc | 6 ++ regression/symex/va_args_8/main.c | 37 +++++++ regression/symex/va_args_8/test.desc | 8 ++ regression/symex/va_args_9/main.c | 41 ++++++++ regression/symex/va_args_9/test.desc | 8 ++ src/path-symex/path_symex.cpp | 145 +++++++++++++++++++++++++- src/path-symex/path_symex_class.h | 5 + src/path-symex/var_map.cpp | 25 +++-- 23 files changed, 591 insertions(+), 13 deletions(-) create mode 100644 regression/symex/va_args_1/main.c create mode 100644 regression/symex/va_args_1/test.desc create mode 100644 regression/symex/va_args_10/main.c create mode 100644 regression/symex/va_args_10/test.desc create mode 100644 regression/symex/va_args_2/main.c create mode 100644 regression/symex/va_args_2/test.desc create mode 100644 regression/symex/va_args_3/main.c create mode 100644 regression/symex/va_args_3/test.desc create mode 100644 regression/symex/va_args_4/main.c create mode 100644 regression/symex/va_args_4/test.desc create mode 100644 regression/symex/va_args_5/main.c create mode 100644 regression/symex/va_args_5/test.desc create mode 100644 regression/symex/va_args_6/main.c create mode 100644 regression/symex/va_args_6/test.desc create mode 100644 regression/symex/va_args_7/main.c create mode 100644 regression/symex/va_args_7/test.desc create mode 100644 regression/symex/va_args_8/main.c create mode 100644 regression/symex/va_args_8/test.desc create mode 100644 regression/symex/va_args_9/main.c create mode 100644 regression/symex/va_args_9/test.desc diff --git a/regression/symex/va_args_1/main.c b/regression/symex/va_args_1/main.c new file mode 100644 index 00000000000..d8778034354 --- /dev/null +++ b/regression/symex/va_args_1/main.c @@ -0,0 +1,37 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + + int y = 7; + int u = 2; + m = max(3, y, u, 9); + + assert(m == 9); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_1/test.desc b/regression/symex/va_args_1/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/symex/va_args_1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex/va_args_10/main.c b/regression/symex/va_args_10/main.c new file mode 100644 index 00000000000..554187f64d6 --- /dev/null +++ b/regression/symex/va_args_10/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + int m2; + int m3; + + m = max(3, 2, 6, 9); + + m2 = max(3, 4, 11, 1); + + m3 = max(2, m, m2); + + assert(m3 == 6); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_10/test.desc b/regression/symex/va_args_10/test.desc new file mode 100644 index 00000000000..6de79559914 --- /dev/null +++ b/regression/symex/va_args_10/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex/va_args_2/main.c b/regression/symex/va_args_2/main.c new file mode 100644 index 00000000000..2a35ca4bb43 --- /dev/null +++ b/regression/symex/va_args_2/main.c @@ -0,0 +1,35 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + int y; + m = max(2, y, 8); + + assert(m == 8); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_2/test.desc b/regression/symex/va_args_2/test.desc new file mode 100644 index 00000000000..6de79559914 --- /dev/null +++ b/regression/symex/va_args_2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex/va_args_3/main.c b/regression/symex/va_args_3/main.c new file mode 100644 index 00000000000..148d70521db --- /dev/null +++ b/regression/symex/va_args_3/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + m = max(2, 1, 8); + + assert(m == 1); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_3/test.desc b/regression/symex/va_args_3/test.desc new file mode 100644 index 00000000000..6de79559914 --- /dev/null +++ b/regression/symex/va_args_3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex/va_args_4/main.c b/regression/symex/va_args_4/main.c new file mode 100644 index 00000000000..4a19acfe54a --- /dev/null +++ b/regression/symex/va_args_4/main.c @@ -0,0 +1,38 @@ +#include +#include +#include + +int max(int n, ...); + +int main() +{ + int m; + m = max(2, 2, 8, 10); + + assert(m == 10); + + return 0; +} + +int max(int repeat,int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + for (i = 0; i < repeat; i++){ + printf("%d. Result is: %d", i, largest); + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_4/test.desc b/regression/symex/va_args_4/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/symex/va_args_4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex/va_args_5/main.c b/regression/symex/va_args_5/main.c new file mode 100644 index 00000000000..a1e4d6a9d70 --- /dev/null +++ b/regression/symex/va_args_5/main.c @@ -0,0 +1,35 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int n; + int m; + m = max(7, 7, 8); + + assert(m == 8); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_5/test.desc b/regression/symex/va_args_5/test.desc new file mode 100644 index 00000000000..b69d21c78ba --- /dev/null +++ b/regression/symex/va_args_5/test.desc @@ -0,0 +1,6 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/symex/va_args_6/main.c b/regression/symex/va_args_6/main.c new file mode 100644 index 00000000000..191435ff3e0 --- /dev/null +++ b/regression/symex/va_args_6/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + m = max(8, 2, 7, 8); + + assert(m == 2); + + return 0; +} + +int max (int j, int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_6/test.desc b/regression/symex/va_args_6/test.desc new file mode 100644 index 00000000000..9431f04e854 --- /dev/null +++ b/regression/symex/va_args_6/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--unwind 8 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/symex/va_args_7/main.c b/regression/symex/va_args_7/main.c new file mode 100644 index 00000000000..cecc1bf0050 --- /dev/null +++ b/regression/symex/va_args_7/main.c @@ -0,0 +1,23 @@ +#include +#include +#include + +int main () +{ + + int eva_arguments; + int n; + + int init_eva = eva_arguments; + + for (unsigned int i = 0; i < n; i++){ + + eva_arguments++; + } + + if (init_eva == 0){ + assert(eva_arguments == n); + } + + return 0; +} diff --git a/regression/symex/va_args_7/test.desc b/regression/symex/va_args_7/test.desc new file mode 100644 index 00000000000..832e94ec88a --- /dev/null +++ b/regression/symex/va_args_7/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--unwind 8 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/symex/va_args_8/main.c b/regression/symex/va_args_8/main.c new file mode 100644 index 00000000000..90e203170f6 --- /dev/null +++ b/regression/symex/va_args_8/main.c @@ -0,0 +1,37 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + + int y = 7; + int u = 2; + m = max(3, y, u, 9); + + assert(m == 10); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int) + 1; + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex/va_args_8/test.desc b/regression/symex/va_args_8/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/symex/va_args_8/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex/va_args_9/main.c b/regression/symex/va_args_9/main.c new file mode 100644 index 00000000000..4c9d52bb394 --- /dev/null +++ b/regression/symex/va_args_9/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + int m2; + int m3; + + m = max(3, 2, 6, 9); + m2 = max(3, 4, 11, 1); + + m3 = max(2, m, m2); + + assert(m3 == 11); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + + return largest; +} diff --git a/regression/symex/va_args_9/test.desc b/regression/symex/va_args_9/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/symex/va_args_9/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index 45fb7bb9e5a..5e1ad444ebf 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -10,10 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include - +#include #include #include @@ -123,6 +124,11 @@ void path_symext::assign( { // done in statet:instantiate_rec } + else if(statement==ID_gcc_builtin_va_arg_next) + { + symex_va_arg_next(state, lhs, side_effect_expr); + return; + } else throw "unexpected side-effect on rhs: "+id2string(statement); } @@ -290,6 +296,103 @@ void path_symext::symex_malloc( assign(state, lhs, rhs); } + +/*******************************************************************\ + +Function: get_old_va_symb + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static irep_idt get_old_va_symbol( + const path_symex_statet &state, + const exprt &src) +{ + if(src.id()==ID_typecast) + return get_old_va_symbol(state, to_typecast_expr(src).op()); + else if(src.id()==ID_address_of) + { + const exprt &op=to_address_of_expr(src).object(); + + if(op.id()==ID_symbol) + return to_symbol_expr(op).get_identifier(); + } + + return irep_idt(); +} + +/*******************************************************************\ + +Function: path_symext::symex_va_arg_next + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void path_symext::symex_va_arg_next( + path_symex_statet &state, + const exprt &lhs, + const side_effect_exprt &code) +{ + if(code.operands().size()!=1) + throw "va_arg_next expected to have one operand"; + + if(lhs.is_nil()) + return;// ignore + + exprt tmp=state.read(code.op0()); // constant prop on va_arg parameter + + // Get old symbol of va_arg and modify it to generate a new one. + irep_idt id=get_old_va_symbol(state, tmp); + exprt rhs=gen_zero(lhs.type()); + + if(!id.empty()) + { + // strip last name off id to get function name + std::size_t pos=id2string(id).rfind("::"); + if(pos!=std::string::npos) + { + irep_idt function_identifier=std::string(id2string(id), 0, pos); + std::string base=id2string(function_identifier)+"::va_arg"; + + /* + * Construct the identifier of the va_arg argument such that it + * corresponds to the respective one set upon function call + */ + if(has_prefix(id2string(id), base)) + id=base + +i2string( + safe_string2unsigned( + std::string(id2string(id), base.size(), std::string::npos)) + +1); + else + id=base+"0"; + + const var_mapt::var_infot &var_info=state.var_map[id]; + + if(var_info.full_identifier==id) + { + const path_symex_statet::var_statet &var_state + =state.get_var_state(var_info); + const exprt symbol_expr=symbol_exprt(id, var_state.ssa_symbol.type()); + rhs=address_of_exprt(symbol_expr); + rhs.make_typecast(lhs.type()); + } + } + } + + assign(state, lhs, rhs); +} + /*******************************************************************\ Function: path_symext::assign_rec @@ -644,6 +747,9 @@ void path_symext::function_call_rec( const code_typet::parameterst &function_parameters=code_type.parameters(); const exprt::operandst &call_arguments=call.arguments(); + + // keep track when va arguments begin. + unsigned va_args_start_index=0; // now assign the argument values to parameters for(unsigned i=0; iis_static_lifetime) { - if(symbol.is_thread_local) + if(symbol->is_thread_local) var_info.kind=var_infot::THREAD_LOCAL; else var_info.kind=var_infot::SHARED; @@ -126,13 +136,6 @@ void var_mapt::init(var_infot &var_info) else var_info.kind=var_infot::PROCEDURE_LOCAL; } - - catch(std::string s) - { - throw "var_mapt::init identifier \"" + - id2string(var_info.full_identifier)+ - "\" lookup in ns failed"; - } } if(var_info.is_shared())