Skip to content

Commit a14d9a0

Browse files
m-yacm-yac
authored
Merge pull request #1849 from GaloisInc/mrs-solver
Add basic mrsolver tactic
2 parents 239c500 + 2403b1d commit a14d9a0

File tree

9 files changed

+340
-114
lines changed

9 files changed

+340
-114
lines changed

‎examples/mr_solver/mr_solver_test_funs.sawcore

+67
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
module test_funs where
2+
3+
import Prelude;
4+
5+
test_fun0 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
6+
test_fun0 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0);
7+
8+
test_fun1 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
9+
test_fun1 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1);
10+
11+
test_fun2 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
12+
test_fun2 x = retS VoidEv emptyFunStack (Vec 64 Bool) x;
13+
14+
-- If x == 0 then x else 0; should be equal to 0
15+
test_fun3 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
16+
test_fun3 x =
17+
ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0))
18+
(retS VoidEv emptyFunStack (Vec 64 Bool) x)
19+
(retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0));
20+
21+
{-
22+
-- let rec f x = 0 in f x
23+
test_fun4 : Vec 64 Bool -> CompM (Vec 64 Bool);
24+
test_fun4 x =
25+
letRecM1
26+
(Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
27+
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (y:Vec 64 Bool) ->
28+
returnM (Vec 64 Bool) (bvNat 64 0))
29+
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) ->
30+
f x);
31+
32+
-- Alternate version of test_fun4 that uses letRecM directly
33+
test_fun4_alt : Vec 64 Bool -> CompM (Vec 64 Bool);
34+
test_fun4_alt x =
35+
letRecM
36+
(LRT_Cons (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool))
37+
LRT_Nil)
38+
(Vec 64 Bool)
39+
(\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
40+
((\ (y:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)), ()))
41+
(\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) -> f x);
42+
43+
-- let rec f = f in f x
44+
test_fun5 : Vec 64 Bool -> CompM (Vec 64 Bool);
45+
test_fun5 x =
46+
letRecM1
47+
(Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
48+
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f)
49+
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f x);
50+
51+
-- let rec f = g and g = f in f x
52+
test_fun6 : Vec 64 Bool -> CompM (Vec 64 Bool);
53+
test_fun6 x =
54+
letRecM
55+
(LRT_Cons
56+
(LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
57+
(LRT_Cons
58+
(LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
59+
LRT_Nil))
60+
(Vec 64 Bool)
61+
(\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
62+
(f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
63+
(f2, (f1, ())))
64+
(\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
65+
(f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
66+
f1 x);
67+
-}

‎examples/mr_solver/mr_solver_unit_tests.saw

+71-16
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
enable_experimental;
22

3+
load_sawcore_from_file "mr_solver_test_funs.sawcore";
4+
35
let eq_bool b1 b2 =
46
if b1 then
57
if b2 then true else false
@@ -15,56 +17,102 @@ let run_test name test expected =
1517
do { print "Test failed\n"; exit 1; }; };
1618

1719
// The constant 0 function const0 x = 0
18-
const0 <- parse_core
19-
"\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0)";
20+
let ret0_core = "retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0)";
21+
let const0_core = str_concat "\\ (_:Vec 64 Bool) -> " ret0_core;
22+
const0 <- parse_core const0_core;
2023

2124
// The constant 1 function const1 x = 1
22-
const1 <- parse_core
23-
"\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1)";
25+
let const1_core = "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1)";
26+
const1 <- parse_core const1_core;
2427

2528
// const0 <= const0
2629
run_test "const0 |= const0" (mr_solver_query const0 const0) true;
27-
28-
/*
29-
// The function test_fun0 from the prelude = const0
30-
test_fun0 <- parse_core "test_fun0";
30+
// (using mrsolver tactic)
31+
let const0_refines =
32+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
33+
"((", const0_core, ") x) ", "((", const0_core, ") x)"];
34+
prove_extcore mrsolver (parse_core const0_refines);
35+
36+
// The function test_fun0 = const0
37+
test_fun0 <- parse_core_mod "test_funs" "test_fun0";
3138
run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;
39+
// (using mrsolver tactic)
40+
let const0_test_fun0_refines =
41+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
42+
"((", const0_core, ") x) ", "(test_fun0 x)"];
43+
prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun0_refines);
3244

3345
// not const0 <= const1
3446
run_test "const0 |= const1" (mr_solver_query const0 const1) false;
35-
36-
// The function test_fun1 from the prelude = const1
37-
test_fun1 <- parse_core "test_fun1";
47+
// (using mrsolver tactic - fails as expected)
48+
// let const0_const1_refines =
49+
// str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
50+
// "((", const0_core, ") x) ", "((", const1_core, ") x)"];
51+
// prove_extcore mrsolver (parse_core const0_const1_refines);
52+
53+
// The function test_fun1 = const1
54+
test_fun1 <- parse_core_mod "test_funs" "test_fun1";
3855
run_test "const1 |= test_fun1" (mr_solver_query const1 test_fun1) true;
3956
run_test "const0 |= test_fun1" (mr_solver_query const0 test_fun1) false;
40-
*/
57+
// (using mrsolver tactic)
58+
let const1_test_fun1_refines =
59+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
60+
"((", const1_core, ") x) ", "(test_fun1 x)"];
61+
prove_extcore mrsolver (parse_core_mod "test_funs" const1_test_fun1_refines);
62+
// (using mrsolver tactic - fails as expected)
63+
// let const0_test_fun1_refines =
64+
// str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
65+
// "((", const0_core, ") x) ", "(test_fun1 x)"];
66+
// prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun1_refines);
4167

4268
// ifxEq0 x = If x == 0 then x else 0; should be equal to 0
43-
ifxEq0 <- parse_core "\\ (x:Vec 64 Bool) -> \
69+
let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
4470
\ ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) \
4571
\ (bvEq 64 x (bvNat 64 0)) \
4672
\ (retS VoidEv emptyFunStack (Vec 64 Bool) x) \
4773
\ (retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0))";
74+
ifxEq0 <- parse_core ifxEq0_core;
4875

