Module DebugAbIdealNonrel
Require
Import
Utf8
String
ToString
AdomLib
IdealExpr
AbIdealNonrel
DebugLib
DebugCminor
.
Set
Implicit
Arguments
.
Local
Open
Scope
string_scope
.
Definition
string_of_i_binary_operation
(
op
:
i_binary_operation
) :
string
:=
match
op
with
|
IOadd
=> " + "
|
IOsub
=> " − "
|
IOmul
=> " × "
|
IOdiv
=> " ÷ "
|
IOmod
=> " % "
|
IOand
=> " & "
|
IOor
=> " | "
|
IOxor
=> " ^ "
|
IOshl
=> " << "
|
IOshr
=> " >> "
|
IOaddf
=> " +. "
|
IOsubf
=> " −. "
|
IOmulf
=> " ×. "
|
IOdivf
=> " ÷. "
|
IOcmp
cmp
|
IOcmpf
cmp
=>
string_of_comparison
cmp
end
.
Definition
string_of_i_unary_operation
(
op
:
i_unary_operation
) :
string
:=
match
op
with
|
IOneg
=> "-"
|
IOnot
=> "¬"
|
IOnegf
=> "-."
|
IOabsf
=> "
absf
"
|
IOsingleofz
|
IOsingleoffloat
=> "(
single
) "
|
IOfloatofz
=> "(
float
) "
|
IOzoffloat
=> "(
Z
) "
end
.
Instance
i_binary_operation_to_string
:
ToString
i_binary_operation
:=
string_of_i_binary_operation
.
Instance
i_unary_operation_to_string
:
ToString
i_unary_operation
:=
string_of_i_unary_operation
.
Definition
print_i_unop
(
op
:
i_unary_operation
) (
x
y
:
string
) :
string
:=
to_string
op
++
x
++ " → " ++
y
.
Definition
print_i_binop
(
op
:
i_binary_operation
) (
x
y
z
:
string
) :
string
:=
x
++
to_string
op
++
y
++ " → " ++
z
.
Definition
print_backward_i_unop
(
op
:
i_unary_operation
) (
x
y
x
':
string
) :
string
:=
to_string
op
++
x
++ " = " ++
y
++ " → " ++
x
'.
Definition
print_backward_i_binop
(
op
:
i_binary_operation
) (
x
y
z
x
'
y
':
string
) :
string
:=
x
++
to_string
op
++
y
++ " = " ++
z
++ " → " ++
x
'
y
'.
Section
S
.
Context
{
t
:
Type
} (
dom
:
ab_ideal_nonrel
t
)
`(
dom_correct
:
ab_ideal_nonrel_correct
t
)
`{
ToString
t
}.
Definition
debug_ab_ideal_nonrel
:
ab_ideal_nonrel
t
:=
{|
as_leb
:=
leb_print
;
as_join
:=
join_print
;
as_meet
:=
meet_print
;
widen
:=
widen
;
const
:=
const
;
z_itv
:=
z_itv
;
forward_unop
op
x
:=
let
r
:=
forward_unop
op
x
in
let
s
:=
print_i_unop
op
(
to_string
x
) (
to_string
r
)
in
print
s
r
;
forward_binop
op
x
y
:=
let
r
:=
forward_binop
op
x
y
in
let
s
:=
print_i_binop
op
(
to_string
x
) (
to_string
y
) (
to_string
r
)
in
print
s
r
;
backward_unop
op
res
x
:=
let
r
:=
backward_unop
op
res
x
in
let
s
:=
print_backward_i_unop
op
(
to_string
x
) (
to_string
res
) (
to_string
r
)
in
print
s
r
;
backward_binop
op
res
x
y
:=
let
r
:=
backward_binop
op
res
x
y
in
let
s
:=
print_backward_i_binop
op
(
to_string
x
) (
to_string
y
) (
to_string
res
) (
to_string
r
)
in
print
s
r
;
enrich_query_chan
:=
enrich_query_chan
;
forward_var
:=
forward_var
;
backward_var
:=
backward_var
;
process_msg
:=
process_msg
;
assign_msgs
:=
assign_msgs
;
assume_msgs
:=
assume_msgs
|}.
Instance
debug_ab_ideal_nonrel_correct
:
ab_ideal_nonrel_correct
debug_ab_ideal_nonrel
_
.
Proof.
destruct
dom_correct
.
split
;
try
assumption
.
Qed.
End
S
.