void goto_convertt::convert_CPROVER_try_catch(
  const codet &code,
  goto_programt &dest)
{
  if(code.operands().size()!=2)
  {
    err_location(code);
    throw "CPROVER_try_catch expects two arguments";
  }

  // this is where we go after 'throw'
  goto_programt tmp;
  tmp.add_instruction(SKIP)->source_location=code.source_location();

  // set 'throw' target
  throw_targett throw_target(targets);
  targets.set_throw(tmp.instructions.begin());
  
  // now put 'catch' code onto destructor stack
  code_ifthenelset catch_code;
  catch_code.cond()=exception_flag();
  catch_code.add_source_location()=code.source_location();
  catch_code.then_case()=to_code(code.op1());

  targets.destructor_stack.push_back(catch_code);

  // now convert 'try' code
  convert(to_code(code.op0()), dest);

  // pop 'catch' code off stack
  targets.destructor_stack.pop_back();
  
  // add 'throw' target
  dest.destructive_append(tmp);
}

void goto_convertt::convert_msc_leave(
  const codet &code,
  goto_programt &dest)
{
  if(!targets.leave_set)
  {
    error().source_location=code.find_source_location();
    error() << "leave without target" << eom;
    throw 0;
  }
  
  // need to process destructor stack
  for(unsigned d=targets.destructor_stack.size();
      d!=targets.leave_stack_size;
      d--)
  {
    codet d_code=targets.destructor_stack[d-1];
    d_code.add_source_location()=code.source_location();
    convert(d_code, dest);
  }

  goto_programt::targett t=dest.add_instruction();
  t->make_goto(targets.leave_target);
  t->source_location=code.source_location();
}

void goto_convertt::convert_CPROVER_throw(
  const codet &code,
  goto_programt &dest)
{
  // set the 'exception' flag
  {
    goto_programt::targett t_set_exception=
      dest.add_instruction(ASSIGN);

    t_set_exception->source_location=code.source_location();
    t_set_exception->code=code_assignt(exception_flag(), true_exprt());
  }

  // do we catch locally?
  if(targets.throw_set)
  {
    // need to process destructor stack
    unwind_destructor_stack(code.source_location(), targets.throw_stack_size, dest);

    // add goto
    goto_programt::targett t=dest.add_instruction();
    t->make_goto(targets.throw_target);
    t->source_location=code.source_location();
  }
  else // otherwise, we do a return
  {
    // need to process destructor stack
    unwind_destructor_stack(code.source_location(), 0, dest);

    // add goto
    goto_programt::targett t=dest.add_instruction();
    t->make_goto(targets.return_target);
    t->source_location=code.source_location();
  }
}

void java_bytecode_typecheckt::typecheck_code(codet &code)
{
  const irep_idt &statement=code.get_statement();

  if(statement==ID_assign)
  {
    code_assignt &code_assign=to_code_assign(code);
    typecheck_expr(code_assign.lhs());
    typecheck_expr(code_assign.rhs());

    if(code_assign.lhs().type()!=code_assign.rhs().type())
      code_assign.rhs().make_typecast(code_assign.lhs().type());
  }
  else if(statement==ID_block)
  {
    Forall_operands(it, code)
      typecheck_code(to_code(*it));
  }
  else if(statement==ID_label)
  {
    code_labelt &code_label=to_code_label(code);
    typecheck_code(code_label.code());
  }
  else if(statement==ID_goto)
  {
  }
  else if(statement==ID_ifthenelse)
  {
    code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
    typecheck_expr(code_ifthenelse.cond());
    typecheck_code(code_ifthenelse.then_case());
    if(code_ifthenelse.else_case().is_not_nil())
      typecheck_code(code_ifthenelse.else_case());
  }
  else if(statement==ID_switch)
  {
    code_switcht &code_switch = to_code_switch(code);
    typecheck_expr(code_switch.value());
  }
  else if(statement==ID_return)
  {
    if(code.operands().size()==1)
      typecheck_expr(code.op0());
  }
  else if(statement==ID_function_call)
  {
    code_function_callt &code_function_call=to_code_function_call(code);
    typecheck_expr(code_function_call.lhs());
    typecheck_expr(code_function_call.function());

    for(code_function_callt::argumentst::iterator
        a_it=code_function_call.arguments().begin();
        a_it!=code_function_call.arguments().end();
        a_it++)
      typecheck_expr(*a_it);
  }
}

