Error on recursive functions in Java about cbmc HOT 11 CLOSED

Replacing '.' in the variable names will be necessary in java test case generation, as it is not allowed in java identfiers. Doing it already before would reduce work there, too.

from cbmc.

I have added regression/cbmc-java/recursion1 for this.

from cbmc.

I'm afraid recursion is still broken: see #163.

from cbmc.

tail recursion does work:

public class recursion1
{
  static int f(int n)
  {
    if(n <= 0)
      return 1;
    else
      return n * f(n-1);
  }

  static int g(int n, int acc)
  {
    if(n <= 0)
      return acc;
    else
      return g(n-1, n*acc);
  }

  public static void main(String[] args)
  {
    assert f(1)==1;
    assert g(1, 1) == 1;
  }
}

from cbmc.

Seems likely that the cause is Java locals not getting declared or added to the symtab (while temp variables are registered), so goto_symext::locality doesn't spot it as a thing to rename at inlining sites. However straightforwardly adding symbol registration and variable declaration in the same way as new_tmp_symbol doesn't seem to fix matters.

from cbmc.

Doh. ssa_exprt.h:73 assumes that identifiers can't contain periods, but Java package names do, leading to symbol identifiers like package.function::arg0, leading to a bad l1 object identifier and use of the wrong version of a variable.

Solutions:
(1) Escape Java package identifiers (I bet there are some sites looking for last-instance-of-period to find a class name that'll need finding and fixing)
(2) Allow periods in identifier names. Likely there are more places in the codebase that don't like them?

(1) sounds like marginally less pain. Put an assert in the symtab / symbol_exprt code to check for a legal name on registration / lookup.

In the meantime flipping #if 0 at line 67 results in correct behaviour. @kroening want to give an opinion of god on this?

Note that the fix for locality above is still required however, but it takes a slightly different test case to show it.

from cbmc.

smowton@48118d5: Local variable registration
smowton@3f8bab9: Workaround to tolerate Java IDs
smowton@75e46e8: Test case exhibiting need for local registration (otherwise int arg_copy gets overwritten by the recursive call)

from cbmc.

@mgudemann at the symtab level we'll need to use something illegal in Java IDs anyhow though, otherwise the uniqueing to avoid clashes between e.g. java_lang_Object_equals and a local that actually has that name will drive us insane

I won't make the change right now since I'm about to go on holiday and it'd seem rude to do it and leave everyone to find all the knock-on consequences, so for now just noting it needs doing :)

from cbmc.

Fixed in Cristina's test_gen branch

from cbmc.

@kroening having taken a fresh look at this today, possible options:

• Mangle Java (and other language) names to remove syntactic ambiguity for struct member vs. namespace (i.e. s/./::/) (substantial cleanup of every instance using . to find the class/namespace boundary)
• Change ssa_exprt::build_identifier to use a different character for the object/member boundary (less natural, risk of code assuming that . is used)
• Change ssa_exprt::build_identifier to store the L1 object identifier, or its offset, as a separate attribute of ssa_exprt (extra memory usage)

Any preference?

from cbmc.

No comment being forthcoming, how about just doing this: https://github.com/smowton/cbmc/tree/ssa_l1_id

from cbmc.