utf8 to utf16 conversion and utf16 to ascii

[romainbrenguier]

Adds functions to util/unicode.cpp to convert from utf8 strings to utf16, both for little and big endian encodings and a function to pretty print utf16 characters in ascii.
These conversions are useful for the string refinement because utf16 is used by java.
Note that codecvt does not come automatically with old version of gcc, so I saw compilation problems with gcc-4.8 (Ubuntu 16.04), but none with gcc-6.

[tautschnig]

It may be acceptable to spell out big_endian (and, below, little_endian). Don't make others decipher names.

[tautschnig]

Is there some macro or named constant that can be used in place of the hex value? Else it would be nice to have some comment explaining why it's exactly this bit pattern.

Also, the line should be broken somewhere before the 80th (or even 70th) character.

[romainbrenguier]

Unfortunately I couldn't find such a constant, this is in fact the default for this template, hopefully this commit af792fe makes it a bit clearer

[tautschnig]

Unrelated to the code: the commit message should be cleaned, we don't really care about that conflict anymore.

[tautschnig]

Is this function missing a declaration in unicode.h?

[tautschnig]

No whitespace around `<=' but do add whitespace after ","

[tautschnig]

Missing whitespace after ","

[martin-cs]

May I suggest the test given at the end of this article: https://mathiasbynens.be/notes/javascript-unicode HTH

[romainbrenguier]

@martin-cs The following test is handled correctly by the solver:

class test
{
    public static void main(String[] args)
    {
	String s="💩Iñtërnâtiônàlizætiøn☃";
	System.out.println(s.length());
	System.out.println(s.codePointAt(0));
	assert(s.length() == 23);
	assert(s.codePointAt(0) == 128169);
    }
}

Note however that the current solver is not able to check the same program for codePoint other than 0 (correspondence between code point and the actual index can be complicated in general).

[martin-cs]

Cool; just thought that it might be a good test to add to find awkward issues with multi-byte UTF16.

[tautschnig]

Thanks a lot for making this easier to read. Would it be possible to add some reference on where you got that magic number from?

[romainbrenguier]

I added a comment and a reference to the c++ documentation: ccbe6f7

[tautschnig]

@romainbrenguier Is the test you mentioned already part of some commit series? If it isn't it would be nice if it were added as a "FUTURE" test to this pull request (and then changed to "CORE" once all parts of the string solver are merged).

[romainbrenguier]

The following test is already marked as future in CBMC: https://github.com/diffblue/cbmc/blob/master/regression/strings/java_code_point/test_code_point.java and it illustrates the same feature. But I can still add the "💩Iñtërnâtiônàlizætiøn☃" test, should it be part of this pull request or another one?

[tautschnig]

It would be great to see the commits squashed into a single one, but otherwise it looks good to me!

[tautschnig]

Hmm, please hold off on merging this one: it seems further fixes for the travis integration of Clang are necessary in order to support codecvt.

[tautschnig]

Could you please add a commit changing .travis.yml to set COMPILER="clang++-3.7 -stdlib=libc++" and ensure that $COMPILER is quoted?

[romainbrenguier]

@tautschnig I squashed the commits and added the modification to .travis.yml you asked for c7a101a , however I'm not sure the compilation with clang++ works

[tautschnig]

It seems possibly that we'll need an explicit
- libc++-dev
line in here.

[tautschnig]

That change isn't necessary as libc++ is the default for Mac OS.

[tautschnig]

If anyone has a Ubuntu system with Clang (3.7, ideally) at hand and could help debug the issues this would be much appreciated. At present, we are blocked as merging this work would break our travis set up.

[romainbrenguier]

@tautschnig I tried the failing command on ubuntu with clang++-3.7 and reproduced the error gotten by travis but after installing libstd++-dev the error disappeared, so I don't know what's happening...

[tautschnig]

@romainbrenguier Can you include in this pull request a travis config that matches the steps you took to make things work? It seems that installing libc++-dev is the wrong library (you stated libstdc++-dev works), and probably the compiler flags need to match as well. Thanks!!!

[romainbrenguier]

@tautschnig sorry I meant libc++-dev , the travis file already mention the library I installed

[romainbrenguier]

Using -stdlib=libstdc++ instead of -stdlib=libc++ makes the problem with cctype disappear put now there is a problem with codecvt

[kroening]

Did you also try Visual Studio?

If C++ library support for the conversion isn't working yet, we might have to put our own implementation in.

[smowton]

Note: Vojtech has asked me to look into the outstanding problems here. AFAIK they are:

1. figure out how and why this can be made to work with Clang (and specifically libc++, or libstd++ too?)
2. Similarly the VS versions we target

[tautschnig]

@smowton In case you need confirmation: yes, I believe you have summarised the problems nicely.

[smowton]

Confirming Romain's findings:

• G++ 5: success
• Clang++-3.7 / libstdc++-4.9: fails (codecvt not implemented)
• Clang++-3.7 / libstdc++-5: success. Thus the install for libstdc++-5-dev is necessary.
• Clang++-3.7 / libc++: success on my local machine, but not easy to do under Travis (there is no libc++ package for Ubuntu 12.04, which Travis runs in its VMs per default. We could switch to 14.04 per https://docs.travis-ci.com/user/ci-environment/ if we wanted to CI this case). Looking at the SVN history for libc++ / codecvt this seems likely to work back to around 2013.
• Visual Studio: success according to AppVeyor, and according to MSDN this should also work back to VS 2010 (according to the COMPILING doc we only support back to 2013 anyhow)

Explanations for the comments above:

• Why does installing libstdc++-5-dev make a difference? Because Ubuntu 12.04 defaults to GCC and libstdc++ 4.9, which don't support codecvt. In the G++ Travis config we install g++-5 which pulls libstdc++-5; in the Clang case we must explicitly pull it in.
• Why does libc++ fail with a cctype error? The attempt to install libc++ isn't working at all (the package doesn't exist), and that's simply the first stdlib include in the build.

[smowton]

#541 is a probable fix (waiting for Travis + AppVeyor)

[smowton]

Fixed one other VS problem-- it doesn't have snprintf until VS 2015. Replaced with iostreams equivalent in #541.