void rw_sett::compute(const codet &code)
{
  const irep_idt &statement=code.get_statement();
  
  if(statement==ID_assign)
  {
    assert(code.operands().size()==2);
    assign(code.op0(), code.op1());
  }
}

void c_typecheck_baset::typecheck_start_thread(codet &code)
{
  if(code.operands().size()!=1)
  {
    err_location(code);
    error() << "start_thread expected to have one operand" << eom;
    throw 0;
  }

  typecheck_code(to_code(code.op0()));
}

void goto_convertt::convert_try_catch(
  const codet &code,
  goto_programt &dest)
{
  assert(code.operands().size()>=2);
  
  // add the CATCH-push instruction to 'dest'
  goto_programt::targett catch_push_instruction=dest.add_instruction();
  catch_push_instruction->make_catch();
  catch_push_instruction->code.set_statement(ID_catch);
  catch_push_instruction->source_location=code.source_location();
  
  // the CATCH-push instruction is annotated with a list of IDs,
  // one per target
  irept::subt &exception_list=
    catch_push_instruction->code.add(ID_exception_list).get_sub();

  // add a SKIP target for the end of everything
  goto_programt end;
  goto_programt::targett end_target=end.add_instruction();
  end_target->make_skip();
  
  // the first operand is the 'try' block
  convert(to_code(code.op0()), dest);
  
  // add the CATCH-pop to the end of the 'try' block
  goto_programt::targett catch_pop_instruction=dest.add_instruction();
  catch_pop_instruction->make_catch();
  catch_pop_instruction->code.set_statement(ID_catch);
  
  // add a goto to the end of the 'try' block
  dest.add_instruction()->make_goto(end_target);

  for(unsigned i=1; i<code.operands().size(); i++)
  {
    const codet &block=to_code(code.operands()[i]);
  
    // grab the ID and add to CATCH instruction
    exception_list.push_back(irept(block.get(ID_exception_id)));
    
    goto_programt tmp;
    convert(block, tmp);
    catch_push_instruction->targets.push_back(tmp.instructions.begin());
    dest.destructive_append(tmp);

    // add a goto to the end of the 'catch' block
    dest.add_instruction()->make_goto(end_target);
  }

  // add the end-target  
  dest.destructive_append(end);
}

void c_typecheck_baset::typecheck_spec_expr(
  codet &code,
  const irep_idt &spec)
{
  if(code.find(spec).is_not_nil())
  {
    exprt &constraint=
      static_cast<exprt&>(code.add(spec));

    typecheck_expr(constraint);
    implicit_typecast_bool(constraint);
  }
}

void c_typecheck_baset::typecheck_expression(codet &code)
{
  if(code.operands().size()!=1)
  {
    err_location(code);
    error() << "expression statement expected to have one operand"
            << eom;
    throw 0;
  }

  exprt &op=code.op0();
  typecheck_expr(op);
}

void goto_convertt::convert_msc_try_except(
  const codet &code,
  goto_programt &dest)
{
  if(code.operands().size()!=3)
  {
    err_location(code);
    throw "msc_try_except expects three arguments";
  }

  convert(to_code(code.op0()), dest);
  
  // todo: generate exception tracking
}

