Remove ARINC analyses by michael-schwarz · Pull Request #812 · goblint/analyzer

michael-schwarz · 2022-08-02T16:46:09Z

This removes the ARINC analyses from the current version of Goblint, they will remain available in the last release.

References #811

sim642 · 2022-08-02T17:20:46Z

On top of my head, I remember there are these (de)obfuscations related to ARINC as well: #460 (comment) and #460 (comment).

michael-schwarz · 2022-08-03T07:19:56Z

The second one was already removed before, I also removed the first now.

sim642 · 2022-08-03T07:21:57Z

The second one was already removed before, I also removed the first now.

Unless I'm mistaken, it's still there on the current master:

analyzer/src/util/goblintutil.ml

Lines 121 to 135 in 26fd6ce

    
           let scrambled = try Sys.getenv "scrambled" = "true" with Not_found -> false 
        
           (* typedef struct { 
        
              PROCESS_NAME_TYPE      NAME; 
        
              SYSTEM_ADDRESS_TYPE    ENTRY_POINT; 
        
              STACK_SIZE_TYPE        STACK_SIZE; 
        
              PRIORITY_TYPE          BASE_PRIORITY; 
        
              SYSTEM_TIME_TYPE       PERIOD; 
        
              SYSTEM_TIME_TYPE       TIME_CAPACITY; 
        
              DEADLINE_TYPE          DEADLINE; 
        
              }                        PROCESS_ATTRIBUTE_TYPE; *) 
        
           let arinc_name          = if scrambled then "M161" else "NAME" 
        
           let arinc_entry_point   = if scrambled then "M162" else "ENTRY_POINT" 
        
           let arinc_base_priority = if scrambled then "M164" else "BASE_PRIORITY" 
        
           let arinc_period        = if scrambled then "M165" else "PERIOD" 
        
           let arinc_time_capacity = if scrambled then "M166" else "TIME_CAPACITY"

michael-schwarz · 2022-08-03T07:23:22Z

Before your comment is what I meant by before 😉

sim642 · 2022-08-03T08:12:54Z

Ah, sorry, right.

The test fails on MacOS. I guess it's because memcpy might be a wrapper/macro for some other internal (fortified?) function there. The solution probably is to handle some extra name variant of it (not sure what exactly).
It's odd though because #391 also contains a similar change, but doesn't show a similar failure.

michael-schwarz · 2022-08-03T08:21:27Z

Yes, it looks like it should be __builtin___memcpy_chk. However, for some reason than the assert succeeds instead of definitely failing, so there still is something fishy going on.

michael-schwarz · 2022-08-03T08:48:04Z

Actually, the memcpy is a bit insane. It is broken if you pull out the AddrOf to somewhere else as it does not in fact dereference its argument 🙃.

void test_memcpy_two() {
  int dest = 0;
  int src = 1;

  int* destp = &dest;
  int* srcp = &src;

  memcpy(destp, srcp, sizeof(int));

  __goblint_check(dest == 0); //FAIL
  __goblint_check(src == 1);
}

sim642 · 2022-08-03T09:39:33Z

However, for some reason than the assert succeeds instead of definitely failing, so there still is something fishy going on.

It was actually unknown instead of fail, which makes sense, because it fell back to the unknown function handling via LibraryFunctions, which handles __builtin___memcpy_chk by completely invalidating the destination. The result of that could also be 0 then.

It is broken if you pull out the AddrOf to somewhere else as it does not in fact dereference its argument upside_down_face.

That's what #729 also fixed but it's still just on interactive.

sim642

There's also src/extract/pml_arinc.ml.

src/analyses/base.ml

CHANGES: Goblint "lean" release after a lot of cleanup. * Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474). * Add interactive analysis (goblint/analyzer#391). * Add server mode (goblint/analyzer#522). * Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448). * Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419). * Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722). * Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595). * Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655). * Add pthread extraction to Promela (goblint/analyzer#220). * Add location spans to output (goblint/analyzer#428, goblint/analyzer#449). * Improve race reporting (goblint/analyzer#550, goblint/analyzer#551). * Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785). * Refactor warnings (goblint/analyzer#55, goblint/analyzer#783). * Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499). * Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675). * Add bash completion (goblint/analyzer#669). * Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).

michael-schwarz added 2 commits August 2, 2022 18:26

Drop ARINC support

4e9f94a

Remove presub

3836a4d

michael-schwarz added the cleanup Refactoring, clean-up label Aug 2, 2022

michael-schwarz added this to the v2.0.0 milestone Aug 2, 2022

michael-schwarz requested a review from sim642 August 2, 2022 16:46

michael-schwarz added 2 commits August 3, 2022 08:32

Remove obfuscated library functions

9b969c4

Merge branch 'master' into issue_811

368a654

michael-schwarz mentioned this pull request Aug 3, 2022

Remove unmaintained features #460

Closed

14 tasks

michael-schwarz added 2 commits August 3, 2022 11:10

Cleanup memcpy

e73ee03

Add second memcopy test

e18ccea

sim642 reviewed Aug 3, 2022

View reviewed changes

src/analyses/base.ml Outdated Show resolved Hide resolved

michael-schwarz added 2 commits August 3, 2022 12:46

Rm spurious memset

54b9bfd

Rm pml_arinc and plm

52ff270

michael-schwarz requested a review from sim642 August 3, 2022 11:18

sim642 approved these changes Aug 3, 2022

View reviewed changes

michael-schwarz merged commit d887244 into master Aug 3, 2022

michael-schwarz deleted the issue_811 branch August 3, 2022 11:20

sim642 mentioned this pull request Aug 3, 2022

Add static module for top-level Control Spec context #801

Merged

sim642 mentioned this pull request Aug 18, 2022

[new release] goblint (2.0.0) ocaml/opam-repository#21998

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove ARINC analyses#812

Remove ARINC analyses#812
michael-schwarz merged 8 commits intomasterfrom
issue_811

michael-schwarz commented Aug 2, 2022

Uh oh!

sim642 commented Aug 2, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

sim642 commented Aug 3, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

sim642 commented Aug 3, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

sim642 commented Aug 3, 2022

Uh oh!

sim642 left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

michael-schwarz commented Aug 2, 2022

Uh oh!

sim642 commented Aug 2, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

sim642 commented Aug 3, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

sim642 commented Aug 3, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

michael-schwarz commented Aug 3, 2022

Uh oh!

sim642 commented Aug 3, 2022

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants