Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to debug Match exceptions when using code_...

Email Gateway (Aug 20 2021 at 09:58):

From: Mark Utting <m.utting@uq.edu.au>
Dear Isabelle users,

Can anyone suggest how I might debug a Match exception error in a ‘value’ command?
(We are using code_pred to generate code for some large inductive definitions).
The error says:
exception Match raised (line 8703 of "generated code")

I’ve tried using export_code to generate the SML code corresponding to the code_pred.
But the line numbers in the generated code (only 8393 lines) do not match the above error.

If I try to run the generated export.ML file directly:
$ isabelle process -o ML_exception_debugger=true -o ML_debugger=true -f export.ML
It just reports an equally unhelpful error message, with no line number this time:
Exception- Match raised
Error trying to use the file: 'export.ML'

I’ve also tried turning on some debugger flags, but get no extra output:
$ isabelle process -o ML_exception_debugger=true -o ML_debugger=true -f export.ML

Is there any way of tracing the execution?

Or seeing the actual code that is being executed?

Or generating a full exception stack trace?

Thanks
Mark

PS. A subset of our definitions is:

inductive object_test :: "Program ⇒ Signature ⇒ Value list ⇒ (Value ⇒ FieldRefHeap ⇒ bool) => bool"
where
InitStatics:
"⟦Some init = prog '''';
config0 = (init, 0, new_map_state, ps);
prog ⊢ ([config0, config0], new_heap) | [] ⟶* ((end1 # xs1), heap1) | l1;

Some g = prog m;
config1 = (g, 0, new_map_state, ps);
prog ⊢ ([config1, config1], heap1) | [] ⟶* ((end2 # xs2), heap2) | l2;
result = get_result end2;
checker result heap2 ⟧
⟹ object_test prog m ps checker" |

NoStatics:
"⟦'''' ∉ dom prog;
Some g = prog m;
config1 = (g, 0, new_map_state, ps);
prog ⊢ ([config1, config1], new_heap) | [] ⟶* ((end2 # xs2), heap2) | l2;
result = get_result end2;
checker result heap2 ⟧
⟹ object_test prog m ps checker"

code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ bool as testObj) object_test .
thm object_test.equation (* view the code_pred equations *)

export_code testObj in SML module_name TestObj

fun check_result_2 :: "Value ⇒ FieldRefHeap ⇒ bool" where
"check_result_2 (ObjRef x) h = (h_load_field ''value'' x h = (IntVal32 (120)))" |
"check_result_2 _ _ = False"

(* this throws exception Match raised (line 8703…) *)
value "object_test unit_factAsAnObject_2 ''FactResult'' [(IntVal32 (5))] check_result_2"

Associate Professor Mark Utting
MSc Waikato, PhD UNSW
Discipline Leader, Cyber Security and Software Engineering

School of Information Technology and Electrical Engineering
The University of Queensland
Brisbane Qld 4072 Australia

T +61 7 3365 2386
E m.utting@uq.edu.au<mailto:m.utting@uq.edu.au> W https://cyber.uq.edu.au<https://cyber.uq.edu.au/>

CRICOS Provider: 00025B

[https://support.staff.uq.edu.au/ci/inlineImage/get/4826099/277631508108acd58f44b90a9297a394]

The University of Queensland is embracing the Green Office philosophy. Please consider the environment before printing this email.

This email (including any attached files) is intended solely for the addressee and may contain confidential information of The University of Queensland. If you are not the addressee, you are notified that any transmission, distribution, printing or photocopying of this email is prohibited. If you have received this email in error, please delete and notify me. Unless explicitly stated, the opinions expressed in this email do not represent the official position of The University of Queensland.
image001.jpg

Email Gateway (Aug 20 2021 at 10:31):

From: Florian Märkl <isabelle-users@florianmaerkl.de>
Hi Mark,

it’s hard to reproduce your particular case without the definitions around, but here is a small example to get an exception trace:

definition broken_deeper :: "nat ⇒ nat" where "broken_deeper n ≡ case n of 0 ⇒ 42"
definition broken :: "nat ⇒ nat" where "broken n ≡ broken_deeper n"
definition some_arg :: nat where "some_arg ≡ 42"

declare [[ML_debugger]]
ML‹Runtime.exn_debugger (fn () => @{code ‹broken›} @{code ‹some_arg›})›

I recently had to figure this out too and was quite confused by all the different options that exist, but eventually this message by Makarius got me on the right track: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-May/msg00136.html

Cheers
Florian

Last updated: Jul 15 2022 at 23:21 UTC