void goto_convertt::convert_java_try_catch(
  const codet &code,
  goto_programt &dest)
{
  assert(!code.operands().empty());

  // add the CATCH instruction to 'dest'
  goto_programt::targett catch_instruction=dest.add_instruction();
  catch_instruction->make_catch();
  catch_instruction->code.set_statement(ID_catch);
  catch_instruction->source_location=code.source_location();
  catch_instruction->function=code.source_location().get_function();

  // the CATCH instruction is annotated with a list of exception IDs
  const irept exceptions=code.op0().find(ID_exception_list);
  if(exceptions.is_not_nil())
  {
    irept::subt exceptions_sub=exceptions.get_sub();
    irept::subt &exception_list=
      catch_instruction->code.add(ID_exception_list).get_sub();
    exception_list.resize(exceptions_sub.size());
    for(size_t i=0; i<exceptions_sub.size(); ++i)
      exception_list[i].id(exceptions_sub[i].id());
  }

  // the CATCH instruction is also annotated with a list of handle labels
  const irept handlers=code.op0().find(ID_label);
  if(handlers.is_not_nil())
  {
    irept::subt handlers_sub=handlers.get_sub();
    irept::subt &handlers_list=
      catch_instruction->code.add(ID_label).get_sub();
    handlers_list.resize(handlers_sub.size());
    for(size_t i=0; i<handlers_sub.size(); ++i)
      handlers_list[i].id(handlers_sub[i].id());
  }

  // the CATCH instruction may also signal a handler
  if(code.op0().has_operands())
  {
    catch_instruction->code.get_sub().resize(1);
    catch_instruction->code.get_sub()[0]=code.op0().op0();
  }

  // add a SKIP target for the end of everything
  goto_programt end;
  goto_programt::targett end_target=end.add_instruction();
  end_target->make_skip();
  end_target->source_location=code.source_location();
  end_target->function=code.source_location().get_function();

  // add the end-target
  dest.destructive_append(end);
}

void c_typecheck_baset::typecheck_assign(codet &code)
{
  if(code.operands().size()!=2)
  {
    err_location(code);
    error() << "assignment statement expected to have two operands"
            << eom;
    throw 0;
  }

  typecheck_expr(code.op0());
  typecheck_expr(code.op1());

  implicit_typecast(code.op1(), code.op0().type());
}

void goto_convertt::convert_msc_try_except(
  const codet &code,
  goto_programt &dest)
{
  if(code.operands().size()!=3)
  {
    error().source_location=code.find_source_location();
    error() << "msc_try_except expects three arguments" << eom;
    throw 0;
  }

  convert(to_code(code.op0()), dest);
  
  // todo: generate exception tracking
}

void static_lifetime_init(
  const contextt &context,
  codet &dest)
{
  dest=code_blockt();

  // Do assignments based on "value".
  context.foreach_operand_in_order(
    [&dest] (const symbolt& s)
    {
      if(s.static_lifetime)
        init_variable(dest, s);
    }
  );

  // call designated "initialization" functions
  context.foreach_operand_in_order(
    [&dest] (const symbolt& s)
    {
      if(s.type.initialization() && s.type.is_code())
      {
        code_function_callt function_call;
        function_call.function() = symbol_expr(s);
        dest.move_to_operands(function_call);
      }
    }
  );
}

void jsil_typecheckt::typecheck_code(codet &code)
{
  const irep_idt &statement=code.get_statement();

  if(statement==ID_function_call)
    typecheck_function_call(to_code_function_call(code));
  else if(statement==ID_return)
    typecheck_return(to_code_return(code));
  else if(statement==ID_expression)
  {
    if(code.operands().size()!=1)
      throw "expression statement expected to have one operand";

    typecheck_expr(code.op0());
  }
  else if(statement==ID_label)
  {
    typecheck_code(to_code_label(code).code());
    // TODO: produce defined label set
  }
  else if(statement==ID_block)
    typecheck_block(code);
  else if(statement==ID_ifthenelse)
    typecheck_ifthenelse(to_code_ifthenelse(code));
  else if(statement==ID_goto)
  {
    // TODO: produce used label set
  }
  else if(statement==ID_assign)
    typecheck_assign(to_code_assign(code));
  else if(statement==ID_try_catch)
    typecheck_try_catch(to_code_try_catch(code));
  else if(statement==ID_skip)
  {
  }
  else
  {
    err_location(code);
    error() << "unexpected statement: " << statement << eom;
    throw 0;
  }
}