4976
// ifxEq0 <= const0
5077
run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true;
78+
// (using mrsolver tactic)
79+
let ifxEq0_const0_refines =
80+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
81+
"((", ifxEq0_core, ") x) ", "((", const0_core, ") x)"];
82+
prove_extcore mrsolver (parse_core ifxEq0_const0_refines);
5183

5284
// not ifxEq0 <= const1
5385
run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;
86+
// (using mrsolver tactic - fails as expected)
87+
// let ifxEq0_const1_refines =
88+
// str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
89+
// "((", ifxEq0_core, ") x) ", "((", const1_core, ") x)"];
90+
// prove_extcore mrsolver (parse_core ifxEq0_const1_refines);
5491

5592
// noErrors1 x = existsS x. retS x
56-
noErrors1 <- parse_core
93+
let noErrors1_core =
5794
"\\ (_:Vec 64 Bool) -> existsS VoidEv emptyFunStack (Vec 64 Bool)";
95+
noErrors1 <- parse_core noErrors1_core;
5896

5997
// const0 <= noErrors
6098
run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true;
99+
// (using mrsolver tactic)
100+
let noErrors1_refines =
101+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
102+
"((", noErrors1_core, ") x) ", "((", noErrors1_core, ") x)"];
103+
prove_extcore mrsolver (parse_core noErrors1_refines);
61104

62105
// const1 <= noErrors
63106
run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;
107+
// (using mrsolver tactic)
108+
let const1_noErrors1_refines =
109+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
110+
"((", const1_core, ") x) ", "((", noErrors1_core, ") x)"];
111+
prove_extcore mrsolver (parse_core const1_noErrors1_refines);
64112

65113
// noErrorsRec1 _ = orS (existsM x. returnM x) (noErrorsRec1 x)
66114
// Intuitively, this specifies functions that either return a value or loop
67-
noErrorsRec1 <- parse_core
115+
let noErrorsRec1_core =
68116
"fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
69117
\ (\\ (f: fixSFun VoidEv emptyFunStack \
70118
\ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
@@ -76,13 +124,20 @@ noErrorsRec1 <- parse_core
76124
\ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
77125
\ (Vec 64 Bool)) \
78126
\ (f x))";
127+
noErrorsRec1 <- parse_core noErrorsRec1_core;
79128

80129
// loop x = loop x
81-
loop1 <- parse_core
130+
let loop1_core =
82131
"fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
83132
\ (\\ (f: fixSFun VoidEv emptyFunStack \
84133
\ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
85134
\ (x:Vec 64 Bool) -> f x)";
135+
loop1 <- parse_core loop1_core;
86136

87137
// loop1 <= noErrorsRec1
88138
run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true;
139+
// (using mrsolver tactic)
140+
let loop1_noErrorsRec1_refines =
141+
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
142+
"((", loop1_core, ") x) ", "((", noErrorsRec1_core, ") x)"];
143+
prove_extcore mrsolver (parse_core loop1_noErrorsRec1_refines);

‎saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

+22-11
Original file line numberDiff line numberDiff line change
@@ -553,6 +553,17 @@ sawCorePreludeSpecialTreatmentMap configuration =
553553
, ("FrameTuple", mapsToExpl specMModule "FrameTuple")
554554
, ("callS", mapsToExpl specMModule "CallS")
555555
, ("multiFixS", mapsToExpl specMModule "MultiFixS")
556+
, ("FunStackE_type", mapsToExpl specMModule "FunStackE")
557+
, ("FunStackE_enc", replace (Coq.Lambda [Coq.Binder "E" (Just (Coq.Var "SpecM.EvType"))]
558+
(Coq.App (Coq.ExplVar "SpecM.FunStackE_encodes")
559+
[Coq.App (Coq.Var "SpecM.evTypeType") [Coq.Var "E"],
560+
Coq.App (Coq.Var "SpecM.evRetType") [Coq.Var "E"]])))
561+
, ("SpecPreRel", mapsToExpl specMModule "SpecPreRel")
562+
, ("SpecPostRel", mapsToExpl specMModule "SpecPostRel")
563+
, ("eqPreRel", mapsToExpl specMModule "eqPreRel")
564+
, ("eqPostRel", mapsToExpl specMModule "eqPostRel")
565+
, ("refinesS", mapsToExpl specMModule "spec_refines")
566+
, ("refinesS_eq", mapsToExpl specMModule "spec_refines_eq")
556567
]
557568

558569
-- Dependent pairs
@@ -566,25 +577,25 @@ sawCorePreludeSpecialTreatmentMap configuration =
566577

567578
-- Lists
568579
++
569-
[ ("List", replace (Coq.ExplVar "Datatypes.list"))
570-
, ("Nil", replace (Coq.ExplVar "Datatypes.nil"))
571-
, ("Cons", replace (Coq.ExplVar "Datatypes.cons"))
572-
, ("List__rec", replace (Coq.ExplVar "Datatypes.list_rect"))
580+
[ ("List", mapsToExpl datatypesModule "list")
581+
, ("Nil", mapsToExpl datatypesModule "nil")
582+
, ("Cons", mapsToExpl datatypesModule "cons")
583+
, ("List__rec", mapsToExpl datatypesModule "list_rect")
573584
]
574585

575586
-- Lists at sort 1
576587
++
577-
[ ("List1", replace (Coq.ExplVar "Datatypes.list"))
578-
, ("Nil1", replace (Coq.ExplVar "Datatypes.nil"))
579-
, ("Cons1", replace (Coq.ExplVar "Datatypes.cons"))
588+
[ ("List1", mapsToExpl datatypesModule "list")
589+
, ("Nil1", mapsToExpl datatypesModule "nil")
590+
, ("Cons1", mapsToExpl datatypesModule "cons")
580591
]
581592

582593
-- Lists at sort 2
583594
++
584-
[ ("List2", replace (Coq.ExplVar "Datatypes.list"))
585-
, ("Nil2", replace (Coq.ExplVar "Datatypes.nil"))
586-
, ("Cons2", replace (Coq.ExplVar "Datatypes.cons"))
587-
, ("List2__rec", replace (Coq.ExplVar "Datatypes.list_rect"))
595+
[ ("List2", mapsToExpl datatypesModule "list")
596+
, ("Nil2", mapsToExpl datatypesModule "nil")
597+
, ("Cons2", mapsToExpl datatypesModule "cons")
598+
, ("List2__rec", mapsToExpl datatypesModule "list_rect")
588599
]
589600

590601
escapeIdent :: String -> String

‎saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,7 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
309309
Recursor (CompiledRecursor d parameters motive _motiveTy eliminators elimOrder) ->
310310
do maybe_d_trans <- translateIdentToIdent (primName d)
311311
rect_var <- case maybe_d_trans of
312-
Just i -> return $ Coq.Var (show i ++ "_rect")
312+
Just i -> return $ Coq.ExplVar (show i ++ "_rect")
313313
Nothing ->
314314
errorTermM ("Recursor for " ++ show d ++
315315
" cannot be translated because the datatype " ++

0 commit comments

Comments
 (0)