Crashes with: Failed to renumber Goblint analyses

[michael-schwarz]

I stumbled across this because I wanted to take a look at #7.

With Goblint 9114bcc51f11f5ba921b1f0f8761d1d75cc16cb1 and GobView 1c5b81f, Gobview fails to renumber analyses, and the renumber_goblint_analyses raises a Not_found exception.

I instrumented the code with debug printouts:

// Each Goblint analysis module is assigned an ID, and this
// ID depends on the module registration order, which might
// differ from build to build. This function reorders the
// analysis list to match the native version of Goblint.
let renumber_goblint_analyses = registered_name => {
  let old_registered = Hashtbl.copy(MCP.registered);
  let old_registered_name = Hashtbl.copy(MCP.registered_name);
    Hashtbl.iter((name, id) => {
    print_endline("Currently registered analysis: " ++ name);
  }, old_registered_name);
  Hashtbl.iter((name, id) => {
    print_endline("Marshaled contains analysis: " ++ name);
  }, registered_name);
  Hashtbl.clear(MCP.registered);
  Hashtbl.clear(MCP.registered_name);
  Hashtbl.iter((name, id) => {
    print_endline("Looking for " ++ name);
    print_endline("looking for id for " ++ name);
    let old_id = Hashtbl.find(old_registered_name, name);
    print_endline("found id for " ++ name);
    let spec = Hashtbl.find(old_registered, old_id);
    print_endline("did not find spec for " ++ name);
    Hashtbl.replace(MCP.registered, id, spec);
    Hashtbl.replace(MCP.registered_name, name, id);
  }, registered_name);
};

For some reason we only find a very specific subset of analyses that is registered with MCP in Gobview, and e.g. not base ?

App.bc.js:952 Currently registered analysis:  unit
App.bc.js:952 Currently registered analysis: OSEK
App.bc.js:952 Currently registered analysis: mutex
App.bc.js:952 Currently registered analysis: mutexEvents
App.bc.js:952 Currently registered analysis: fmode
App.bc.js:952 Currently registered analysis: escape


App.bc.js:952 Marshaled contains analysis: flag
App.bc.js:952 Marshaled contains analysis: threadJoins
App.bc.js:952 Marshaled contains analysis: deadlock
App.bc.js:952 Marshaled contains analysis: threadreturn
App.bc.js:952 Marshaled contains analysis: base
App.bc.js:952 Marshaled contains analysis: maylocks
App.bc.js:952 Marshaled contains analysis: unit
App.bc.js:952 Marshaled contains analysis: OSEK
App.bc.js:952 Marshaled contains analysis: symb_locks
App.bc.js:952 Marshaled contains analysis: malloc_null
App.bc.js:952 Marshaled contains analysis: mhp
App.bc.js:952 Marshaled contains analysis: extract_osek
App.bc.js:952 Marshaled contains analysis: var_eq
App.bc.js:952 Marshaled contains analysis: term
App.bc.js:952 Marshaled contains analysis: file
App.bc.js:952 Marshaled contains analysis: condvars
App.bc.js:952 Marshaled contains analysis: access
App.bc.js:952 Marshaled contains analysis: thread
App.bc.js:952 Marshaled contains analysis: expRelation
App.bc.js:952 Marshaled contains analysis: stack_trace
App.bc.js:952 Marshaled contains analysis: mutex
App.bc.js:952 Marshaled contains analysis: mallocWrapper
App.bc.js:952 Marshaled contains analysis: OSEK2
App.bc.js:952 Marshaled contains analysis: threadid
App.bc.js:952 Marshaled contains analysis: threadflag
App.bc.js:952 Marshaled contains analysis: spec
App.bc.js:952 Marshaled contains analysis: stack_loc
App.bc.js:952 Marshaled contains analysis: mutexEvents
App.bc.js:952 Marshaled contains analysis: uninit
App.bc.js:952 Marshaled contains analysis: fmode
App.bc.js:952 Marshaled contains analysis: signs
App.bc.js:952 Marshaled contains analysis: escape
App.bc.js:952 Marshaled contains analysis: stack_trace_set
App.bc.js:952 Marshaled contains analysis: constants
App.bc.js:952 Looking for flag
App.bc.js:952 looking for id for flag

Any ideas what is happening here @sofamaniac @keremc ?

[michael-schwarz]

It appears as if those modules are not loaded at all, even if I put a printout into base at the top-level that does not happen

[sim642]

Maybe it's missing the linkall flag? I'm not sure if and how linking works in js_of_ocaml though. Or why it would suddenly have changed then.

[michael-schwarz]

I was suspecting it might be the switch to fpath: At 5162202cbb120bbbba1b53922c781e30d2a1a302 for Goblint and 91b7e22 it appears to work.

Then, I went back to the newest version, and it now for some reason manages to find everything (???), but then fails with a BatInnerIO.Output_closed from somewhere. This entire thing is super fragile.

[michael-schwarz]

The issue seems to be inside the solve here (I still see the output second one done but nothing further):

  let wrap_solver_state () =
    let module Arg = struct
      include A.PostSolverArg

      let should_prune = false
    end
  in

  print_endline("first one done");
    let module S2' =
      Constraints.GlobSolverFromEqSolver (Generic.LoadRunIncrSolver (Arg)) (EQSys) (LHT) (GHT)
    in
    print_endline("second one done");
    let r2, _ = S2'.solve [] [] [] in
    print_endline("solve done");
    new solver_state_impl r2

[michael-schwarz]

It seems we actually need to keep some of the print_endlines as print_endlines instead of Printf for the same reason as this:

  // For some reason, the standard Batteries output channels
  // appear to be closed by default and writing to them
  // raises [BatInnerIO.Output_closed]. This fixes it.
  let out = IO.output_channel(Stdlib.stdout);
  Messages.formatter := Format.formatter_of_output(out);

With this change it now seems to work mostly fine, with the oddity that I can never see the source code of the input file, as that always causes a 404 error (not sure if copying in the file was always a manual step @keremc)?

[sim642]

With this change it now seems to work mostly fine, with the oddity that I can never see the source code of the input file, as that always causes a 404 error (not sure if copying in the file was always a manual step @keremc)?

That never worked for me anyway: #2.

[keremc]

@michael-schwarz Yeah, it was always a manual step. Usually, I just symlink the source directory.

[michael-schwarz]

Hmm, maybe we should think about making that step automatic, which should make it easier for people to use?

[sim642]

Indeed it should be automatic like with g2html. The difficulty with copying/symlinking sources is making sure it all works on more complex analysis targets as well, like zstd analysis with compilation database, not just single input files.

[michael-schwarz]

True, but even if we do not get that to work in a first approximation, it would already be nice if it works for simple examples.

[michael-schwarz]

I think this issue is resolved now @stilscher?

[stilscher]

Yes it should be. Gobview is working in the current version without the mentioned error. And also the source files are copied automatically, at least for simple examples like our regression tests. Support for bigger projects like zstd still needs to be tested and probably added, but I think that can be considered a separate issue.