void c_typecheck_baset::typecheck_return(codet &code)
{
  if(code.operands().empty())
  {
    if(follow(return_type).id()!=ID_empty)
    {
      // gcc doesn't actually complain, it just warns!
      // We'll put a zero here, which is dubious.
      exprt zero=zero_initializer(return_type, code.source_location(), *this, get_message_handler());
      code.copy_to_operands(zero);
    }
  }
  else if(code.operands().size()==1)
  {
    typecheck_expr(code.op0());

    if(follow(return_type).id()==ID_empty)
    {
      // gcc doesn't actually complain, it just warns!
      if(follow(code.op0().type()).id()!=ID_empty)
      {
        warning().source_location=code.source_location();

        warning() << "function has return void ";
        warning() << "but a return statement returning ";
        warning() << to_string(follow(code.op0().type()));
        warning() << eom;

        code.op0().make_typecast(return_type);
      }
    }
    else
      implicit_typecast(code.op0(), return_type);
  }
  else
  {
    err_location(code);
    error() << "return expected to have 0 or 1 operands" << eom;
    throw 0;
  }
}

std::string expr2javat::convert_code(
  const codet &src,
  unsigned indent)
{
  const irep_idt &statement=src.get(ID_statement);

  if(statement==ID_java_new ||
     statement==ID_java_new_array)
    return convert_java_new(src,indent);

  return expr2ct::convert_code(src, indent);
}

void c_typecheck_baset::typecheck_asm(codet &code)
{
  const irep_idt flavor=to_code_asm(code).get_flavor();

  if(flavor==ID_gcc)
  {
    // These have 5 operands.
    // The first parameter is a string.
    // Parameters 1, 2, 3, 4 are lists of expressions.

    // Parameter 1: OutputOperands
    // Parameter 2: InputOperands
    // Parameter 3: Clobbers
    // Parameter 4: GotoLabels

    assert(code.operands().size()==5);

    typecheck_expr(code.op0());

    for(unsigned i=1; i<code.operands().size(); i++)
    {
      exprt &list=code.operands()[i];
      Forall_operands(it, list)
        typecheck_expr(*it);
    }
  }
  else if(flavor==ID_msc)
  {
    assert(code.operands().size()==1);
    typecheck_expr(code.op0());
  }
}

void goto_convertt::convert_CPROVER_try_finally(
  const codet &code,
  goto_programt &dest)
{
  if(code.operands().size()!=2)
  {
    err_location(code);
    throw "CPROVER_try_finally expects two arguments";
  }
  
  // first put 'finally' code onto destructor stack
  targets.destructor_stack.push_back(to_code(code.op1()));
  
  // do 'try' code
  convert(to_code(code.op0()), dest);

  // pop 'finally' from destructor stack
  targets.destructor_stack.pop_back();

  // now add 'finally' code
  convert(to_code(code.op1()), dest);
}

void c_typecheck_baset::typecheck_block(codet &code)
{
  Forall_operands(it, code)
    typecheck_code(to_code(*it));

  // do decl-blocks

  exprt new_ops;
  new_ops.operands().reserve(code.operands().size());

  Forall_operands(it1, code)
  {
    if(it1->is_nil()) continue;

    codet &code_op=to_code(*it1);

    if(code_op.get_statement()==ID_label)
    {
      // these may be nested
      codet *code_ptr=&code_op;

      while(code_ptr->get_statement()==ID_label)
      {
        assert(code_ptr->operands().size()==1);
        code_ptr=&to_code(code_ptr->op0());
      }

      //codet &label_op=*code_ptr;

      new_ops.move_to_operands(code_op);
    }
    else
      new_ops.move_to_operands(code_op);
  }

  code.operands().swap(new_ops.operands());
}