sel4: handle platform_pd destruction

Issue #2044

repos/base-sel4/src/core/include/cnode.h

@@ -109,6 +109,10 @@ class Genode::Cnode_base
 
 class Genode::Cnode : public Cnode_base, Noncopyable
 {
+	private:
+
+		addr_t _phys = 0UL;
+
 	public:
 
 		class Untyped_lookup_failed : Exception { };
@@ -135,7 +139,7 @@ class Genode::Cnode : public Cnode_base, Noncopyable
 		:
 			Cnode_base(dst_idx, size_log2)
 		{
-			create<Cnode_kobj>(phys_alloc, parent_sel, dst_idx, size_log2);
+			_phys = create<Cnode_kobj>(phys_alloc, parent_sel, dst_idx, size_log2);
 		}
 
 		/**
@@ -160,13 +164,35 @@ class Genode::Cnode : public Cnode_base, Noncopyable
 			create<Cnode_kobj>(untyped_pool, parent_sel, dst_idx, size_log2);
 		}
 
-		~Cnode()
+		void destruct(Range_allocator &phys_alloc)
 		{
-			/* convert CNode back to untyped memory */
-
 			/* revert phys allocation */
 
-			PDBG("not implemented");
+			if (!_phys) {
+				error("invalid call to destruct Cnode");
+				return;
+			}
+
+			int ret = seL4_CNode_Delete(seL4_CapInitThreadCNode,
+			                            sel().value(), 32);
+			if (ret != seL4_NoError)
+				error(__PRETTY_FUNCTION__, ": seL4_CNode_Delete (",
+				      Hex(sel().value()), ") returned ", ret);
+
+			Untyped_memory::free_page(phys_alloc, _phys);
+
+			_phys = ~0UL;
+		}
+
+		~Cnode()
+		{
+			if (_phys == ~0UL)
+				return;
+
+			/* convert CNode back to untyped memory */
+
+			error(__FUNCTION__, " - not implemented phys=", Hex(_phys),
+			      " sel=", Hex(sel().value()));
 		}
 };
 

repos/base-sel4/src/core/include/page_table_registry.h

@@ -79,6 +79,8 @@ class Genode::Page_table_registry
 
 				Page_table(addr_t addr) : addr(addr) { }
 
+				Entry *first() { return _entries.first(); }
+
 				Entry &lookup(addr_t addr)
 				{
 					for (Entry *e = _entries.first(); e; e = e->next()) {
@@ -221,6 +223,12 @@ class Genode::Page_table_registry
 		 */
 		Page_table_registry(Allocator &md_alloc) { }
 
+		~Page_table_registry()
+		{
+			if (_page_tables.first())
+				error("still entries in page table registry in destruction");
+		}
+
 		/**
 		 * Register page table
 		 *
@@ -299,6 +307,22 @@ class Genode::Page_table_registry
 					PDBG("no PT entry found for virtual address 0x%lx", addr);
 			}
 		}
+
+		template <typename FN>
+		void apply_to_and_destruct_all(FN const &fn)
+		{
+			for (Page_table *pt; (pt = _page_tables.first());) {
+
+				Page_table::Entry *entry = pt->first();
+				for (; entry; entry = entry->next())
+					fn(entry->sel);
+
+				pt->flush_all(_page_table_entry_alloc);
+
+				_page_tables.remove(pt);
+				destroy(_page_table_alloc, pt);
+			}
+		}
 };
 
 #endif /* _CORE__INCLUDE__PAGE_TABLE_REGISTRY_H_ */

repos/base-sel4/src/core/include/untyped_memory.h

@@ -53,6 +53,12 @@ struct Genode::Untyped_memory
 	}
 
 
+	static inline void free_page(Range_allocator &phys_alloc, Genode::addr_t addr)
+	{
+		phys_alloc.free(reinterpret_cast<void *>(addr));
+	}
+
+
 	/**
 	 * Local utility solely used by 'untyped_sel' and 'frame_sel'
 	 */

repos/base-sel4/src/core/include/vm_space.h

@@ -113,8 +113,10 @@ class Genode::Vm_space
 					                 LEAF_CNODE_SIZE_LOG2, phys_alloc);
 				}
 
-				void destruct(Cap_sel_alloc &cap_sel_alloc)
+				void destruct(Cap_sel_alloc &cap_sel_alloc,
+				               Range_allocator &phys_alloc)
 				{
+					_cnode->destruct(phys_alloc);
 					cap_sel_alloc.free(_cnode->sel());
 				}
 
@@ -306,16 +308,31 @@ class Genode::Vm_space
 			_vm_pad_cnode.copy(cspace, _vm_3rd_cnode.sel(), Cnode_index(0));
 
 			/* insert 2nd-level VM-pad CNode into 1st-level CNode */
-			_top_level_cnode.copy(cspace, _vm_pad_cnode.sel(), Cnode_index(id));
+			_top_level_cnode.copy(cspace, _vm_pad_cnode.sel(), Cnode_index(_id));
 		}
 
 		~Vm_space()
 		{
-			_cap_sel_alloc.free(_vm_pad_cnode.sel());
-			_cap_sel_alloc.free(_vm_3rd_cnode.sel());
+			/* delete copy of the mapping's page-frame selectors */
+			_page_table_registry.apply_to_and_destruct_all([&] (unsigned idx) {
+				_leaf_cnode(idx).remove(_leaf_cnode_entry(idx));
+
+				_sel_alloc.free(idx);
+			});
+
+			for (unsigned i = 0; i < NUM_LEAF_CNODES; i++) {
+				_vm_3rd_cnode.remove(Cnode_index(i));
+				_vm_cnodes[i].destruct(_cap_sel_alloc, _phys_alloc);
+			}
+			_vm_pad_cnode.remove(Cnode_index(0));
+			_top_level_cnode.remove(Cnode_index(_id));
+
+			_vm_3rd_cnode.destruct(_phys_alloc);
+			_vm_pad_cnode.destruct(_phys_alloc);
+
+			_cap_sel_alloc.free(_vm_3rd_cnode.sel());
+			_cap_sel_alloc.free(_vm_pad_cnode.sel());
 
-			for (unsigned i = 0; i < NUM_LEAF_CNODES; i++)
-				_vm_cnodes[i].destruct(_cap_sel_alloc);
 		}
 
 		void map(addr_t from_phys, addr_t to_virt, size_t num_pages,

repos/base-sel4/src/core/platform_pd.cc

@@ -194,6 +194,15 @@ Platform_pd::Platform_pd(Allocator * md_alloc, char const *label,
 
 Platform_pd::~Platform_pd()
 {
+	for (unsigned i = 0; i < sizeof(_cspace_cnode_2nd) /
+	                         sizeof(_cspace_cnode_2nd[0]); i++) {
+		_cspace_cnode_2nd[i]->destruct(*platform()->ram_alloc());
+		platform_specific()->core_sel_alloc().free(_cspace_cnode_2nd[i]->sel());
+	}
+
+	_cspace_cnode_1st.destruct(*platform()->ram_alloc());
+	platform_specific()->core_sel_alloc().free(_cspace_cnode_1st.sel());
+
 	/* invalidate weak pointers to this object */
 	Address_space::lock_for_destruction();
 }