-
Notifications
You must be signed in to change notification settings - Fork 63
/
Copy pathPermissions.hs
7822 lines (6748 loc) · 341 KB
/
Permissions.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Verifier.SAW.Heapster.Permissions where
import Prelude hiding (pred)
import Numeric (showHex)
import Data.Char
import qualified Data.Text as Text
import Data.Word
import Data.Maybe
import Data.Either
import Data.List hiding (sort)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.String
import Data.Proxy
import Data.Reflection
import Data.Functor.Constant
import qualified Data.BitVector.Sized as BV
import Data.BitVector.Sized (BV)
import Numeric.Natural
import GHC.TypeLits
import Data.Kind
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Control.Applicative hiding (empty)
import Control.Monad.Identity hiding (ap)
import Control.Monad.State hiding (ap)
import Control.Monad.Reader hiding (ap)
import Control.Lens hiding ((:>), Index, Empty, ix, op)
import Data.Binding.Hobbits hiding (sym)
import Data.Type.RList (append, memberElem, mapRAssign, mapToList, Eq1(..))
import qualified Data.Type.RList as RL
import Data.Binding.Hobbits.MonadBind as MB
import Data.Binding.Hobbits.NameMap (NameMap, NameAndElem(..))
import qualified Data.Binding.Hobbits.NameMap as NameMap
import Data.Binding.Hobbits.NameSet (NameSet, SomeName(..), toList,
SomeRAssign(..), namesListToNames,
nameSetIsSubsetOf)
import qualified Data.Binding.Hobbits.NameSet as NameSet
import Data.Parameterized.Context (Assignment, AssignView(..),
pattern Empty, viewAssign)
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.BoolRepr
import Data.Parameterized.NatRepr
import Data.Parameterized.Pair
import Prettyprinter as PP
import Prettyprinter.Render.String (renderString)
import Lang.Crucible.Types
import Lang.Crucible.FunctionHandle
import Lang.Crucible.LLVM.DataLayout
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.Bytes
import Lang.Crucible.CFG.Core
import Verifier.SAW.Term.Functor (ModuleName)
import Verifier.SAW.Module
import Verifier.SAW.SharedTerm hiding (Constant)
import Verifier.SAW.OpenTerm
import Verifier.SAW.Heapster.CruUtil
import GHC.Stack
import Debug.Trace
----------------------------------------------------------------------
-- * Data types and related types
----------------------------------------------------------------------
-- | The Haskell type of expression variables
type ExprVar = (Name :: CrucibleType -> Type)
-- | Crucible type for lifetimes; we give them a Crucible type so they can be
-- existentially bound in the same way as other Crucible objects
type LifetimeType = IntrinsicType "Lifetime" EmptyCtx
-- | Crucible type for read/write modalities; we give them a Crucible type so
-- they can be used as variables in recursive permission definitions
type RWModalityType = IntrinsicType "RWModality" EmptyCtx
-- | Crucible type for lists of expressions and permissions on them
type PermListType = IntrinsicType "PermList" EmptyCtx
-- | Crucible type for LLVM stack frame objects
type LLVMFrameType w = IntrinsicType "LLVMFrame" (EmptyCtx ::> BVType w)
-- | Crucible type for value permissions themselves
type ValuePermType a = IntrinsicType "Perm" (EmptyCtx ::> a)
-- | Crucible type for LLVM shapes
type LLVMShapeType w = IntrinsicType "LLVMShape" (EmptyCtx ::> BVType w)
-- | Crucible type for LLVM memory blocks
type LLVMBlockType w = IntrinsicType "LLVMBlock" (EmptyCtx ::> BVType w)
-- | Expressions that are considered "pure" for use in permissions. Note that
-- these are in a normal form, that makes them easier to analyze.
data PermExpr (a :: CrucibleType) where
-- | A variable of any type
PExpr_Var :: ExprVar a -> PermExpr a
-- | A unit literal
PExpr_Unit :: PermExpr UnitType
-- | A literal Boolean number
PExpr_Bool :: Bool -> PermExpr BoolType
-- | A literal natural number
PExpr_Nat :: Natural -> PermExpr NatType
-- | A literal string
PExpr_String :: String -> PermExpr (StringType Unicode)
-- | A bitvector expression is a linear expression in @N@ variables, i.e., sum
-- of constant times variable factors plus a constant
--
-- FIXME: make the offset a 'Natural'
PExpr_BV :: (1 <= w, KnownNat w) =>
[BVFactor w] -> BV w -> PermExpr (BVType w)
-- | A struct expression is an expression for each argument of the struct type
PExpr_Struct :: PermExprs (CtxToRList args) -> PermExpr (StructType args)
-- | The @always@ lifetime that is always current
PExpr_Always :: PermExpr LifetimeType
-- | An LLVM value that represents a word, i.e., whose region identifier is 0
PExpr_LLVMWord :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
PermExpr (LLVMPointerType w)
-- | An LLVM value built by adding an offset to an LLVM variable
PExpr_LLVMOffset :: (1 <= w, KnownNat w) =>
ExprVar (LLVMPointerType w) ->
PermExpr (BVType w) ->
PermExpr (LLVMPointerType w)
-- | A literal function pointer
PExpr_Fun :: FnHandle args ret -> PermExpr (FunctionHandleType args ret)
-- | An empty permission list
PExpr_PermListNil :: PermExpr PermListType
-- | A cons of an expression and a permission on it to a permission list
PExpr_PermListCons :: TypeRepr a -> PermExpr a -> ValuePerm a ->
PermExpr PermListType -> PermExpr PermListType
-- | A read/write modality
PExpr_RWModality :: RWModality -> PermExpr RWModalityType
-- | The empty / vacuously true shape
PExpr_EmptyShape :: PermExpr (LLVMShapeType w)
-- | A named shape along with arguments for it, with optional read/write and
-- lifetime modalities that are applied to the body of the shape
PExpr_NamedShape :: KnownNat w => Maybe (PermExpr RWModalityType) ->
Maybe (PermExpr LifetimeType) ->
NamedShape b args w -> PermExprs args ->
PermExpr (LLVMShapeType w)
-- | The equality shape, which describes some @N@ bytes of memory that are
-- equal to a given LLVM block
PExpr_EqShape :: PermExpr (BVType w) -> PermExpr (LLVMBlockType w) ->
PermExpr (LLVMShapeType w)
-- | A shape for a pointer to another memory block, i.e., a @memblock@
-- permission, with a given shape. This @memblock@ permission will have the
-- same read/write and lifetime modalities as the @memblock@ permission
-- containing this pointer shape, unless they are specifically overridden by
-- the pointer shape; i.e., we have that
--
-- > [l]memblock(rw,off,len,ptrsh(rw',l',sh)) =
-- > [l]memblock(rw,off,len,fieldsh([l']memblock(rw',0,len(sh),sh)))
--
-- where @rw'@ and/or @l'@ can be 'Nothing', in which case they default to
-- @rw@ and @l@, respectively.
PExpr_PtrShape :: Maybe (PermExpr RWModalityType) ->
Maybe (PermExpr LifetimeType) ->
PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w)
-- | A shape for a single field with a given permission
PExpr_FieldShape :: (1 <= w, KnownNat w) => LLVMFieldShape w ->
PermExpr (LLVMShapeType w)
-- | A shape for an array of @len@ individual regions of memory, called "array
-- cells"; the size of each cell in bytes is given by the array stride, which
-- must be known statically, and each cell has shape given by the supplied
-- LLVM shape, also called the cell shape
PExpr_ArrayShape :: (1 <= w, KnownNat w) =>
PermExpr (BVType w) -> Bytes ->
PermExpr (LLVMShapeType w) ->
PermExpr (LLVMShapeType w)
-- | A sequence of two shapes
PExpr_SeqShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) ->
PermExpr (LLVMShapeType w)
-- | A disjunctive shape
PExpr_OrShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) ->
PermExpr (LLVMShapeType w)
-- | An existential shape
PExpr_ExShape :: KnownRepr TypeRepr a =>
Binding a (PermExpr (LLVMShapeType w)) ->
PermExpr (LLVMShapeType w)
-- | A false shape
PExpr_FalseShape :: PermExpr (LLVMShapeType w)
-- | A permission as an expression
PExpr_ValPerm :: ValuePerm a -> PermExpr (ValuePermType a)
-- | A sequence of permission expressions
type PermExprs = RAssign PermExpr
{-
data PermExprs (as :: RList CrucibleType) where
PExprs_Nil :: PermExprs RNil
PExprs_Cons :: PermExprs as -> PermExpr a -> PermExprs (as :> a)
-}
-- | A bitvector variable, possibly multiplied by a constant
data BVFactor w where
-- | A variable of type @'BVType' w@ multiplied by a constant @i@, which
-- should be in the range @0 <= i < 2^w@
BVFactor :: (1 <= w, KnownNat w) => BV w -> ExprVar (BVType w) ->
BVFactor w
-- | Whether a permission allows reads or writes
data RWModality
= Write
| Read
deriving Eq
-- | The Haskell type of permission variables, that is, variables that range
-- over 'ValuePerm's
type PermVar (a :: CrucibleType) = Name (ValuePermType a)
-- | Ranges @[off,off+len)@ of bitvector values @x@ equal to @off+y@ for some
-- unsigned @y < len@. Note that ranges are allowed to wrap around 0, meaning
-- @off+y@ can overflow when testing whether @x@ is in the range. Thus, @x@ is
-- in range @[off,off+len)@ iff @x-off@ is unsigned less than @len@.
data BVRange w = BVRange { bvRangeOffset :: PermExpr (BVType w),
bvRangeLength :: PermExpr (BVType w) }
-- | Propositions about bitvectors
data BVProp w
-- | True iff the two expressions are equal
= BVProp_Eq (PermExpr (BVType w)) (PermExpr (BVType w))
-- | True iff the two expressions are not equal
| BVProp_Neq (PermExpr (BVType w)) (PermExpr (BVType w))
-- | True iff the first expression is unsigned less-than the second
| BVProp_ULt (PermExpr (BVType w)) (PermExpr (BVType w))
-- | True iff the first expression is unsigned @<=@ the second
| BVProp_ULeq (PermExpr (BVType w)) (PermExpr (BVType w))
-- | True iff the first expression is unsigned @<=@ the difference of the
-- second minus the third
| (1 <= w, KnownNat w) =>
BVProp_ULeq_Diff (PermExpr (BVType w)) (PermExpr (BVType w))
(PermExpr (BVType w))
-- | An atomic permission is a value permission that is not one of the compound
-- constructs in the 'ValuePerm' type; i.e., not a disjunction, existential,
-- recursive, or equals permission. These are the permissions that we can put
-- together with separating conjuctions.
data AtomicPerm (a :: CrucibleType) where
-- | Gives permissions to a single field pointed to by an LLVM pointer
Perm_LLVMField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
LLVMFieldPerm w sz ->
AtomicPerm (LLVMPointerType w)
-- | Gives permissions to an array pointer to by an LLVM pointer
Perm_LLVMArray :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
AtomicPerm (LLVMPointerType w)
-- | Gives read or write access to a memory block, whose contents also give
-- some permissions
Perm_LLVMBlock :: (1 <= w, KnownNat w) => LLVMBlockPerm w ->
AtomicPerm (LLVMPointerType w)
-- | Says that we have permission to free the memory pointed at by this
-- pointer if we have write permission to @e@ words of size @w@
Perm_LLVMFree :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
AtomicPerm (LLVMPointerType w)
-- | Says that we known an LLVM value is a function pointer whose function has
-- the given permissions
Perm_LLVMFunPtr :: (1 <= w, KnownNat w) =>
TypeRepr (FunctionHandleType cargs ret) ->
ValuePerm (FunctionHandleType cargs ret) ->
AtomicPerm (LLVMPointerType w)
-- | Says that a memory block has a given shape
Perm_LLVMBlockShape :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) ->
AtomicPerm (LLVMBlockType w)
-- | Says we know an LLVM value is a pointer value, meaning that its block
-- value is non-zero. Note that this does not say the pointer is allocated.
Perm_IsLLVMPtr :: (1 <= w, KnownNat w) =>
AtomicPerm (LLVMPointerType w)
-- | A named conjunctive permission
Perm_NamedConj :: NameSortIsConj ns ~ 'True =>
NamedPermName ns args a -> PermExprs args ->
PermOffset a -> AtomicPerm a
-- | Permission to allocate (via @alloca@) on an LLVM stack frame, and
-- permission to delete that stack frame if we have exclusive permissions to
-- all the given LLVM pointer objects
Perm_LLVMFrame :: (1 <= w, KnownNat w) => LLVMFramePerm w ->
AtomicPerm (LLVMFrameType w)
-- | Ownership permission for a lifetime, including an assertion that it is
-- still current and permission to end that lifetime. A lifetime also
-- represents a permission "borrow" of some sub-permissions out of some larger
-- permissions. For example, we might borrow a portion of an array, or a
-- portion of a larger data structure. When the lifetime is ended, you have to
-- give back to sub-permissions to get back the larger permissions. Together,
-- these are a form of permission implication, so we write lifetime ownership
-- permissions as @lowned(Pin -o Pout)@. Intuitively, @Pin@ must be given back
-- before the lifetime is ended, and @Pout@ is returned afterwards.
-- Additionally, a lifetime may contain some other lifetimes, meaning the all
-- must end before the current one can be ended.
Perm_LOwned :: [PermExpr LifetimeType] ->
LOwnedPerms ps_in -> LOwnedPerms ps_out ->
AtomicPerm LifetimeType
-- | A simplified version of @lowned@, written just @lowned(ps)@, which
-- represents a lifetime where the permissions @ps@ have been borrowed and no
-- simplifications have been done. Semantically, this is logically equivalent
-- to @lowned ([l](R)ps -o ps)@, i.e., an @lowned@ permissions where the input
-- and output permissions are the same except that the input permissions are
-- the minimal possible versions of @ps@ in lifetime @l@ that could be given
-- back when @l@ is ended.
Perm_LOwnedSimple :: LOwnedPerms ps -> AtomicPerm LifetimeType
-- | Assertion that a lifetime is current during another lifetime
Perm_LCurrent :: PermExpr LifetimeType -> AtomicPerm LifetimeType
-- | Assertion that a lifetime has finished
Perm_LFinished :: AtomicPerm LifetimeType
-- | A struct permission = a sequence of permissions for each field
Perm_Struct :: RAssign ValuePerm (CtxToRList ctx) ->
AtomicPerm (StructType ctx)
-- | A function permission
Perm_Fun :: FunPerm ghosts (CtxToRList cargs) gouts ret ->
AtomicPerm (FunctionHandleType cargs ret)
-- | An LLVM permission that asserts a proposition about bitvectors
Perm_BVProp :: (1 <= w, KnownNat w) => BVProp w ->
AtomicPerm (LLVMPointerType w)
-- | A value permission is a permission to do something with a value, such as
-- use it as a pointer. This also includes a limited set of predicates on values
-- (you can think about this as "permission to assume the value satisfies this
-- predicate" if you like).
data ValuePerm (a :: CrucibleType) where
-- | Says that a value is equal to a known static expression
ValPerm_Eq :: PermExpr a -> ValuePerm a
-- | The disjunction of two value permissions
ValPerm_Or :: ValuePerm a -> ValuePerm a -> ValuePerm a
-- | An existential binding of a value in a value permission
--
-- FIXME: turn the 'KnownRepr' constraint into a normal 'TypeRepr' argument
ValPerm_Exists :: KnownRepr TypeRepr a =>
Binding a (ValuePerm b) ->
ValuePerm b
-- | A named permission
ValPerm_Named :: NamedPermName ns args a -> PermExprs args ->
PermOffset a -> ValuePerm a
-- | A permission variable plus an offset
ValPerm_Var :: PermVar a -> PermOffset a -> ValuePerm a
-- | A separating conjuction of 0 or more atomic permissions, where 0
-- permissions is the trivially true permission
ValPerm_Conj :: [AtomicPerm a] -> ValuePerm a
-- | The false value permission
ValPerm_False :: ValuePerm a
-- | A sequence of value permissions
{-
data ValuePerms as where
ValPerms_Nil :: ValuePerms RNil
ValPerms_Cons :: ValuePerms as -> ValuePerm a -> ValuePerms (as :> a)
-}
type ValuePerms = RAssign ValuePerm
-- | A binding of 0 or more variables, each with permissions
type MbValuePerms ctx = Mb ctx (ValuePerms ctx)
-- | A frame permission is a list of the pointers that have been allocated in
-- the frame and their corresponding allocation sizes in words of size
-- @w@. Write permissions of the given sizes are required to these pointers in
-- order to delete the frame.
type LLVMFramePerm w = [(PermExpr (LLVMPointerType w), Integer)]
-- | A permission for a pointer to a specific field of a given size
data LLVMFieldPerm w sz =
LLVMFieldPerm { llvmFieldRW :: PermExpr RWModalityType,
-- ^ Whether this is a read or write permission
llvmFieldLifetime :: PermExpr LifetimeType,
-- ^ The lifetime during which this field permission is active
llvmFieldOffset :: PermExpr (BVType w),
-- ^ The offset from the pointer in bytes of this field
llvmFieldContents :: ValuePerm (LLVMPointerType sz)
-- ^ The permissions we get for the value read from this field
}
-- | Helper type to represent byte offsets
--
-- > stride * ix + off
--
-- from the beginning of an array permission. Such an expression refers to
-- offset @off@, which must be a statically-known constant, in array cell @ix@.
data LLVMArrayIndex w =
LLVMArrayIndex { llvmArrayIndexCell :: PermExpr (BVType w),
llvmArrayIndexOffset :: BV w }
-- | A permission to an array of @len@ individual regions of memory, called
-- "array cells". The size of each cell in bytes is given by the array /stride/,
-- which must be known statically, and each cell has shape given by the supplied
-- LLVM shape, also called the cell shape.
data LLVMArrayPerm w =
LLVMArrayPerm { llvmArrayRW :: PermExpr RWModalityType,
-- ^ Whether this array gives read or write access
llvmArrayLifetime :: PermExpr LifetimeType,
-- ^ The lifetime during which this array permission is valid
llvmArrayOffset :: PermExpr (BVType w),
-- ^ The offset from the pointer in bytes of this array
llvmArrayLen :: PermExpr (BVType w),
-- ^ The number of array blocks
llvmArrayStride :: Bytes,
-- ^ The array stride in bytes
llvmArrayCellShape :: PermExpr (LLVMShapeType w),
-- ^ The shape of each cell in the array
llvmArrayBorrows :: [LLVMArrayBorrow w]
-- ^ Indices or index ranges that are missing from this array
}
-- | An index or range of indices that are missing from an array perm
--
-- FIXME: think about calling the just @LLVMArrayIndexSet@
data LLVMArrayBorrow w
= FieldBorrow (PermExpr (BVType w))
-- ^ Borrow a specific cell of an array permission
| RangeBorrow (BVRange w)
-- ^ Borrow a range of array cells, where each cell is 'llvmArrayStride'
-- bytes long
-- | An LLVM block permission is read or write access to the memory at a given
-- offset with a given length with a given shape
data LLVMBlockPerm w =
LLVMBlockPerm { llvmBlockRW :: PermExpr RWModalityType,
-- ^ Whether this is a read or write block permission
llvmBlockLifetime :: PermExpr LifetimeType,
-- ^ The lifetime during with this block permission is active
llvmBlockOffset :: PermExpr (BVType w),
-- ^ The offset of the block from the pointer in bytes
llvmBlockLen :: PermExpr (BVType w),
-- ^ The length of the block in bytes
llvmBlockShape :: PermExpr (LLVMShapeType w)
-- ^ The shape of the permissions in the block
}
-- | An LLVM shape for a single pointer field of unknown size
data LLVMFieldShape w =
forall sz. (1 <= sz, KnownNat sz) =>
LLVMFieldShape (ValuePerm (LLVMPointerType sz))
-- | A form of permission used in lifetime ownership permissions
data LOwnedPerm a where
LOwnedPermField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
PermExpr (LLVMPointerType w) -> LLVMFieldPerm w sz ->
LOwnedPerm (LLVMPointerType w)
LOwnedPermArray :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) ->
LLVMArrayPerm w -> LOwnedPerm (LLVMPointerType w)
LOwnedPermBlock :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) ->
LLVMBlockPerm w -> LOwnedPerm (LLVMPointerType w)
-- | A sequence of 'LOwnedPerm's
type LOwnedPerms = RAssign LOwnedPerm
-- | A function permission is a set of input and output permissions inside a
-- context of ghost variables @ghosts@ with an additional context of output
-- ghost variables @gouts@
data FunPerm ghosts args gouts ret where
FunPerm :: CruCtx ghosts -> CruCtx args -> CruCtx gouts -> TypeRepr ret ->
MbValuePerms (ghosts :++: args) ->
MbValuePerms ((ghosts :++: args) :++: gouts :> ret) ->
FunPerm ghosts args gouts ret
-- | A function permission that existentially quantifies the ghost types
data SomeFunPerm args ret where
SomeFunPerm :: FunPerm ghosts args gouts ret -> SomeFunPerm args ret
-- | The different sorts of name, each of which comes with a 'Bool' flag
-- indicating whether the name can be used as an atomic permission. A recursive
-- sort also comes with a second flag indicating whether it is a reachability
-- permission.
data NameSort = DefinedSort Bool | OpaqueSort Bool | RecursiveSort Bool Bool
type DefinedSort = 'DefinedSort
type OpaqueSort = 'OpaqueSort
type RecursiveSort = 'RecursiveSort
-- | Test whether a name of a given 'NameSort' is conjoinable
type family NameSortIsConj (ns::NameSort) :: Bool where
NameSortIsConj (DefinedSort b) = b
NameSortIsConj (OpaqueSort b) = b
NameSortIsConj (RecursiveSort b _) = b
-- | Test whether a name of a given 'NameSort' is a reachability permission
type family IsReachabilityName (ns::NameSort) :: Bool where
IsReachabilityName (DefinedSort _) = 'False
IsReachabilityName (OpaqueSort _) = 'False
IsReachabilityName (RecursiveSort _ reach) = reach
-- | A singleton representation of 'NameSort'
data NameSortRepr (ns::NameSort) where
DefinedSortRepr :: BoolRepr b -> NameSortRepr (DefinedSort b)
OpaqueSortRepr :: BoolRepr b -> NameSortRepr (OpaqueSort b)
RecursiveSortRepr :: BoolRepr b -> BoolRepr reach ->
NameSortRepr (RecursiveSort b reach)
-- | A constraint that the last argument of a reachability permission is a
-- permission argument
data NameReachConstr ns args a where
NameReachConstr :: (IsReachabilityName ns ~ 'True) =>
NameReachConstr ns (args :> a) a
NameNonReachConstr :: (IsReachabilityName ns ~ 'False) =>
NameReachConstr ns args a
-- | A name for a named permission
data NamedPermName ns args a = NamedPermName {
namedPermNameName :: String,
namedPermNameType :: TypeRepr a,
namedPermNameArgs :: CruCtx args,
namedPermNameSort :: NameSortRepr ns,
namedPermNameReachConstr :: NameReachConstr ns args a
}
-- | An existentially quantified 'NamedPermName'
data SomeNamedPermName where
SomeNamedPermName :: NamedPermName ns args a -> SomeNamedPermName
-- | A named LLVM shape is a name, a list of arguments, and a body, where the
-- Boolean flag @b@ determines whether the shape can be unfolded or not
data NamedShape b args w = NamedShape {
namedShapeName :: String,
namedShapeArgs :: CruCtx args,
namedShapeBody :: NamedShapeBody b args w
}
data NamedShapeBody b args w where
-- | A defined shape is just a definition in terms of the arguments
DefinedShapeBody :: Mb args (PermExpr (LLVMShapeType w)) ->
NamedShapeBody 'True args w
-- | An opaque shape has no body, just a length and a translation to a type
OpaqueShapeBody :: Mb args (PermExpr (BVType w)) -> Ident ->
NamedShapeBody 'False args w
-- | A recursive shape body has a one-step unfolding to a shape, which can
-- refer to the shape itself via the last bound variable; it also has
-- identifiers for the type it is translated to, along with fold and unfold
-- functions for mapping to and from this type. The fold and unfold functions
-- can be undefined if we are in the process of defining this recusive shape.
RecShapeBody :: Mb (args :> LLVMShapeType w) (PermExpr (LLVMShapeType w)) ->
Ident -> Maybe (Ident, Ident) ->
NamedShapeBody 'True args w
-- | An offset that is added to a permission. Only makes sense for llvm
-- permissions (at least for now...?)
data PermOffset a where
NoPermOffset :: PermOffset a
-- | NOTE: the invariant is that the bitvector offset is non-zero
LLVMPermOffset :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
PermOffset (LLVMPointerType w)
-- | The semantics of a named permission, which can can either be an opaque
-- named permission, a recursive named permission, a defined permission, or an
-- LLVM shape
data NamedPerm ns args a where
NamedPerm_Opaque :: OpaquePerm b args a -> NamedPerm (OpaqueSort b) args a
NamedPerm_Rec :: RecPerm b reach args a ->
NamedPerm (RecursiveSort b reach) args a
NamedPerm_Defined :: DefinedPerm b args a -> NamedPerm (DefinedSort b) args a
-- | An opaque named permission is just a name and a SAW core type given by
-- identifier that it is translated to
data OpaquePerm b args a = OpaquePerm {
opaquePermName :: NamedPermName (OpaqueSort b) args a,
opaquePermTrans :: Ident
}
-- | The interpretation of a recursive permission as a reachability permission.
-- Reachability permissions are recursive permissions of the form
--
-- > reach<args,x> = eq(x) | p
--
-- where @reach@ occurs exactly once in @p@ in the form @reach<args,x>@ and @x@
-- does not occur at all in @p@. This means their interpretations look like a
-- list type, where the @eq(x)@ is the nil constructor and the @p@ is the
-- cons. To support the transitivity rule, we need an append function for these
-- lists, which is given by the transitivity method listed here, which has type
--
-- > trans : forall args (x y:A), t args x -> t args y -> t args y
--
-- where @args@ are the arguments and @A@ is the translation of type @a@ (which
-- may correspond to 0 or more arguments)
data ReachMethods reach args a where
ReachMethods :: {
reachMethodTrans :: Ident
} -> ReachMethods (args :> a) a 'True
NoReachMethods :: ReachMethods args a 'False
-- | A recursive permission is a disjunction of 1 or more permissions, each of
-- which can contain the recursive permission itself. NOTE: it is an error to
-- have an empty list of cases. A recursive permission is also associated with a
-- SAW datatype, given by a SAW 'Ident', and each disjunctive permission case is
-- associated with a constructor of that datatype. The @b@ flag indicates
-- whether this recursive permission can be used as an atomic permission, which
-- should be 'True' iff all of the cases are conjunctive permissions as in
-- 'isConjPerm'. If the recursive permission is a reachability permission, then
-- it also has a 'ReachMethods' structure.
data RecPerm b reach args a = RecPerm {
recPermName :: NamedPermName (RecursiveSort b reach) args a,
recPermTransType :: Ident,
recPermFoldFun :: Ident,
recPermUnfoldFun :: Ident,
recPermReachMethods :: ReachMethods args a reach,
recPermCases :: [Mb args (ValuePerm a)]
}
-- | A defined permission is a name and a permission to which it is
-- equivalent. The @b@ flag indicates whether this permission can be used as an
-- atomic permission, which should be 'True' iff the associated permission is a
-- conjunctive permission as in 'isConjPerm'.
data DefinedPerm b args a = DefinedPerm {
definedPermName :: NamedPermName (DefinedSort b) args a,
definedPermDef :: Mb args (ValuePerm a)
}
-- | A pair of a variable and its permission; we give it its own datatype to
-- make certain typeclass instances (like pretty-printing) specific to it
data VarAndPerm a = VarAndPerm (ExprVar a) (ValuePerm a)
-- | A list of "distinguished" permissions to named variables
-- FIXME: just call these VarsAndPerms or something like that...
type DistPerms = RAssign VarAndPerm
-- | A special-purpose 'DistPerms' that specifies a list of permissions needed
-- to prove that a lifetime is current
data LifetimeCurrentPerms ps_l where
-- | The @always@ lifetime needs no proof that it is current
AlwaysCurrentPerms :: LifetimeCurrentPerms RNil
-- | A variable @l@ that is @lowned@ is current, requiring perms
--
-- > l:lowned[ls](ps_in -o ps_out)
LOwnedCurrentPerms :: ExprVar LifetimeType -> [PermExpr LifetimeType] ->
LOwnedPerms ps_in -> LOwnedPerms ps_out ->
LifetimeCurrentPerms (RNil :> LifetimeType)
-- | A variable @l@ with a simple @lowned@ perm is also current
LOwnedSimpleCurrentPerms :: ExprVar LifetimeType -> LOwnedPerms ps ->
LifetimeCurrentPerms (RNil :> LifetimeType)
-- | A variable @l@ that is @lcurrent@ during another lifetime @l'@ is
-- current, i.e., if @ps@ ensure @l'@ is current then we need perms
--
-- > ps, l:lcurrent(l')
CurrentTransPerms :: LifetimeCurrentPerms ps_l -> ExprVar LifetimeType ->
LifetimeCurrentPerms (ps_l :> LifetimeType)
-- | A lifetime functor is a function from a lifetime plus a set of 0 or more
-- rwmodalities to a permission that satisfies a number of properties discussed
-- in Issue #62 (FIXME: copy those here). Rather than try to enforce these
-- properties, we syntactically restrict lifetime functors to one of a few forms
-- that are guaranteed to satisfy the properties. The @args@ type lists all
-- arguments (which should all be rwmodalities) other than the lifetime
-- argument.
data LifetimeFunctor args a where
-- | The functor @\(l,rw) -> [l]ptr((rw,off) |-> p)@
LTFunctorField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
PermExpr (BVType w) -> ValuePerm (LLVMPointerType sz) ->
LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w)
-- | The functor @\(l,rw) -> [l]array(rw,off,<len,*stride,sh,bs)@
LTFunctorArray :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
PermExpr (BVType w) -> Bytes ->
PermExpr (LLVMShapeType w) -> [LLVMArrayBorrow w] ->
LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w)
-- | The functor @\(l,rw) -> [l]memblock(rw,off,len,sh)
LTFunctorBlock :: (1 <= w, KnownNat w) =>
PermExpr (BVType w) -> PermExpr (BVType w) ->
PermExpr (LLVMShapeType w) ->
LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w)
-- FIXME: add functors for arrays and named permissions
-- | An 'LLVMBlockPerm' with a proof that its type is valid
data SomeLLVMBlockPerm a where
SomeLLVMBlockPerm :: (1 <= w, KnownNat w) => LLVMBlockPerm w ->
SomeLLVMBlockPerm (LLVMPointerType w)
-- | A block permission in a binding at some unknown type
data SomeBindingLLVMBlockPerm w =
forall a. SomeBindingLLVMBlockPerm (Binding a (LLVMBlockPerm w))
-- | A tagged union shape is a shape of the form
--
-- > sh1 orsh sh2 orsh ... orsh shn
--
-- where each @shi@ is equivalent up to associativity of the @;@ operator to a
-- shape of the form
--
-- > fieldsh(eq(llvmword(bvi)));shi'
--
-- That is, each disjunct of the shape starts with an equality permission that
-- determines which disjunct should be used. These shapes are represented as a
-- list of the disjuncts, which are tagged with the bitvector values @bvi@ used
-- in the equality permission.
data TaggedUnionShape w sz
= TaggedUnionShape (NonEmpty (BV sz, PermExpr (LLVMShapeType w)))
-- | A 'TaggedUnionShape' with existentially quantified tag size
data SomeTaggedUnionShape w
= forall sz. (1 <= sz, KnownNat sz) =>
SomeTaggedUnionShape (TaggedUnionShape w sz)
-- | Like a substitution but assigns variables instead of arbitrary expressions
-- to bound variables
data PermVarSubst (ctx :: RList CrucibleType) where
PermVarSubst_Nil :: PermVarSubst RNil
PermVarSubst_Cons :: PermVarSubst ctx -> Name tp -> PermVarSubst (ctx :> tp)
-- | An entry in a permission environment that associates a permission and
-- corresponding SAW identifier with a Crucible function handle
data PermEnvFunEntry where
PermEnvFunEntry :: args ~ CtxToRList cargs => FnHandle cargs ret ->
FunPerm ghosts args gouts ret -> Ident ->
PermEnvFunEntry
-- | An existentially quantified 'NamedPerm'
data SomeNamedPerm where
SomeNamedPerm :: NamedPerm ns args a -> SomeNamedPerm
-- | An existentially quantified LLVM shape with arguments
data SomeNamedShape where
SomeNamedShape :: (1 <= w, KnownNat w) => NamedShape b args w ->
SomeNamedShape
-- | An entry in a permission environment that associates a 'GlobalSymbol' with
-- a permission and a translation of that permission
data PermEnvGlobalEntry where
PermEnvGlobalEntry :: (1 <= w, KnownNat w) => GlobalSymbol ->
ValuePerm (LLVMPointerType w) -> [OpenTerm] ->
PermEnvGlobalEntry
-- | The different sorts hints for blocks
data BlockHintSort args where
-- | This hint specifies the ghost args and input permissions for a block
BlockEntryHintSort ::
CruCtx top_args -> CruCtx ghosts ->
MbValuePerms ((top_args :++: CtxToRList args) :++: ghosts) ->
BlockHintSort args
-- | This hint says that the input perms for a block should be generalized
GenPermsHintSort :: BlockHintSort args
-- | This hint says that a block should be a join point
JoinPointHintSort :: BlockHintSort args
-- | A hint for a block
data BlockHint blocks init ret args where
BlockHint :: FnHandle init ret -> Assignment CtxRepr blocks ->
BlockID blocks args -> BlockHintSort args ->
BlockHint blocks init ret args
-- | A "hint" from the user for type-checking
data Hint where
Hint_Block :: BlockHint blocks init ret args -> Hint
-- | A permission environment that maps function names, permission names, and
-- 'GlobalSymbols' to their respective permission structures
data PermEnv = PermEnv {
permEnvFunPerms :: [PermEnvFunEntry],
permEnvNamedPerms :: [SomeNamedPerm],
permEnvNamedShapes :: [SomeNamedShape],
permEnvGlobalSyms :: [PermEnvGlobalEntry],
permEnvHints :: [Hint]
}
----------------------------------------------------------------------
-- * Template Haskell–generated instances
----------------------------------------------------------------------
instance NuMatchingAny1 PermExpr where
nuMatchingAny1Proof = nuMatchingProof
instance NuMatchingAny1 ValuePerm where
nuMatchingAny1Proof = nuMatchingProof
instance NuMatchingAny1 VarAndPerm where
nuMatchingAny1Proof = nuMatchingProof
instance NuMatchingAny1 LOwnedPerm where
nuMatchingAny1Proof = nuMatchingProof
instance NuMatchingAny1 DistPerms where
nuMatchingAny1Proof = nuMatchingProof
$(mkNuMatching [t| forall a . BVFactor a |])
$(mkNuMatching [t| RWModality |])
$(mkNuMatching [t| forall b args w. NamedShapeBody b args w |])
$(mkNuMatching [t| forall b args w. NamedShape b args w |])
$(mkNuMatching [t| forall w . LLVMFieldShape w |])
$(mkNuMatching [t| forall a . PermExpr a |])
$(mkNuMatching [t| forall w. BVRange w |])
$(mkNuMatching [t| forall w. BVProp w |])
$(mkNuMatching [t| forall w sz . LLVMFieldPerm w sz |])
$(mkNuMatching [t| forall w . LLVMArrayBorrow w |])
$(mkNuMatching [t| forall w . LLVMArrayPerm w |])
$(mkNuMatching [t| forall w . LLVMBlockPerm w |])
$(mkNuMatching [t| forall ns. NameSortRepr ns |])
$(mkNuMatching [t| forall ns args a. NameReachConstr ns args a |])
$(mkNuMatching [t| forall ns args a. NamedPermName ns args a |])
$(mkNuMatching [t| forall a. PermOffset a |])
$(mkNuMatching [t| forall w . LOwnedPerm w |])
$(mkNuMatching [t| forall ghosts args gouts ret. FunPerm ghosts args gouts ret |])
$(mkNuMatching [t| forall a . AtomicPerm a |])
$(mkNuMatching [t| forall a . ValuePerm a |])
-- $(mkNuMatching [t| forall as. ValuePerms as |])
$(mkNuMatching [t| forall a . VarAndPerm a |])
$(mkNuMatching [t| forall w . LLVMArrayIndex w |])
$(mkNuMatching [t| forall args ret. SomeFunPerm args ret |])
$(mkNuMatching [t| SomeNamedPermName |])
$(mkNuMatching [t| forall b args a. OpaquePerm b args a |])
$(mkNuMatching [t| forall args a reach. ReachMethods args a reach |])
$(mkNuMatching [t| forall b reach args a. RecPerm b reach args a |])
$(mkNuMatching [t| forall b args a. DefinedPerm b args a |])
$(mkNuMatching [t| forall ns args a. NamedPerm ns args a |])
$(mkNuMatching [t| forall args a. LifetimeFunctor args a |])
$(mkNuMatching [t| forall ps. LifetimeCurrentPerms ps |])
$(mkNuMatching [t| forall a. SomeLLVMBlockPerm a |])
$(mkNuMatching [t| forall w. SomeBindingLLVMBlockPerm w |])
$(mkNuMatching [t| forall w sz. TaggedUnionShape w sz |])
$(mkNuMatching [t| forall w. SomeTaggedUnionShape w |])
$(mkNuMatching [t| forall ctx. PermVarSubst ctx |])
$(mkNuMatching [t| PermEnvFunEntry |])
$(mkNuMatching [t| SomeNamedPerm |])
$(mkNuMatching [t| SomeNamedShape |])
$(mkNuMatching [t| PermEnvGlobalEntry |])
$(mkNuMatching [t| forall args. BlockHintSort args |])
$(mkNuMatching [t| forall blocks init ret args.
BlockHint blocks init ret args |])
$(mkNuMatching [t| Hint |])
$(mkNuMatching [t| PermEnv |])
-- NOTE: this instance would require a NuMatching instance for NameMap...
-- $(mkNuMatching [t| forall ps. PermSet ps |])
----------------------------------------------------------------------
-- * Utility Functions and Definitions
----------------------------------------------------------------------
-- | Call 'RL.split' twice to split a nested appended 'RAssign' into three
rlSplit3 :: prx1 ctx1 -> RAssign prx2 ctx2 -> RAssign prx3 ctx3 ->
RAssign f ((ctx1 :++: ctx2) :++: ctx3) ->
(RAssign f ctx1, RAssign f ctx2, RAssign f ctx3)
rlSplit3 (ctx1 :: prx1 ctx1) (ctx2 :: RAssign prx2 ctx2) ctx3 fs123 =
let (fs12, fs3) = RL.split (Proxy :: Proxy (ctx1 :++: ctx2)) ctx3 fs123 in
let (fs1, fs2) = RL.split ctx1 ctx2 fs12 in
(fs1, fs2, fs3)
-- | Take the ceiling of a division
ceil_div :: Integral a => a -> a -> a
ceil_div a b = (a + b - fromInteger 1) `div` b
-- | Replace the body of a binding with a constant
mbConst :: a -> Mb ctx b -> Mb ctx a
mbConst a = fmap $ const a
-- | Get the first element of a pair in a binding
mbFst :: NuMatching a => NuMatching b => Mb ctx (a,b) -> Mb ctx a
mbFst = mbMapCl $(mkClosed [| fst |])
-- | Get the second element of a pair in a binding
mbSnd :: NuMatching a => NuMatching b => Mb ctx (a,b) -> Mb ctx b
mbSnd = mbMapCl $(mkClosed [| snd |])
-- | Get the first element of a triple in a binding
mbFst3 :: NuMatching a => NuMatching b => NuMatching c =>
Mb ctx (a,b,c) -> Mb ctx a
mbFst3 = mbMapCl $(mkClosed [| \(a,_,_) -> a |])
-- | Get the first element of a triple in a binding
mbSnd3 :: NuMatching a => NuMatching b => NuMatching c =>
Mb ctx (a,b,c) -> Mb ctx b
mbSnd3 = mbMapCl $(mkClosed [| \(_,b,_) -> b |])
-- | Get the first element of a triple in a binding
mbThd3 :: NuMatching a => NuMatching b => NuMatching c =>
Mb ctx (a,b,c) -> Mb ctx c
mbThd3 = mbMapCl $(mkClosed [| \(_,_,c) -> c |])
-- | FIXME: put this somewhere more appropriate
subNat' :: NatRepr m -> NatRepr n -> Maybe (NatRepr (m-n))
subNat' m n
| Left leq <- decideLeq n m =
Just $ withLeqProof leq $ subNat m n
subNat' _ _ = Nothing
-- | Delete the nth element of a list
deleteNth :: Int -> [a] -> [a]
deleteNth i xs | i >= length xs = error "deleteNth"
deleteNth i xs = take i xs ++ drop (i+1) xs
-- | Apply 'deleteNth' inside a name-binding
mbDeleteNth :: NuMatching a => Int -> Mb ctx [a] -> Mb ctx [a]
mbDeleteNth i = mbMapCl ($(mkClosed [| deleteNth |]) `clApply` toClosed i)
-- | Replace the nth element of a list
replaceNth :: Int -> a -> [a] -> [a]
replaceNth i _ xs | i >= length xs = error "replaceNth"
replaceNth i x xs = take i xs ++ x : drop (i+1) xs
-- | Insert an element at the nth location in a list
insertNth :: Int -> a -> [a] -> [a]
insertNth i x xs = take i xs ++ x : drop i xs
-- | Find the @n@th element of a list in a binding
mbNth :: NuMatching a => Int -> Mb ctx [a] -> Mb ctx a
mbNth i = mbMapCl ($(mkClosed [| flip (!!) |]) `clApply` toClosed i)
-- | Find all elements of list @l@ where @f@ returns a value and return that
-- value plus its index into @l@
findMaybeIndices :: (a -> Maybe b) -> [a] -> [(Int, b)]
findMaybeIndices f l = catMaybes $ zipWith (\i a -> (i,) <$> f a) [0 ..] l
-- | Find the index of the first element of a list that returns the maximal
-- positive value from the supplied ranking function, or return 'Nothing' if all
-- elements have non-positive rank
findBestIndex :: (a -> Int) -> [a] -> Maybe Int
findBestIndex rank_f l =
fst $ foldl (\(best_ix,best_rank) (ix,rank) ->
if rank > best_rank then (Just ix, rank) else
(best_ix,best_rank))
(Nothing, 0) (zipWith (\i a -> (i,rank_f a)) [0 ..] l)
-- | Combine all elements of a list like 'foldr1' unless the list is empty, in
-- which case return the default case
foldr1WithDefault :: (a -> a -> a) -> a -> [a] -> a
foldr1WithDefault _ def [] = def
foldr1WithDefault _ _ [a] = a
foldr1WithDefault f def (a:as) = f a $ foldr1WithDefault f def as
-- | Map a function across a list and then call 'foldr1WithDefault'. This is a