bench test error Alt-Ergo Unsupported operator rotl

[felixL-K]

Nummber of tests : 1 Tests: 669 Error: owi: internal error, uncaught exception: Failure("Bv: Unsupported binary operator "rotl"") Raised at Stdlib__Domain.join in file "domain.ml", line 258, characters 16-24 Called from Stdlib__Array.iter in file "array.ml", line 92, characters 31-48 Called from Owi__Wq.read_as_seq in file "src/data_structures/wq.ml", line 17, characters 4-16 Called from Owi__Cmd_sym.print_and_count_failures.aux in file "src/cmd/cmd_sym.ml", line 133, characters 10-20 Called from Owi__Cmd_sym.handle_result in file "src/cmd/cmd_sym.ml", line 199, characters 4-190 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24 Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

[redianthus]

implement it in smtml?

[hra687261]

The error is fixed, but a new one occurs, in which rotate_left is called with two bit-vectors, not a numeral and a bit-vector (as expected from the smt-lib https://smt-lib.org/logics-all.shtml). Not sure if we can define it since the function expects a numeral (constant integer) not an (eventually symbolic) bit-vector term. (cc @filipeom)

[filipeom]

The error is fixed, but a new one occurs, in which rotate_left is called with two bit-vectors, not a numeral and a bit-vector (as expected from the smt-lib https://smt-lib.org/logics-all.shtml). Not sure if we can define it since the function expects a numeral (constant integer) not an (eventually symbolic) bit-vector term. (cc @filipeom)

~Possibly fixed by formalsec/smtml#353? Altough I don't think there will be rotations where n is symbolic, we should probably continue using the binary operator Rot{l|r} (Which with the PR will now have a new API: Ext_rotate_{left|right}) because z3 by defaults supports symbolic rotations I believe.~

[filipeom]

Also when I run the rotate_left test in smtml with alt-ergo I get:

$ dune exec -- smtml run test/cli/smt2/test_bitv_rotl.smt2 --solver alt-ergo
sat                                    
smtml: internal error, uncaught exception:
       File "src/smtml/altergo_mappings.default.ml", line 315, characters 23-29: Assertion failed
       Raised at Smtml__Altergo_mappings.M.Make.Model.eval.(fun) in file "src/smtml/altergo_mappings.default.ml", line 315, characters 23-35
       Called from Stdlib__Map.Make.fold in file "map.ml", line 329, characters 19-42
       Called from AltErgoLib__ModelMap.fold in file "src/lib/structures/modelMap.ml" (inlined), line 145, characters 2-21
       Called from Smtml__Altergo_mappings.M.Make.Model.eval in file "src/smtml/altergo_mappings.default.ml", lines 308-318, characters 10-32
       Called from Smtml__Mappings.Make.Make_.value_of_term in file "src/smtml/mappings.ml", line 738, characters 14-59
       Called from Smtml__Mappings.Make.Make_.values_of_model.(fun) in file "src/smtml/mappings.ml", line 790, characters 20-56
       Called from Stdlib__Map.Make.iter in file "map.ml", line 305, characters 20-25
       Called from Smtml__Mappings.Make.Make_.values_of_model in file "src/smtml/mappings.ml", lines 788-792, characters 8-13
       Called from Stdlib__Option.map in file "option.ml", line 24, characters 57-62
       Called from Smtml__Interpret.Make.eval in file "src/smtml/interpret.ml", line 44, characters 18-37
       Called from Smtml__Interpret.Make.loop in file "src/smtml/interpret.ml", line 70, characters 28-60
       Called from Dune__exe__Cmd_run.run.run_file.(fun) in file "src/bin/cmd_run.ml", line 54, characters 21-49
       Called from Stdlib__Fun.protect in file "fun.ml", line 34, characters 8-15
       Re-raised at Stdlib__Fun.protect in file "fun.ml", line 39, characters 6-52
       Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
       Called from Dune__exe__Cmd_run.run in file "src/bin/cmd_run.ml", line 87, characters 14-52
       Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
       Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

[hra687261]

Did something change in the Symbols.ml module? In the mapping I use Symbol.make to create the smtml symbol that corresponds to a dolmen/alt-ergo symbol and with this function the namespace is var (so the x I create from the model is a var) while the symbols in the ctx have the namespace term. So the solution should be either to change the Symbol.make to allow it to take the namespace as an argument and then change aeid_to_sym in alt-ergo's mapping to make it provide the namespace term in the call to Symbol.make, or use the same namespace for the symbols in ctx and those that are created with Symbol.make.

[filipeom]

Did something change in the Symbols.ml module? In the mapping I use Symbol.make to create the smtml symbol that corresponds to a dolmen/alt-ergo symbol and with this function the namespace is var (so the x I create from the model is a var) while the symbols in the ctx have the namespace term.

So yeah, the parsed symbol is given from the dolmen parser and is going to have namespace term.

So the solution should be either to change the Symbol.make to allow it to take the namespace as an argument and then change aeid_to_sym in alt-ergo's mapping to make it provide the namespace term in the call to Symbol.make, or use the same namespace for the symbols in ctx and those that are created with Symbol.make.

Couldn't we just make Symbol.make create symbols with namespace term instead of var? This fixes the issue and the tests seem to be running ok.

[hra687261]

Couldn't we just make Symbol.make create symbols with namespace term instead of var? This fixes the issue and the tests seem to be running ok.

Yes it should, I just don't know if Symbol.make is used somewhere else where the namespace has to be var

[filipeom]

I checked quickly, and I think it's only ever when the namespace should be var. In any case, I adjusted the documentation just in case as well https://github.com/formalsec/smtml/pull/354

[filipeom]

Also, formalsec/smtml#355 should fix https://github.com/OCamlPro/owi/issues/637#issuecomment-2889089206 at least in the case where the number of bits to rotate is concrete.

[hra687261]

Great! Thanks!

[filipeom]

I didn't know I could close this by referencing it in the smtml repo. I'll run this locally to ensure it is indeed fixed 😅

[filipeom]

So, it seems that formalsec/smtml#356 was needed. But now I'm getting this weird behaviour where sometimes it crashes and other times it finishes:

$ dune exec -- owi c --unsafe testcomp/sv-benchmarks/c/hardware-verification-bv/btor2c-lazyMod.vis_QF_BV_rotate32.c --solver alt-ergo
owi: internal error, uncaught exception:
     File "src/lib/structures/expr.ml", line 952, characters 4-10: Assertion failed
     Raised at Stdlib__Domain.join in file "domain.ml", line 299, characters 16-24
     Called from Stdlib__Array.iter in file "array.ml", line 113, characters 31-48
     Called from Owi__Wq.read_as_seq.(fun) in file "src/data_structures/wq.ml", line 17, characters 4-16
     Called from Owi__Cmd_sym.print_and_count_failures.aux in file "src/cmd/cmd_sym.ml", line 127, characters 10-20
     Called from Owi__Cmd_sym.handle_result in file "src/cmd/cmd_sym.ml", lines 197-199, characters 4-45
     Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
     Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

$ dune exec -- owi c --unsafe testcomp/sv-benchmarks/c/hardware-verification-bv/btor2c-lazyMod.vis_QF_BV_rotate32.c --solver alt-ergo
owi: [ERROR] Assert failure: false      
model {
  symbol symbol_0 i32 0
  symbol symbol_1 i32 0
  symbol symbol_2 i32 30
  symbol symbol_3 i32 0
  symbol symbol_4 i32 1
  symbol symbol_5 i32 30
  symbol symbol_6 i32 0
  symbol symbol_7 i32 -1431655766
  symbol symbol_8 i32 30
  symbol symbol_9 i32 0
  symbol symbol_10 i32 0
  symbol symbol_11 i32 0
  symbol symbol_12 i32 0
  symbol symbol_13 i32 0
}
owi: [ERROR] Reached problem!

Here are two execution of the same command (one right after the other)

[redianthus]

It is expected that two runs may lead to a different output with many workers, you can add -w1 to get something more deterministic. It seems to be crashing somewhere else, so it may be one of the other issues ? It looks similar to #650 #640 and #644

[filipeom]

It is expected that two runs may lead to a different output with many workers, you can add -w1 to get something more deterministic. It seems to be crashing somewhere else, so it may be one of the other issues ? It looks similar to #650 #640 and #644

With -w1 I cannot reproduce the assert failure 😅. But when I use -w 2 it appears to be triggering the same assert failure as this issue: #644

[redianthus]

OK, then I guess we can close this one and investigate #644 separately?

Once we believe everything is fixed, we'll do another Test-Comp run to check if we missed some anyway :)