diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-24 14:51:15 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-24 14:51:15 +0200 |
| commit | e49318b3606d7568d8592887e4278efa696afd10 (patch) | |
| tree | 99a9a1b883e1db3a4f56e1b5046453817827ceef /backend | |
| parent | 2789e6179af061381f5b18a268adb562b28bcb8e (diff) | |
| parent | c34d25e011402aedad62b3fe9b7b04989df4522e (diff) | |
| download | compcert-kvx-e49318b3606d7568d8592887e4278efa696afd10.tar.gz compcert-kvx-e49318b3606d7568d8592887e4278efa696afd10.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/IRC.ml | 6 | ||||
| -rw-r--r-- | backend/Inlining.v | 7 |
2 files changed, 8 insertions, 5 deletions
diff --git a/backend/IRC.ml b/backend/IRC.ml index 29d224c8..d9e4651e 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -34,8 +34,8 @@ type node = { ident: int; (*r unique identifier *) typ: typ; (*r its type *) var: var; (*r the XTL variable it comes from *) - mutable regclass: int; (*r identifier of register class *) - mutable accesses: int; (*r number of defs and uses *) + regclass: int; (*r identifier of register class *) + accesses: int; (*r number of defs and uses *) mutable spillcost: float; (*r estimated cost of spilling *) mutable adjlist: node list; (*r all nodes it interferes with *) mutable degree: int; (*r number of adjacent nodes *) @@ -207,7 +207,7 @@ type graph = { varTable: (var, node) Hashtbl.t; mutable nextIdent: int; (* The adjacency set *) - mutable adjSet: unit IntPairs.t; + adjSet: unit IntPairs.t; (* Low-degree, non-move-related nodes *) simplifyWorklist: DLinkNode.t; (* Low-degree, move-related nodes *) diff --git a/backend/Inlining.v b/backend/Inlining.v index 0e18d38e..317c288c 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -293,10 +293,13 @@ Inductive inline_decision (ros: reg + ident) : Type := | Cannot_inline | Can_inline (id: ident) (f: function) (P: ros = inr reg id) (Q: fenv!id = Some f). +Arguments Cannot_inline {ros}. +Arguments Can_inline {ros}. + Program Definition can_inline (ros: reg + ident): inline_decision ros := match ros with - | inl r => Cannot_inline _ - | inr id => match fenv!id with Some f => Can_inline _ id f _ _ | None => Cannot_inline _ end + | inl r => Cannot_inline + | inr id => match fenv!id with Some f => Can_inline id f _ _ | None => Cannot_inline end end. (** Inlining of a call to function [f]. An appropriate context is |