remove_asm now guarantees that functions called exist by kroening · Pull Request #2642 · diffblue/cbmc

kroening · 2018-07-31T11:17:04Z

This fixes the problem that remove_asm introduces calls to functions that subsequently don't exist in the function_map.

Consequently, it is now no longer required to do goto_conversion after remove_asm(), greatly simplifying the use of remove_asm().

smowton · 2018-07-31T11:20:07Z

I presume it is no coincidence this appears concurrently with @polgreen's #2636

smowton · 2018-07-31T11:21:48Z

src/goto-programs/remove_asm.cpp

    symbol_table.add(symbol);
  }
+
+  if(goto_functions.function_map.find(function_identifier)==


insert / emplace?

+1 on this suggestion. This may require adding a constructor to goto_functiont.

tautschnig

It seems this might fix #2631; if so, a test needs to be added. The GitHub PR comment is very helpful (and indicates that a bug is fixed), but unfortunately the commit message lacks all such information. Please fix.

polgreen · 2018-07-31T11:27:15Z

This is going to have the same problem as I have in my PR as soon as you introduce tests:

windows CI won't deal with __asm__ __volatile__ ("mfence": : :"memory");
CBMC doesn't treat __asm mfence in the same way as __asm__ __volatile__ ("mfence": : :"memory");.

As a result you won't be able to have any tests without including a hack like I have done in my PR.

I also don't think it is the right fix to force every function to be added to the function_map. All other places in CBMC, where the function map is accessed, if the function is not found in the map it is treated as having no body.

kroening · 2018-07-31T12:07:34Z

I'll re-use the test in #2631 once that's merged. This PR will eliminate the need for the 'windows hack'.

allredj

Passed Diffblue compatibility checks (cbmc commit: b8c86e7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80492971

allredj

This PR failed Diffblue compatibility checks (cbmc commit: d81a713).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80494821
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

kroening · 2018-07-31T13:34:53Z

This now removes the need for the 'hack' in #2636

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 21feec4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80498081
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: 45141d4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80502428

polgreen · 2018-08-06T08:16:35Z

I would be very keen on this being merged. It appears that assembly functions not appearing in the function map causes a multitude of issues all over the place.

tautschnig

Approving with a couple of requests that I'd really like to see addressed...

tautschnig · 2018-08-08T12:33:33Z

src/goto-programs/remove_asm.cpp

    symbol_table.add(symbol);
  }
+
+  if(goto_functions.function_map.find(function_identifier)==


+1 on this suggestion. This may require adding a constructor to goto_functiont.

tautschnig · 2018-08-08T12:35:36Z

src/goto-programs/remove_asm.cpp

-  remove_asmt(
-    symbol_tablet &_symbol_table,
-    goto_functionst &_goto_functions)
+  remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)


Nit picking, but should this change possibly go in the previous commit?

Yes, will now happen after merging this, then rebasing #2714

tautschnig · 2018-08-08T12:36:36Z

src/goto-programs/remove_asm.cpp

    symbol.type=fkt_type;
    symbol.base_name=function_base_name;
    symbol.value=nil_exprt();
+    symbol.mode = ID_C;


This is an important bugfix that may warrant its own commit (and regression test - @polgreen may have one).

Moved to PR #2711

tautschnig · 2018-08-08T12:37:57Z

src/goto-programs/remove_asm.cpp

+    process_instruction_msc(code, dest);
+  else
+  {
+    // ignore


I'd rather see UNIMPLEMENTED or the likes here. Those silent failures have bitten us before.

Moved to PR #2714

kroening · 2018-08-10T14:33:35Z

On using emplace instead of if(find()==end()) { insert() }
I don't like this for two reasons:

Emplace doesn't actually guarantee that the constructor isn't run, which is the expensive thing here.
Emplace is much harder to read.
Any STL implementation I know uses finger search, i.e., the find ... insert idiom isn't slower than insert.

tautschnig · 2018-08-10T15:39:25Z

src/goto-programs/remove_asm.cpp

+
+  if(
+    goto_functions.function_map.find(function_identifier) ==
+    goto_functions.function_map.end())


Nit picking: I'd still like to see using .insert or .emplace here instead of the redundancy of doing .find plus .operator[].

Ah, sorry, I hadn't seen #2642 (comment). In response to that: I believe insert will always do find + insert-with-hint, which ought to be faster. But indeed it's very minor.

4f5e148 Merge pull request diffblue#2713 from thk123/dump/expr2c-configuration 01b7418 Merge pull request diffblue#2710 from thomasspriggs/tas/struct_component b763877 Merge pull request diffblue#2737 from diffblue/remove-appveyor 9c3fd45 Add AWS CodeBuild badges 4261fd8 Remove appveyor badge fe23db7 Remove appveyor.yml 21857a7 Add support for getting components by name to `struct_exprt` 05993f4 Merge pull request diffblue#2727 from tautschnig/fptr-debug 0ecd008 Merge pull request diffblue#2701 from antlechner/antonia/enum-constants 159bf15 Merge pull request diffblue#2205 from diffblue/rename_symbol_type 5ca6cd2 Restrict new clinit_wrapper calls to enum types 6e04213 Reformatting the structs to aid readability 0cfacb8 Add type2c conversion for specifying a type name c3fef70 Add a clean configuration for expr2c 3a40db1 Make expr2ct configurable in a number of ways 097cf71 Merge pull request diffblue#2731 from diffblue/increase-version 170c1ea Merge pull request diffblue#2730 from diffblue/parent-child-invariant c9e46ae Temporarily remove new UNREACHABLE statements 03e3877 Add tests for nondet initialization of enums 3e32140 CI lazy methods: load clinit for all param types 5542c54 Move nondet enum initialization to new function 6ecf4f9 Nondet-init enums by assigning them to a constant 6c84caa Refactor logic for generating a nondet int 07d1e44 Always run clinit_wrapper before nondet object init 3be826f Add some documentation to java_object_factory 5e80310 add invariant on parent-child class relationship 2cf1931 Merge pull request diffblue#2661 from jeannielynnmoulton/jeannie/JavaMethodType c6acc9c increased version number in preparation for release 5.10 0ee4178 Merge pull request diffblue#2729 from tautschnig/add-sub-conflict f5aff56 Merge pull request diffblue#2705 from danpoe/feature/replace-function-calls 89048e6 Function-pointer remvoval: print human-friendly debug messages 1fc3118 Use pointer difference type when adding to pointer 072b592 Merge pull request diffblue#2726 from tautschnig/java-loc 4dca215 Goto program should not use java_method_typet 273fff4 Add can_cast_type and precondition. 6cb7e5d Reinstate require_code and add require_java_method 78f7cb7 Refactor constructors for java_method_typet 6cefc61 Unit tests conversion from code_typet to java_method_typet c3b8b5a Update tag in to_java_method_type 972315a Update docs on java_method_typet constructor 211931c Add tag for java_method_type 551df9c Update unit tests to use java_method_typet da18c9f Change variables named code_type to method_type f1bd41e Change code_typet to java_method_typet in jbmc be3c4c6 Merge pull request diffblue#2430 from tautschnig/vs-function-id 03fa885 Replace function calls c4d79ab Java string preprocessing: use provided source location fb0c552 Java string preprocessing: use and document parameter function_id c31edca Merge pull request diffblue#2725 from tautschnig/replace-symbolt-code-type 2c1fc06 Merge pull request diffblue#2721 from tautschnig/replace_symbol-cleanup2 8211a78 Merge pull request diffblue#2722 from tautschnig/cleanup-valuest 30bc071 Add "// empty last line" to options list in goto_instrument_parse_options.h 8c8801c List source files in goto-programs/Makefile in lexicographic order 40d28ae replace_symbolt: report replacements in code_typet::return_type 4b9df3b Revert "Ignore return value" e39ea2e Merge pull request diffblue#2683 from karkhaz/kk-continue-unsafe 424ab4f --stop-on-fail now stops on failed path 545bff8 Add clear() to path exploration worklist 95d8d0f Generalise option setting from strategy unit tests e85fb77 Cleanup constant_propagator_domaint::valuest 18d08bf Merge pull request diffblue#2719 from tautschnig/quiet-unit-tests 30d557a Constant propagation: Check type consistency before adding to replacement map a5ce621 Make unit tests quiet 61b3086 Merge pull request diffblue#2468 from tautschnig/vs-names 7bfd36b Merge pull request diffblue#2714 from diffblue/msvc-asm 3785941 Remove names of unused parameters af79cb9 add support for Visual Studio style inline assembler 254b4d4 Merge pull request diffblue#2642 from diffblue/remove_asm_fix 26009a3 remove_asm now guarantees that functions called exist 9c10f38 Merge pull request diffblue#2716 from tautschnig/fix-buildspec c3b2beb Merge pull request diffblue#2635 from qaphla/move_is_lvalue e247a29 CodeBuild: Remove empty artifact stanza 756018d Merge pull request diffblue#2709 from owen-jones-diffblue/doc/how-to-run-tests bba5dea Merge pull request diffblue#2699 from diffblue/goto-cc-clang 355fbd2 avoid assert() 6178908 bump goto binary version f93deec type symbols now use ID_symbol_type 22b755a Merge pull request diffblue#2711 from diffblue/mode-gcc-asm-functions cf75535 Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation 5c06786 set mode for functions added by remove_asm ef53b65 Update description of regression test framework 312ca1d Add section to documentation about running tests d7ddf59 Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location 119e88b Pass location around for nondet initialization 50660db Specify source location for nondet expressions d1f2ad9 Replace -> with → e448db6 Merge pull request diffblue#2708 from owen-jones-diffblue/coding-standard-class-comments 519370d State that identifiers should be good 30d29b9 Replace unicode arrows → with ascii ones -> 611374f Document classes and member variables unless obvious adb7ef0 Minor fixes to documentation outline fd4f563 Add side_effect_exprt constructor with location 98657d8 Merge pull request diffblue#2668 from diffblue/expose_remove_preconditions 6a36fa4 Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide 61a8c30 Merge pull request diffblue#2666 from NlightNFotis/invariant_changes c0bcce7 use clang as native compiler for goto-clang 1f19e23 goto-cc: use result of our native compiler detection d9d9e2a Merge pull request diffblue#2692 from diffblue/follow-tags f94d5e2 follow union, struct and enum tags 99e33bd fix typo in comments for struct_tag_typet 1f53246 expose remove_preconditions f212505 Avoids using expr.op0 when type is known 7b36ca2 Moves is_lvalue to expr_util.c 4782b48 Fix invariant regression tests efb1c40 Refactor invariant_failedt definition. 515f050 Pass the condition to the invariant_failedt constructor. bf6dd9e Added extra use-case hints to the already present invariant definitions. 612b4f8 Address review comments 7233f92 Rearrange everything into separate pages 1cb3cdd Move other tools into a separate file 82eefb7 Fix links between files d9e690b Move folder walkthrough to a separate file 2939db4 Address review comments 8d5cbcb Create CBMC developer guide documentation git-subtree-dir: cbmc git-subtree-split: 4f5e148

kroening assigned tautschnig Jul 31, 2018

kroening requested a review from tautschnig July 31, 2018 11:17

kroening requested review from peterschrammel, pkesseli and smowton as code owners July 31, 2018 11:17

smowton approved these changes Jul 31, 2018

View reviewed changes

tautschnig requested changes Jul 31, 2018

View reviewed changes

kroening force-pushed the remove_asm_fix branch from d81a713 to 21feec4 Compare July 31, 2018 11:59

allredj reviewed Jul 31, 2018

View reviewed changes

kroening force-pushed the remove_asm_fix branch from 21feec4 to 45141d4 Compare July 31, 2018 13:33

allredj reviewed Jul 31, 2018

View reviewed changes

kroening added the bugfix label Aug 1, 2018

polgreen mentioned this pull request Aug 3, 2018

Make goto_rw slightly less conservative [depends-on: #3769, blocks: #2677, #2694] #2646

Closed

polgreen mentioned this pull request Aug 7, 2018

goto-analyser simplify generates binary that can't be analyzed with goto-instrument #2689

Open

tautschnig approved these changes Aug 8, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Aug 8, 2018

kroening force-pushed the remove_asm_fix branch from 45141d4 to 95e7c4a Compare August 10, 2018 14:22

kroening mentioned this pull request Aug 10, 2018

add support for Visual Studio style inline assembler #2714

Merged

tautschnig approved these changes Aug 10, 2018

View reviewed changes

kroening force-pushed the remove_asm_fix branch from 95e7c4a to 84f7eac Compare August 10, 2018 18:30

tautschnig force-pushed the remove_asm_fix branch from 84f7eac to 56697be Compare August 11, 2018 09:14

remove_asm now guarantees that functions called exist

26009a3

tautschnig force-pushed the remove_asm_fix branch from 56697be to 26009a3 Compare August 11, 2018 09:50

tautschnig merged commit 254b4d4 into develop Aug 11, 2018

tautschnig deleted the remove_asm_fix branch August 11, 2018 10:21

Conversation

kroening commented Jul 31, 2018

Uh oh!

smowton commented Jul 31, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

polgreen commented Jul 31, 2018

Uh oh!

kroening commented Jul 31, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Jul 31, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

polgreen commented Aug 6, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Aug 10, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants